From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 21 May 2022 22:58:11 +0000 (-0500)
Subject: Add option to send all instantiations in a bounded range (#8796)
X-Git-Tag: cvc5-1.0.1~110
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aaf5d11d3506c5f946c6b6edec2240d0a5b484d0;p=cvc5.git

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 a4c33c946..2d6d74bb4 100644
--- 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 6a419f08e..7c66a3e9a 100644
--- 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)
         {