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.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 20376c0530667f506fe30d40f5736cd52ef9700e..45341a6a6bd777a903967d4504c179a02ccde74b 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -474,6 +474,14 @@ name   = "Quantifiers"
   default    = "true"
   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"

diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index cbe5a316afa5f6d9e4ffc205134d7869ed9c8475..a2a3baa0f60b5bb829be9075f8b8fddbe09b8f9f 100644 (file)
--- 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 c166d0c0ab4962ff17e953e568a481a4abf82157..951c2a94f9ebf2b9e54cee88faa229d9b35bc64d 100644 (file)
--- 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 0f82d83012d3f20ebbc87cf6c001ff912b7b1c09..157f0f64ba16eb22f2790a44d9e122a91c32bed2 100644 (file)
--- 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 95a396d518dc30e3669fcdb0ac50d5130b33f481..eddc7470b90b443a346f73cb9acfb034069b9996 100644 (file)
--- 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 1e7927dc091a746585743d7bd83f4494140ca73a..5f91a9488b0757f28e36b19195d92abc883898ed 100644 (file)
--- 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 01465c7ca790cb5694454a9a40535091b18dbec7..72126302f318f71d79ed28d20bf95b3f145ed003 100644 (file)
--- 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 31e5240df29df751565f880b9c1150fbdfbcc3e9..3d17099cb221cec8ef8ccd77ef425a951bcbecb0 100644 (file)
--- 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 4f20fae22cb77d0c262adf0a89f9a2ce6a7e9487..6214737ad19d2fa9cc49a83d052f6d9173bd42c4 100644 (file)
--- 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 482dbfaee8288cab77bd9e1ede429b76d2d8a90c..23b6d9708bd40f189dc0d5d166b1bc76f3f83611 100644 (file)
--- 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