diff options
| -rw-r--r-- | src/options/quantifiers_options.toml | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 34 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.h | 8 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue3481.smt2 | 2 |
4 files changed, 45 insertions, 14 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 84545e66e..cb989b433 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -545,7 +545,7 @@ header = "options/quantifiers_options.h" long = "full-saturate-quant" type = "bool" default = "false" - help = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown" + help = "enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown" [[option]] name = "fullSaturateQuantRd" @@ -554,16 +554,25 @@ header = "options/quantifiers_options.h" type = "bool" default = "true" read_only = true - help = "whether to use relevant domain first for full saturation instantiation strategy" + help = "whether to use relevant domain first for enumerative instantiation strategy" [[option]] + name = "fullSaturateLimit" + category = "regular" + long = "full-saturate-quant-limit=N" + type = "int" + default = "-1" + read_only = true + help = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)" + +[[option]] name = "fullSaturateInterleave" category = "regular" long = "fs-interleave" type = "bool" default = "false" read_only = true - help = "interleave full saturate instantiation with other techniques" + help = "interleave enumerative instantiation with other techniques" [[option]] name = "fullSaturateStratify" diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 83856dfc4..1e2e34aa2 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -33,12 +33,19 @@ using namespace inst; namespace quantifiers { InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd) - : QuantifiersModule(qe), d_rd(rd) + : QuantifiersModule(qe), d_rd(rd), d_fullSaturateLimit(-1) { } - +void InstStrategyEnum::presolve() +{ + d_fullSaturateLimit = options::fullSaturateLimit(); +} bool InstStrategyEnum::needsCheck(Theory::Effort e) { + if (d_fullSaturateLimit == 0) + { + return false; + } if (options::fullSaturateInterleave()) { if (d_quantEngine->getInstWhenNeedsCheck(e)) @@ -61,15 +68,18 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { bool doCheck = false; bool fullEffort = false; - if (options::fullSaturateInterleave()) + if (d_fullSaturateLimit != 0) { - // we only add when interleaved with other strategies - doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); - } - if (options::fullSaturateQuant() && !doCheck) - { - doCheck = quant_e == QEFFORT_LAST_CALL; - fullEffort = !d_quantEngine->hasAddedLemma(); + if (options::fullSaturateInterleave()) + { + // we only add when interleaved with other strategies + doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + } + if (options::fullSaturateQuant() && !doCheck) + { + doCheck = quant_e == QEFFORT_LAST_CALL; + fullEffort = !d_quantEngine->hasAddedLemma(); + } } if (!doCheck) { @@ -150,6 +160,10 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) Trace("fs-engine") << "Finished full saturation engine, time = " << (clSet2 - clSet) << std::endl; } + if (d_fullSaturateLimit > 0) + { + d_fullSaturateLimit--; + } } bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 48285c877..4d98f00ef 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -64,6 +64,8 @@ class InstStrategyEnum : public QuantifiersModule public: InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd); ~InstStrategyEnum() {} + /** Presolve */ + void presolve() override; /** Needs check. */ bool needsCheck(Theory::Effort e) override; /** Reset round. */ @@ -101,6 +103,12 @@ class InstStrategyEnum : public QuantifiersModule * term instantiations. */ bool process(Node q, bool fullEffort, bool isRd); + /** + * A limit on the number of rounds to apply this strategy, where a value < 0 + * means no limit. This value is set to the value of fullSaturateLimit() + * during presolve. + */ + int32_t d_fullSaturateLimit; }; /* class InstStrategyEnum */ } /* CVC4::theory::quantifiers namespace */ diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2 index 47d2bcbe4..fe8c84d62 100644 --- a/test/regress/regress1/quantifiers/issue3481.smt2 +++ b/test/regress/regress1/quantifiers/issue3481.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --full-saturate-quant +; COMMAND-LINE: --full-saturate-quant --full-saturate-quant-limit=2 ; EXPECT: unsat ;; produced by cvc4_16.drv ;; |