renaming of mbqi-fast-sygus to mbqi-enum

contrib/competitions/smt-comp/run-script-smtcomp-current

@@ -111,23 +111,23 @@ UFBV)
   trywith 150 --sygus-inst
   trywith 150 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 30 --enum-inst --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 ABV|BV)
   trywith 80 --enum-inst
   trywith 80 --sygus-inst
   trywith 80 --mbqi --no-cegqi --no-sygus-inst
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   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 --enum-inst --no-cegqi-innermost --global-negate
   ;;
 ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA|BVFPLRA)
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --nl-ext-tplanes
   trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --sygus-inst
@@ -136,7 +136,7 @@ LIA|LRA)
   trywith 30 --enum-inst
   trywith 300 --enum-inst --cegqi-nested-qe
   trywith 30 --mbqi --no-cegqi --no-sygus-inst
-  trywith 30 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 30 --mbqi-enum --no-cegqi --no-sygus-inst
   finishwith --enum-inst --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)

contrib/competitions/smt-comp/run-script-smtcomp2024

@@ -111,23 +111,23 @@ UFBV)
   trywith 150 --sygus-inst
   trywith 150 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 30 --enum-inst --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 ABV|BV)
   trywith 80 --enum-inst
   trywith 80 --sygus-inst
   trywith 80 --mbqi --no-cegqi --no-sygus-inst
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   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 --enum-inst --no-cegqi-innermost --global-negate
   ;;
 ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA|BVFPLRA)
-  trywith 300 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 300 --mbqi-enum --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --nl-ext-tplanes
   trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --sygus-inst
@@ -136,7 +136,7 @@ LIA|LRA)
   trywith 30 --enum-inst
   trywith 300 --enum-inst --cegqi-nested-qe
   trywith 30 --mbqi --no-cegqi --no-sygus-inst
-  trywith 30 --mbqi-fast-sygus --no-cegqi --no-sygus-inst
+  trywith 30 --mbqi-enum --no-cegqi --no-sygus-inst
   finishwith --enum-inst --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)

src/CMakeLists.txt

@@ -911,8 +911,8 @@ libcvc5_add_sources(
   theory/quantifiers/lazy_trie.h
   theory/quantifiers/master_eq_notify.cpp
   theory/quantifiers/master_eq_notify.h
-  theory/quantifiers/mbqi_fast_sygus.cpp
-  theory/quantifiers/mbqi_fast_sygus.h
+  theory/quantifiers/mbqi_enum.cpp
+  theory/quantifiers/mbqi_enum.h
   theory/quantifiers/oracle_checker.cpp
   theory/quantifiers/oracle_checker.h
   theory/quantifiers/oracle_engine.cpp

src/options/quantifiers_options.toml

@@ -201,33 +201,33 @@ name   = "Quantifiers"
   help       = "use model-based quantifier instantiation"
 
 [[option]]
-  name       = "mbqiFastSygus"
+  name       = "mbqiEnum"
   category   = "expert"
-  long       = "mbqi-fast-sygus"
+  long       = "mbqi-enum"
   type       = "bool"
   default    = "false"
   help       = "use fast enumeration to augment instantiations from MBQI"
 
 [[option]]
-  name       = "mbqiFastSygusExtVarsGrammar"
+  name       = "mbqiEnumExtVarsGrammar"
   category   = "expert"
-  long       = "mbqi-fast-sygus-ext-vars-grammar"
+  long       = "mbqi-enum-ext-vars-grammar"
   type       = "bool"
   default    = "true"
   help       = "include variables defined in terms of others in grammars for fast enumerative mbqi"
 
 [[option]]
-  name       = "mbqiFastSygusFreeSymsGrammar"
+  name       = "mbqiEnumFreeSymsGrammar"
   category   = "expert"
-  long       = "mbqi-fast-sygus-free-syms-grammar"
+  long       = "mbqi-enum-free-syms-grammar"
   type       = "bool"
   default    = "true"
   help       = "include free symbols from the body of the quantified formula in grammars for fast enumerative mbqi"
 
 [[option]]
-  name       = "mbqiFastSygusGlobalSymGrammar"
+  name       = "mbqiEnumGlobalSymGrammar"
   category   = "expert"
-  long       = "mbqi-fast-sygus-global-syms-grammar"
+  long       = "mbqi-enum-global-syms-grammar"
   type       = "bool"
   default    = "false"
   help       = "include global symbols from all available assertions in grammars for fast enumerative mbqi"

src/smt/set_defaults.cpp

@@ -1532,10 +1532,10 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     SET_AND_NOTIFY(quantifiers, cegqi, false, "instMaxLevel");
   }
