From 9b120a987bc0421d2fd9029ec9b9b7c6a78c3897 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Jan 2022 16:56:46 -0600 Subject: [PATCH] Clean enumerative instantiation options (#7947) --full-saturate-quant is kept as a generic option, and implies --enum-inst. --- .../smt-comp/run-script-smtcomp-current | 58 +++++++++---------- src/options/quantifiers_options.toml | 28 +++++---- src/smt/set_defaults.cpp | 5 ++ .../quantifiers/inst_strategy_enumerative.cpp | 42 +++++++------- .../quantifiers/inst_strategy_enumerative.h | 2 +- src/theory/quantifiers/inst_strategy_pool.cpp | 2 +- .../quantifiers/quantifiers_modules.cpp | 2 +- .../regress1/quantifiers/issue3481.smt2 | 2 +- .../regress2/quantifiers/syn874-1.smt2 | 2 +- 9 files changed, 78 insertions(+), 65 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 9b4f534b0..3fe7bbd11 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -77,25 +77,25 @@ QF_NRA) # all logics with UF + quantifiers should either fall under this or special cases below ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) # initial runs 1 min - trywith 30 --simplification=none --full-saturate-quant - trywith 30 --no-e-matching --full-saturate-quant - trywith 30 --no-e-matching --full-saturate-quant --fs-sum + trywith 30 --simplification=none --enum-inst + trywith 30 --no-e-matching --enum-inst + trywith 30 --no-e-matching --enum-inst --enum-inst-sum # trigger selections 3 min - trywith 30 --relevant-triggers --full-saturate-quant - trywith 30 --trigger-sel=max --full-saturate-quant - trywith 30 --multi-trigger-when-single --full-saturate-quant - trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant - trywith 30 --multi-trigger-cache --full-saturate-quant - trywith 30 --no-multi-trigger-linear --full-saturate-quant + trywith 30 --relevant-triggers --enum-inst + trywith 30 --trigger-sel=max --enum-inst + trywith 30 --multi-trigger-when-single --enum-inst + trywith 30 --multi-trigger-when-single --multi-trigger-priority --enum-inst + trywith 30 --multi-trigger-cache --enum-inst + trywith 30 --no-multi-trigger-linear --enum-inst # other 4 min - trywith 30 --pre-skolem-quant --full-saturate-quant - trywith 30 --inst-when=full --full-saturate-quant - trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant - trywith 30 --full-saturate-quant --quant-ind - trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant - trywith 30 --decision=internal --full-saturate-quant --fs-sum - trywith 30 --term-db-mode=relevant --full-saturate-quant - trywith 30 --fs-interleave --full-saturate-quant + trywith 30 --pre-skolem-quant --enum-inst + trywith 30 --inst-when=full --enum-inst + trywith 30 --no-e-matching --no-quant-cf --enum-inst + trywith 30 --enum-inst --quant-ind + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --enum-inst + trywith 30 --decision=internal --enum-inst --enum-inst-sum + trywith 30 --term-db-mode=relevant --enum-inst + trywith 30 --enum-inst-interleave --enum-inst # finite model find 3 min trywith 30 --finite-model-find --mbqi=none trywith 30 --finite-model-find --decision=internal @@ -103,32 +103,32 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD trywith 60 --finite-model-find --fmf-inst-engine # long runs 4 min trywith 240 --finite-model-find --decision=internal - finishwith --full-saturate-quant + finishwith --enum-inst ;; UFBV) # most problems in UFBV are essentially BV trywith 300 --sygus-inst - trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal - trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate + trywith 300 --enum-inst --cegqi-nested-qe --decision=internal + trywith 30 --enum-inst --no-cegqi-innermost --global-negate finishwith --finite-model-find ;; ABV|BV) - trywith 120 --full-saturate-quant + trywith 120 --enum-inst trywith 120 --sygus-inst - trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal - trywith 30 --full-saturate-quant --no-cegqi-bv - trywith 30 --full-saturate-quant --cegqi-bv-ineq=eq-slack + trywith 300 --enum-inst --cegqi-nested-qe --decision=internal + trywith 30 --enum-inst --no-cegqi-bv + trywith 30 --enum-inst --cegqi-bv-ineq=eq-slack # finish 10min - finishwith --full-saturate-quant --no-cegqi-innermost --global-negate + finishwith --enum-inst --no-cegqi-innermost --global-negate ;; ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA) - trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp + trywith 300 --enum-inst --nl-ext-tplanes --fp-exp finishwith --sygus-inst --fp-exp ;; LIA|LRA) - trywith 30 --full-saturate-quant - trywith 300 --full-saturate-quant --cegqi-nested-qe - finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal + trywith 30 --enum-inst + trywith 300 --enum-inst --cegqi-nested-qe + finishwith --enum-inst --cegqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4021ac2aa..f477d879c 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -505,44 +505,52 @@ name = "Quantifiers" long = "full-saturate-quant" type = "bool" default = "false" + help = "resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation" + +[[option]] + name = "enumInst" + category = "regular" + long = "enum-inst" + type = "bool" + default = "false" help = "enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown" [[option]] - name = "fullSaturateQuantRd" + name = "enumInstRd" category = "regular" - long = "full-saturate-quant-rd" + long = "enum-inst-rd" type = "bool" default = "true" help = "whether to use relevant domain first for enumerative instantiation strategy" [[option]] - name = "fullSaturateLimit" + name = "enumInstLimit" category = "regular" - long = "full-saturate-quant-limit=N" + long = "enum-inst-limit=N" type = "int64_t" default = "-1" help = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)" [[option]] - name = "fullSaturateInterleave" + name = "enumInstInterleave" category = "regular" - long = "fs-interleave" + long = "enum-inst-interleave" type = "bool" default = "false" help = "interleave enumerative instantiation with other techniques" [[option]] - name = "fullSaturateStratify" + name = "enumInstStratify" category = "regular" - long = "fs-stratify" + long = "enum-inst-stratify" type = "bool" default = "false" help = "stratify effort levels in enumerative instantiation, which favors speed over fairness" [[option]] - name = "fullSaturateSum" + name = "enumInstSum" category = "regular" - long = "fs-sum" + long = "enum-inst-sum" type = "bool" default = "false" help = "enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 0335af870..fea9d4398 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1258,6 +1258,11 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, Options& opts) const { + if (opts.quantifiers.fullSaturateQuant) + { + Trace("smt") << "enabling enum-inst for full-saturate-quant" << std::endl; + opts.quantifiers.enumInst = true; + } if (opts.arrays.arraysExp) { // Allows to answer sat more often by default. diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 7b87556a5..ce671902c 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -35,20 +35,20 @@ InstStrategyEnum::InstStrategyEnum(Env& env, QuantifiersRegistry& qr, TermRegistry& tr, RelevantDomain* rd) - : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_enumInstLimit(-1) { } void InstStrategyEnum::presolve() { - d_fullSaturateLimit = options().quantifiers.fullSaturateLimit; + d_enumInstLimit = options().quantifiers.enumInstLimit; } bool InstStrategyEnum::needsCheck(Theory::Effort e) { - if (d_fullSaturateLimit == 0) + if (d_enumInstLimit == 0) { return false; } - if (options().quantifiers.fullSaturateInterleave) + if (options().quantifiers.enumInstInterleave) { // if interleaved, we run at the same time as E-matching if (d_qstate.getInstWhenNeedsCheck(e)) @@ -56,7 +56,7 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e) return true; } } - if (options().quantifiers.fullSaturateQuant) + if (options().quantifiers.enumInst) { if (e >= Theory::EFFORT_LAST_CALL) { @@ -71,14 +71,14 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { bool doCheck = false; bool fullEffort = false; - if (d_fullSaturateLimit != 0) + if (d_enumInstLimit != 0) { - if (options().quantifiers.fullSaturateInterleave) + if (options().quantifiers.enumInstInterleave) { // we only add when interleaved with other strategies doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma(); } - if (options().quantifiers.fullSaturateQuant && !doCheck) + if (options().quantifiers.enumInst && !doCheck) { if (!d_qstate.getValuation().needCheck()) { @@ -93,13 +93,13 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } Assert(!d_qstate.isInConflict()); double clSet = 0; - if (Trace.isOn("fs-engine")) + if (Trace.isOn("enum-engine")) { clSet = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" - << std::endl; + Trace("enum-engine") << "---Full Saturation Round, effort = " << e << "---" + << std::endl; } - unsigned rstart = options().quantifiers.fullSaturateQuantRd ? 0 : 1; + unsigned rstart = options().quantifiers.enumInstRd ? 0 : 1; unsigned rend = fullEffort ? 1 : rstart; unsigned addedLemmas = 0; // First try in relevant domain of all quantified formulas, if no @@ -138,7 +138,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) if (process(q, fullEffort, r == 0)) { // don't need to mark this if we are not stratifying - if (!options().quantifiers.fullSaturateStratify) + if (!options().quantifiers.enumInstStratify) { alreadyProc[q] = true; } @@ -152,7 +152,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } } if (d_qstate.isInConflict() - || (addedLemmas > 0 && options().quantifiers.fullSaturateStratify)) + || (addedLemmas > 0 && options().quantifiers.enumInstStratify)) { // we break if we are in conflict, or if we added any lemma at this // effort level and we stratify effort levels. @@ -160,16 +160,16 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } } } - if (Trace.isOn("fs-engine")) + if (Trace.isOn("enum-engine")) { - Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + Trace("enum-engine") << "Added lemmas = " << addedLemmas << std::endl; double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished full saturation engine, time = " - << (clSet2 - clSet) << std::endl; + Trace("enum-engine") << "Finished full saturation engine, time = " + << (clSet2 - clSet) << std::endl; } - if (d_fullSaturateLimit > 0) + if (d_enumInstLimit > 0) { - d_fullSaturateLimit--; + d_enumInstLimit--; } } @@ -184,7 +184,7 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) TermTupleEnumeratorEnv ttec; ttec.d_fullEffort = fullEffort; - ttec.d_increaseSum = options().quantifiers.fullSaturateSum; + ttec.d_increaseSum = options().quantifiers.enumInstSum; // make the enumerator, which is either relevant domain or term database // based on the flag isRd. std::unique_ptr enumerator( diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 66315c070..544c72800 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -114,7 +114,7 @@ class InstStrategyEnum : public QuantifiersModule * means no limit. This value is set to the value of fullSaturateLimit() * during presolve. */ - int32_t d_fullSaturateLimit; + int32_t d_enumInstLimit; }; /* class InstStrategyEnum */ } // namespace quantifiers diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp index 16152b50f..2a13b13ff 100644 --- a/src/theory/quantifiers/inst_strategy_pool.cpp +++ b/src/theory/quantifiers/inst_strategy_pool.cpp @@ -129,7 +129,7 @@ bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas) { TermTupleEnumeratorEnv ttec; ttec.d_fullEffort = true; - ttec.d_increaseSum = options().quantifiers.fullSaturateSum; + ttec.d_increaseSum = options().quantifiers.enumInstSum; TermPools* tp = d_treg.getTermPools(); std::shared_ptr enumerator( mkTermTupleEnumeratorPool(q, &ttec, tp, p)); diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index f882daaba..e63947b20 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -99,7 +99,7 @@ void QuantifiersModules::initialize(Env& env, d_alpha_equiv.reset(new AlphaEquivalence(env)); } // full saturation : instantiate from relevant domain, then arbitrary terms - if (options::fullSaturateQuant() || options::fullSaturateInterleave()) + if (options::enumInst() || options::enumInstInterleave()) { d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr)); d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get())); diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2 index 3d9bfe981..3a8c5350a 100644 --- a/test/regress/regress1/quantifiers/issue3481.smt2 +++ b/test/regress/regress1/quantifiers/issue3481.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --full-saturate-quant --full-saturate-quant-limit=2 +; COMMAND-LINE: --enum-inst --enum-inst-limit=2 ; EXPECT: unsat ;; produced by cvc4_16.drv ;; diff --git a/test/regress/regress2/quantifiers/syn874-1.smt2 b/test/regress/regress2/quantifiers/syn874-1.smt2 index 1db06abcd..37d524281 100644 --- a/test/regress/regress2/quantifiers/syn874-1.smt2 +++ b/test/regress/regress2/quantifiers/syn874-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --full-saturate-quant --fs-stratify +; COMMAND-LINE: --enum-inst --enum-inst-stratify ; EXPECT: unsat (set-logic ALL) (declare-sort $$unsorted 0) -- 2.30.2