Change option name for mbqi in fmf (#8701)

In preparation for a new basic implementation of MBQI.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index bbd26f702c466c7ed23bdf0842864d0b3e41bca9..a4c33c946ad3d08076404f22cb7b2d64351e526c 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -602,10 +602,10 @@ name   = "Quantifiers"
   help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
 
 [[option]]
-  name       = "mbqiMode"
+  name       = "fmfMbqiMode"
   category   = "expert"
-  long       = "mbqi=MODE"
-  type       = "MbqiMode"
+  long       = "fmf-mbqi=MODE"
+  type       = "FmfMbqiMode"
   default    = "FMC"
   help       = "choose mode for model-based quantifier instantiation"
   help_mode  = "Model-based quantifier instantiation modes."

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 32fd86f2460652b3c8c7f2da17032c614b12288a..4f54310e7b75ae723c9edc183cf8b1e1118bd071 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1416,12 +1416,12 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   // apply fmfBound options
   if (opts.quantifiers.fmfBound)
   {
-    if (!opts.quantifiers.mbqiModeWasSetByUser
-        || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE
-            && opts.quantifiers.mbqiMode != options::MbqiMode::FMC))
+    if (!opts.quantifiers.fmfMbqiModeWasSetByUser
+        || (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE
+            && opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::FMC))
     {
       // if bounded integers are set, use no MBQI by default
-      opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
+      opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE;
     }
     if (!opts.quantifiers.prenexQuantUserWasSetByUser)
     {
@@ -1432,9 +1432,9 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
-    if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE)
+    if (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE)
     {
-      opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
+      opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE;
     }
     if (!opts.quantifiers.hoElimStoreAxWasSetByUser)
     {

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 503ee4c2c4b275f69faaa5effe92e613093fff5c..0304043e9af3d03cba437b93d8cb16650ef8abe9 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -646,7 +646,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
   FirstOrderModelFmc* fmfmc = static_cast<FirstOrderModelFmc*>(fm);
   if (effort == 0)
   {
-    if (options().quantifiers.mbqiMode == options::MbqiMode::NONE)
+    if (options().quantifiers.fmfMbqiMode == options::FmfMbqiMode::NONE)
     {
       // just exhaustive instantiate
       Node c = mkCondDefault(fmfmc, f);

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index b52f7178dac15866f36e8a06b212792186d1cd3b..34054e366c456f218d74167eedd6dea9ebd585d4 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -54,7 +54,7 @@ void QModelBuilder::finishInit()
 }
 
 bool QModelBuilder::optUseModel() {
-  return options().quantifiers.mbqiMode != options::MbqiMode::NONE
+  return options().quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE
          || options().quantifiers.fmfBound || options().strings.stringExp;
 }
 

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index a295c30059068afedc0e783b4d41e0949335f2e5..641ac836fdbf5b8f58c578e579559e3c8bd69ad9 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -219,11 +219,10 @@ int ModelEngine::checkModel(){
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
-  int e_max =
-      options().quantifiers.mbqiMode == options::MbqiMode::FMC
-          ? 2
-          : (options().quantifiers.mbqiMode == options::MbqiMode::TRUST ? 0
-                                                                        : 1);
+  options::FmfMbqiMode mode = options().quantifiers.fmfMbqiMode;
+  int e_max = mode == options::FmfMbqiMode::FMC
+                  ? 2
+                  : (mode == options::FmfMbqiMode::TRUST ? 0 : 1);
   for( int e=0; e<e_max; e++) {
     d_incompleteQuants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index c08815c43eda9c2abfa4b0b55748a478a316e660..06b3f318a71d33258d0777093a24f6285c29ecd4 100644 (file)
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -57,9 +57,6 @@ TermRegistry::TermRegistry(Env& env,
     d_sygusTdb.reset(new TermDbSygus(env, qs, d_ochecker.get()));
   }
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
-  Trace("quant-engine-debug")
-      << "Initialize model, mbqi : " << options().quantifiers.mbqiMode
-      << std::endl;
 }
 
 void TermRegistry::finishInit(FirstOrderModel* fm,

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0eaea7fe77690bcc19a3b6b8b86ccead2bbe2f3e..08d68a95ff480f0011cd1f37c328b85d88e146f1 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -63,16 +63,17 @@ QuantifiersEngine::QuantifiersEngine(
       d_quants_red(userContext()),
       d_numInstRoundsLemma(0)
 {
+  options::FmfMbqiMode mmode = options().quantifiers.fmfMbqiMode;
   Trace("quant-init-debug")
-      << "Initialize model engine, mbqi : " << options().quantifiers.mbqiMode
-      << " " << options().quantifiers.fmfBound << std::endl;
+      << "Initialize model engine, mbqi : " << mmode << " "
+      << options().quantifiers.fmfBound << std::endl;
   // Finite model finding requires specialized ways of building the model.
   // We require constructing the model here, since it is required for
   // initializing the CombinationEngine and the rest of quantifiers engine.
   if (options().quantifiers.fmfBound || options().strings.stringExp
       || (options().quantifiers.finiteModelFind
-          && (options().quantifiers.mbqiMode == options::MbqiMode::FMC
-              || options().quantifiers.mbqiMode == options::MbqiMode::TRUST)))
+          && (mmode == options::FmfMbqiMode::FMC
+              || mmode == options::FmfMbqiMode::TRUST)))
   {
     Trace("quant-init-debug") << "...make fmc builder." << std::endl;
     d_builder.reset(