Add option to limit the number of instantiation rounds (#6818)

This adds an option to limit the number of instantiation rounds used by quantifiers engine.

This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.

This PR also makes minor improvements to the quantifier utility infrastructure.

10 files changed, 65 insertions, 34 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 20376c053..45341a6a6 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -475,6 +475,14 @@ name   = "Quantifiers"
   help       = "only input terms are assigned instantiation level zero"
 
 [[option]]
+  name       = "instMaxRounds"
+  category   = "regular"
+  long       = "inst-max-rounds=N"
+  type       = "int"
+  default    = "-1"
+  help       = "maximum number of instantiation rounds (-1 == no limit, default)"
+
+[[option]]
   name       = "quantRepMode"
   category   = "regular"
   long       = "quant-rep-mode=MODE"
diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index cbe5a316a..a2a3baa0f 100644
--- a/src/theory/incomplete_id.cpp
+++ b/src/theory/incomplete_id.cpp
@@ -33,6 +33,8 @@ const char* toString(IncompleteId i)
     case IncompleteId::QUANTIFIERS_FMF: return "QUANTIFIERS_FMF";
     case IncompleteId::QUANTIFIERS_RECORDED_INST:
       return "QUANTIFIERS_RECORDED_INST";
+    case IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS:
+      return "QUANTIFIERS_MAX_INST_ROUNDS";
     case IncompleteId::SEP: return "SEP";
     case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD";
     case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index c166d0c0a..951c2a94f 100644
--- a/src/theory/incomplete_id.h
+++ b/src/theory/incomplete_id.h
@@ -42,6 +42,8 @@ enum class IncompleteId
   QUANTIFIERS_FMF,
   // incomplete due to explicitly recorded instantiations
   QUANTIFIERS_RECORDED_INST,
+  // incomplete due to limited number of allowed instantiation rounds
+  QUANTIFIERS_MAX_INST_ROUNDS,
   // incomplete due to separation logic
   SEP,
   // relations were used in combination with set cardinality constraints
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 0f82d8301..157f0f64b 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -23,6 +23,8 @@
 #include "proof/lazy_proof.h"
 #include "proof/proof_node_manager.h"
 #include "smt/logic_exception.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -71,6 +73,7 @@ bool Instantiate::reset(Theory::Effort e)
   Trace("inst-debug") << "Reset, effort " << e << std::endl;
   // clear explicitly recorded instantiations
   d_recordedInst.clear();
+  d_instDebugTemp.clear();
   return true;
 }
 
