From 6a761852b93510bf707e7002ad663ca0f36ad720 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 17 Feb 2020 13:29:09 -0600
Subject: [PATCH] Option to limit the number of rounds of enumerative
 instantiation (#3760)

---
 src/options/quantifiers_options.toml          | 15 ++++++--
 .../quantifiers/inst_strategy_enumerative.cpp | 34 +++++++++++++------
 .../quantifiers/inst_strategy_enumerative.h   |  8 +++++
 .../regress1/quantifiers/issue3481.smt2       |  2 +-
 4 files changed, 45 insertions(+), 14 deletions(-)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 84545e66e..cb989b433 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -545,7 +545,7 @@ header = "options/quantifiers_options.h"
   long       = "full-saturate-quant"
   type       = "bool"
   default    = "false"
-  help       = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
+  help       = "enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
 
 [[option]]
   name       = "fullSaturateQuantRd"
@@ -554,8 +554,17 @@ header = "options/quantifiers_options.h"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "whether to use relevant domain first for full saturation instantiation strategy"
+  help       = "whether to use relevant domain first for enumerative instantiation strategy"
 
+[[option]]
+  name       = "fullSaturateLimit"
+  category   = "regular"
+  long       = "full-saturate-quant-limit=N"
+  type       = "int"
+  default    = "-1"
+  read_only  = true
+  help       = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)"
+  
 [[option]]
   name       = "fullSaturateInterleave"
   category   = "regular"
@@ -563,7 +572,7 @@ header = "options/quantifiers_options.h"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "interleave full saturate instantiation with other techniques"
+  help       = "interleave enumerative instantiation with other techniques"
 
 [[option]]
   name       = "fullSaturateStratify"
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)
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 48285c877..4d98f00ef 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -64,6 +64,8 @@ class InstStrategyEnum : public QuantifiersModule
  public:
   InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd);
   ~InstStrategyEnum() {}
+  /** Presolve */
+  void presolve() override;
   /** Needs check. */
   bool needsCheck(Theory::Effort e) override;
   /** Reset round. */
@@ -101,6 +103,12 @@ class InstStrategyEnum : public QuantifiersModule
    * term instantiations.
    */
   bool process(Node q, bool fullEffort, bool isRd);
+  /**
+   * A limit on the number of rounds to apply this strategy, where a value < 0
+   * means no limit. This value is set to the value of fullSaturateLimit()
+   * during presolve.
+   */
+  int32_t d_fullSaturateLimit;
 }; /* class InstStrategyEnum */
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2
index 47d2bcbe4..fe8c84d62 100644
--- a/test/regress/regress1/quantifiers/issue3481.smt2
+++ b/test/regress/regress1/quantifiers/issue3481.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --full-saturate-quant
+; COMMAND-LINE: --full-saturate-quant --full-saturate-quant-limit=2
 ; EXPECT: unsat
 
 ;; produced by cvc4_16.drv ;;
-- 
2.30.2