fix

Author: kondylidou

src/smt/set_defaults.cpp

@@ -1437,9 +1437,9 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     SET_AND_NOTIFY(quantifiers, cegqi, false, "instMaxLevel");
   }
   // enable MBQI if --mbqi-enum is provided
-  if (opts.quantifiers.mbqiFastSygus)
+  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

@@ -50,7 +50,7 @@ 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));
   }
@@ -496,7 +496,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);
   }
@@ -542,7 +542,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/mbqi_fast_sygus.cpp

@@ -53,7 +53,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)