@@ -334,7 +337,7 @@ bool Instantiate::addInstantiation(Node q,
   InstLemmaList* ill = getOrMkInstLemmaList(q);
   ill->d_list.push_back(body);
   // add to temporary debug statistics (# inst on this round)
-  d_temp_inst_debug[q]++;
+  d_instDebugTemp[q]++;
   if (Trace.isOn("inst"))
   {
     Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
@@ -671,30 +674,35 @@ void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
 
 bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
 
-void Instantiate::debugPrint(std::ostream& out)
+void Instantiate::notifyEndRound()
 {
-  // debug information
-  if (Trace.isOn("inst-per-quant-round"))
+  bool debugInstTrace = Trace.isOn("inst-per-quant-round");
+  if (options::debugInst() || debugInstTrace)
   {
-    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
+    Options& sopts = smt::currentSmtEngine()->getOptions();
+    std::ostream& out = *sopts.base.out;
+    // debug information
+    if (debugInstTrace)
     {
-      Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
-                                    << std::endl;
-      d_temp_inst_debug[i.first] = 0;
+      for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
+      {
+        Trace("inst-per-quant-round")
+            << " * " << i.second << " for " << i.first << std::endl;
+      }
     }
-  }
-  if (options::debugInst())
-  {
-    bool req = !options::printInstFull();
-    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
+    if (options::debugInst())
     {
-      Node name;
-      if (!d_qreg.getNameForQuant(i.first, name, req))
+      bool req = !options::printInstFull();
+      for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
       {
-        continue;
+        Node name;
+        if (!d_qreg.getNameForQuant(i.first, name, req))
+        {
+          continue;
+        }
+        out << "(num-instantiations " << name << " " << i.second << ")"
+            << std::endl;
       }
-      out << "(num-instantiations " << name << " " << i.second << ")"
-          << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 95a396d51..eddc7470b 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -110,7 +110,6 @@ class Instantiate : public QuantifiersUtil
               TermRegistry& tr,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
-
   /** reset */
   bool reset(Theory::Effort e) override;
   /** register quantifier */
@@ -237,11 +236,11 @@ class Instantiate : public QuantifiersUtil
   //--------------------------------------end general utilities
 
   /**
-   * Debug print, called once per instantiation round. This prints
+   * Called once at the end of each instantiation round. This prints
    * instantiations added this round to trace inst-per-quant-round, if
    * applicable, and prints to out if the option debug-inst is enabled.
    */
-  void debugPrint(std::ostream& out);
+  void notifyEndRound();
   /** debug print model, called once, before we terminate with sat/unknown. */
   void debugPrintModel();
 
@@ -339,7 +338,7 @@ class Instantiate : public QuantifiersUtil
    */
   std::map<Node, std::vector<Node> > d_recordedInst;
   /** statistics for debugging total instantiations per quantifier per round */
-  std::map<Node, uint32_t> d_temp_inst_debug;
+  std::map<Node, uint32_t> d_instDebugTemp;
 
   /** list of all instantiations produced for each quantifier
    *
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 1e7927dc0..5f91a9488 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -38,6 +38,8 @@ class QuantifiersUtil {
 public:
   QuantifiersUtil(){}
   virtual ~QuantifiersUtil(){}
+  /**  Called at the beginning of check-sat call. */
+  virtual void presolve() {}
   /* reset
    * Called at the beginning of an instantiation round
    * Returns false if the reset failed. When reset fails, the utility should
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 01465c7ca..72126302f 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -79,7 +79,7 @@ class TermDb : public QuantifiersUtil {
   /** Finish init, which sets the inference manager */
   void finishInit(QuantifiersInferenceManager* qim);
   /** presolve (called once per user check-sat) */
-  void presolve();
+  void presolve() override;
   /** reset (calculate which terms are active) */
   bool reset(Theory::Effort effort) override;
   /** register quantified formula */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 31e5240df..3d17099cb 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -60,7 +60,6 @@ void TermRegistry::finishInit(FirstOrderModel* fm,
 
 void TermRegistry::presolve()
 {
-  d_termDb->presolve();
   d_presolve = false;
   // add all terms to database
   if (options::incrementalSolving() && !options::termDbCd())
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4f20fae22..6214737ad 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -58,7 +58,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_treg(tr),
       d_model(nullptr),
       d_quants_prereg(qs.getUserContext()),
-      d_quants_red(qs.getUserContext())
+      d_quants_red(qs.getUserContext()),
+      d_numInstRoundsLemma(0)
 {
   Trace("quant-init-debug")
       << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
@@ -145,9 +146,15 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
+  d_numInstRoundsLemma = 0;
   d_qim.clearPending();
-  for( unsigned i=0; i<d_modules.size(); i++ ){
-    d_modules[i]->presolve();
+  for (QuantifiersUtil*& u : d_util)
+  {
+    u->presolve();
+  }
+  for (QuantifiersModule*& mdl : d_modules)
+  {
+    mdl->presolve();
   }
   // presolve with term registry, which populates the term database based on
   // terms registered before presolve when in incremental mode
@@ -241,6 +248,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
   d_qim.reset();
   bool setIncomplete = false;
   IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS;
+  if (options::instMaxRounds() >= 0
+      && d_numInstRoundsLemma >= static_cast<uint32_t>(options::instMaxRounds()))
+  {
+    needsCheck = false;
+    setIncomplete = true;
+    setIncompleteId = IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS;
+  }
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
@@ -458,13 +472,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
     // debug print
     if (d_qim.hasSentLemma())
     {
-      bool debugInstTrace = Trace.isOn("inst-per-quant-round");
-      if (options::debugInst() || debugInstTrace)
-      {
-        Options& sopts = smt::currentSmtEngine()->getOptions();
-        std::ostream& out = *sopts.base.out;
-        d_qim.getInstantiate()->debugPrint(out);
-      }
+      d_qim.getInstantiate()->notifyEndRound();
+      d_numInstRoundsLemma++;
     }
     if( Trace.isOn("quant-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 482dbfaee..23b6d9708 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -206,6 +206,8 @@ public:
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map<Node, Node> d_quants_red_lem;
+  /** Number of rounds we have instantiated */
+  uint32_t d_numInstRoundsLemma;
 };/* class QuantifiersEngine */
 
 }  // namespace theory