Clean enumerative instantiation options (#7947)

--full-saturate-quant is kept as a generic option, and implies --enum-inst.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 9b4f534b017c0fe11dc62e3ad1dee89e95e4146b..3fe7bbd11fce9d10f53a2ef3e7fc595933973bd7 100755 (executable)
--- 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 4021ac2aa10d25a0f46df37bcf98a4a3f45de365..f477d879c4072c571fc61290036c9c0177f936e4 100644 (file)
--- 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 0335af87057f541360da231a3a865234755b624b..fea9d43985d3419209da131933d94eefa8a1a20a 100644 (file)
--- 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 7b87556a5aae8fdfaef9725d02daba86271c54af..ce671902ce21ee3399b33af90a4b497710291b9a 100644 (file)
--- 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<TermTupleEnumeratorInterface> enumerator(

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 66315c07005b38fcc2252af55c8ed86aab0460ba..544c72800d489d46c83c5580d07c3e500b28915f 100644 (file)
--- 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 16152b50ff0bb408e05a6a1608d5deec3acc7a95..2a13b13ffa69be0c4397d3ed7fb5841560abcb75 100644 (file)
--- 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<TermTupleEnumeratorInterface> enumerator(
       mkTermTupleEnumeratorPool(q, &ttec, tp, p));

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index f882daaba045ab5e0a4072d71d9893fbb6ddd6f2..e63947b201a2d65b95abd798259e9fbc50c64641 100644 (file)
--- 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 3d9bfe981b322c1bb7fa9c195892350c1d42cb9a..3a8c5350a03d79827ee62924e36281e7cad4d8ff 100644 (file)
--- 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 1db06abcd4a8babe4d58fd13f5bb24834d289f3b..37d5242819cf952f3aa58b3e67a4a83ba46dc018 100644 (file)
--- 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)