Option to limit the number of rounds of enumerative instantiation (#3760)

1 files changed, 24 insertions, 10 deletions

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 83856dfc4..1e2e34aa2 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -33,12 +33,19 @@ using namespace inst;
 namespace quantifiers {
 
 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd)
-    : QuantifiersModule(qe), d_rd(rd)
+    : QuantifiersModule(qe), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
-
+void InstStrategyEnum::presolve()
+{
+  d_fullSaturateLimit = options::fullSaturateLimit();
+}
 bool InstStrategyEnum::needsCheck(Theory::Effort e)
 {
+  if (d_fullSaturateLimit == 0)
+  {
+    return false;
+  }
   if (options::fullSaturateInterleave())
   {
     if (d_quantEngine->getInstWhenNeedsCheck(e))
@@ -61,15 +68,18 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
 {
   bool doCheck = false;
   bool fullEffort = false;
-  if (options::fullSaturateInterleave())
+  if (d_fullSaturateLimit != 0)
   {
-    // we only add when interleaved with other strategies
-    doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
-  }
-  if (options::fullSaturateQuant() && !doCheck)
-  {
-    doCheck = quant_e == QEFFORT_LAST_CALL;
-    fullEffort = !d_quantEngine->hasAddedLemma();
+    if (options::fullSaturateInterleave())
+    {
+      // we only add when interleaved with other strategies
+      doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+    }
+    if (options::fullSaturateQuant() && !doCheck)
+    {
+      doCheck = quant_e == QEFFORT_LAST_CALL;
+      fullEffort = !d_quantEngine->hasAddedLemma();
+    }
   }
   if (!doCheck)
   {
@@ -150,6 +160,10 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
     Trace("fs-engine") << "Finished full saturation engine, time = "
                        << (clSet2 - clSet) << std::endl;
   }
+  if (d_fullSaturateLimit > 0)
+  {
+    d_fullSaturateLimit--;
+  }
 }
 
 bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)