Add option to send all instantiations in a bounded range (#8796)

There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index a4c33c946ad3d08076404f22cb7b2d64351e526c..2d6d74bb4700f629ac9efd63eba2bb40423c6103 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -659,6 +659,14 @@ name   = "Quantifiers"
   default    = "1000"
   help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
 
+[[option]]
+  name       = "fmfBoundBlast"
+  category   = "expert"
+  long       = "fmf-bound-blast"
+  type       = "bool"
+  default    = "false"
+  help       = "send all instantiations for bounded ranges in a single round"
+
 ### Conflict-based instantiation options
 
 [[option]]

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 6a419f08efbced22296fa1166d9fcf0929ccbe1b..7c66a3e9a2fc9ea8af39bb5a17eca60f621bf0f0 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -919,7 +919,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
       Trace("fmc-exh-debug") << std::endl;
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
-      if( !riter.isFinished() ){
+      if (!options().quantifiers.fmfBoundBlast && !riter.isFinished())
+      {
         if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0
             && riter.d_enum_type[index] == ENUM_CUSTOM)
         {