-  // enable MBQI if --mbqi-fast-sygus is provided
-  if (opts.quantifiers.mbqiFastSygus)
+  // enable MBQI if --mbqi-enum is provided
+  if (opts.quantifiers.mbqiEnum)
   {
-    SET_AND_NOTIFY_IF_NOT_USER(quantifiers, mbqi, true, "mbqiFastSygus");
+    SET_AND_NOTIFY_IF_NOT_USER(quantifiers, mbqi, true, "mbqiEnum");
   }
   if (opts.quantifiers.mbqi)
   {

src/theory/quantifiers/inst_strategy_mbqi.cpp

@@ -19,7 +19,7 @@
 #include "expr/skolem_manager.h"
 #include "expr/subs.h"
 #include "printer/smt2/smt2_printer.h"
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
@@ -51,9 +51,9 @@ InstStrategyMbqi::InstStrategyMbqi(Env& env,
   // may appear in certain models e.g. strings of excessive length
   d_nonClosedKinds.insert(Kind::WITNESS);
 
-  if (options().quantifiers.mbqiFastSygus)
+  if (options().quantifiers.mbqiEnum)
   {
-    d_msenum.reset(new MbqiFastSygus(env, *this));
+    d_msenum.reset(new MbqiEnum(env, *this));
   }
   d_subOptions.copyValues(options());
   smt::SetDefaults::disableChecking(d_subOptions);
@@ -322,7 +322,6 @@ void InstStrategyMbqi::process(Node q)
   // get a term that has the same model value as the value each fresh variable
   // represents
   Subs fvToInst;
-  // bool modifiedInst = false;
   for (const Node& v : allVars)
   {
     // get a term that witnesses this variable
@@ -332,7 +331,6 @@ void InstStrategyMbqi::process(Node q)
     // is combined with MBQI
     if (mvt.isNull() || !TermUtil::getInstConstAttr(mvt).isNull())
     {
-      // modifiedInst = true;
       Trace("mbqi") << "warning: failed to get term from value " << ov
                     << ", use arbitrary term in query" << std::endl;
       mvt = NodeManager::mkGroundTerm(ov.getType());
@@ -351,7 +349,6 @@ void InstStrategyMbqi::process(Node q)
   Instantiate* qinst = d_qim.getInstantiate();
   if (!qinst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_MBQI))
   {
-    // AlwaysAssert(modifiedInst) << "Failed to add instantiation";
     Trace("mbqi") << "...failed to add instantiation" << std::endl;
     return;
   }
@@ -500,7 +497,7 @@ Node InstStrategyMbqi::convertToQuery(
 Node InstStrategyMbqi::modelValueToQuery(const Node& t)
 {
   FirstOrderModel* fm = d_treg.getModel();
-  if (!options().quantifiers.mbqiFastSygus)
+  if (!options().quantifiers.mbqiEnum)
   {
     return fm->getValue(t);
   }
@@ -546,7 +543,7 @@ void InstStrategyMbqi::modelValueFromQuery(
     const std::map<Node, Node>& mvToFreshVar)
 {
   getModelFromSubsolver(smt, vars, mvs);
-  if (options().quantifiers.mbqiFastSygus)
+  if (options().quantifiers.mbqiEnum)
   {
     std::vector<Node> smvs(mvs);
     if (d_msenum->constructInstantiation(q, query, vars, smvs, mvToFreshVar))

src/theory/quantifiers/inst_strategy_mbqi.h

@@ -32,7 +32,7 @@ class SolverEngine;
 namespace theory {
 namespace quantifiers {
 
-class MbqiFastSygus;
+class MbqiEnum;
 
 /**
  * InstStrategyMbqi
@@ -47,7 +47,7 @@ class MbqiFastSygus;
  */
 class InstStrategyMbqi : public QuantifiersModule
 {
-  friend class MbqiFastSygus;
+  friend class MbqiEnum;
  public:
   InstStrategyMbqi(Env& env,
                    QuantifiersState& qs,
@@ -66,7 +66,7 @@ class InstStrategyMbqi : public QuantifiersModule
   /** Check was complete for quantified formula q */
   bool checkCompleteFor(Node q) override;
   /** For collecting global terms from all available assertions. */
-  void ppNotifyAssertions(const std::vector<Node>& assertions);
+  void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   /** Get the symbols appearing in assertions */
   const context::CDHashSet<Node>& getGlobalSyms() const;
   /** identify */
@@ -139,7 +139,7 @@ class InstStrategyMbqi : public QuantifiersModule
   /** Kinds that cannot appear in queries */
   std::unordered_set<Kind, kind::KindHashFunction> d_nonClosedKinds;
   /** Submodule for sygus enum */
-  std::unique_ptr<MbqiFastSygus> d_msenum;
+  std::unique_ptr<MbqiEnum> d_msenum;
   /** The options for subsolver calls */
   Options d_subOptions;
   /* Set of global ground terms in assertions (outside of quantifiers). */

src/theory/quantifiers/mbqi_fast_sygus.cpp → src/theory/quantifiers/mbqi_enum.cpp

@@ -13,7 +13,7 @@
  * A class for augmenting model-based instantiations via fast sygus enumeration.
  */
 
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
@@ -54,7 +54,7 @@ void MVarInfo::initialize(Env& env,
     trules.insert(trules.end(), vs.begin(), vs.end());
   }
   // include free symbols from body of quantified formula if applicable
-  if (env.getOptions().quantifiers.mbqiFastSygusFreeSymsGrammar)
+  if (env.getOptions().quantifiers.mbqiEnumFreeSymsGrammar)
   {
     std::unordered_set<Node> syms;
     expr::getSymbols(q[1], syms);
@@ -144,14 +144,14 @@ void MQuantInfo::initialize(Env& env, InstStrategyMbqi& parent, const Node& q)
     {
       d_nindices.push_back(index);
       // include variables defined in terms of others if applicable
-      if (env.getOptions().quantifiers.mbqiFastSygusExtVarsGrammar)
+      if (env.getOptions().quantifiers.mbqiEnumExtVarsGrammar)
       {
         etrules.push_back(v);
       }
     }
   }
   // include the global symbols if applicable
-  if (env.getOptions().quantifiers.mbqiFastSygusGlobalSymGrammar)
+  if (env.getOptions().quantifiers.mbqiEnumGlobalSymGrammar)
   {
     const context::CDHashSet<Node>& gsyms = parent.getGlobalSyms();
     for (const Node& v : gsyms)
@@ -184,14 +184,14 @@ bool MQuantInfo::shouldEnumerate(const TypeNode& tn)
   return true;
 }
 
-MbqiFastSygus::MbqiFastSygus(Env& env, InstStrategyMbqi& parent)
+MbqiEnum::MbqiEnum(Env& env, InstStrategyMbqi& parent)
     : EnvObj(env), d_parent(parent)
 {
   d_subOptions.copyValues(options());
   smt::SetDefaults::disableChecking(d_subOptions);
 }
 
-MQuantInfo& MbqiFastSygus::getOrMkQuantInfo(const Node& q)
+MQuantInfo& MbqiEnum::getOrMkQuantInfo(const Node& q)
 {
   auto [it, inserted] = d_qinfo.try_emplace(q);
   if (inserted)
@@ -201,18 +201,13 @@ MQuantInfo& MbqiFastSygus::getOrMkQuantInfo(const Node& q)
   return it->second;
 }
 
-bool MbqiFastSygus::constructInstantiation(
+bool MbqiEnum::constructInstantiation(
     const Node& q,
     const Node& query,
     const std::vector<Node>& vars,
     std::vector<Node>& mvs,
     const std::map<Node, Node>& mvFreshVar)
 {
-  // TODO: it would better for the last child to simply invoke addInstantiation
-  // as an oracle to determine if the instantiation is feasiable. This would
-  // avoid one subsolver call per instantiation we construct.
-  // Doing this ignores the constructed model in favor of using "entailment"
-  // from the main solver. This is likely a better notion of filtering.
   Assert(q[0].getNumChildren() == vars.size());
   Assert(vars.size() == mvs.size());
   if (TraceIsOn("mbqi-model-enum"))

src/theory/quantifiers/mbqi_fast_sygus.h → src/theory/quantifiers/mbqi_enum.h

@@ -15,8 +15,8 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H
-#define CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H
+#define CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H
 
 #include <map>
 #include <unordered_map>
@@ -108,14 +108,14 @@ class MQuantInfo
 };
 
 /**
- * MbqiFastSygus, which postprocesses an instantiation from MBQI based on
+ * MbqiEnum, which postprocesses an instantiation from MBQI based on
  * sygus enumeration.
  */
-class MbqiFastSygus : protected EnvObj
+class MbqiEnum : protected EnvObj
 {
  public:
-  MbqiFastSygus(Env& env, InstStrategyMbqi& parent);
-  ~MbqiFastSygus() {}
+  MbqiEnum(Env& env, InstStrategyMbqi& parent);
+  ~MbqiEnum() {}
 
   /**
    * Updates mvs to the desired instantiation of q. Returns true if successful.
@@ -160,4 +160,4 @@ class MbqiFastSygus : protected EnvObj
 }  // namespace theory
 }  // namespace cvc5::internal
 
-#endif /* CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H */

src/theory/quantifiers/quantifiers_modules.h

@@ -29,7 +29,7 @@
 #include "theory/quantifiers/inst_strategy_mbqi.h"
 #include "theory/quantifiers/inst_strategy_pool.h"
 #include "theory/quantifiers/inst_strategy_sub_conflict.h"
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 #include "theory/quantifiers/oracle_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_split.h"

src/theory/quantifiers_engine.cpp

@@ -181,7 +181,7 @@ void QuantifiersEngine::ppNotifyAssertions(
   }
   if (options().quantifiers.mbqi)
   {
-    // may need to be notified of assertions, for mbqi-fast-sygus
+    // may need to be notified of assertions, for mbqi-enum
     quantifiers::InstStrategyMbqi* mi = d_qmodules->d_mbqi.get();
     mi->ppNotifyAssertions(assertions);
   }

test/regress/cli/regress0/ho/dd.lcl720.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: sat
 (set-logic HO_ALL)
 (declare-const P (-> Int Bool))

test/regress/cli/regress0/ho/m-enum-bug1.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

test/regress/cli/regress0/ho/m-enum-bug2.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

test/regress/cli/regress0/ho/m-enum-bug3.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)

test/regress/cli/regress1/quantifiers/ho-grammar.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 (set-logic HO_ALL)

test/regress/cli/regress1/quantifiers/lcl579-2-ho-mbqi.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --mbqi --mbqi-fast-sygus
+; COMMAND-LINE: --mbqi --mbqi-enum
 ; EXPECT: unsat
 (set-logic HO_ALL)
 (declare-sort a 0)