Reorganizing initialization of term registry in quantifiers (#6127)

This is in preparation for moving several utilities into the quantifiers inference manager.

This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine.

15 files changed, 71 insertions, 33 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 953693f59..17cbba7ea 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 257684704..4470e5bf4 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quant_relevance.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "util/random.h"
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 62a63a2d5..3940370cf 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index ac59a852e..456a7a8fc 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -13,8 +13,10 @@
  **/
 
 #include "theory/quantifiers/relevant_domain.h"
+
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index fa90d699a..50c522d95 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -47,9 +47,8 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
   return os;
 }
 
-TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim)
+TermDbSygus::TermDbSygus(QuantifiersState& qs)
     : d_qstate(qs),
-      d_qim(qim),
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
       d_eval(new Evaluator),
@@ -60,6 +59,8 @@ TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim)
   d_false = NodeManager::currentNM()->mkConst( false );
 }
 
+void TermDbSygus::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; }
+
 bool TermDbSygus::reset( Theory::Effort e ) { 
   return true;  
 }
@@ -565,8 +566,8 @@ void TermDbSygus::registerEnumerator(Node e,
     ag = d_qstate.getValuation().ensureLiteral(ag);
     // must ensure that it is asserted as a literal before we begin solving
     Node lem = nm->mkNode(OR, ag, ag.negate());
-    d_qim.requirePhase(ag, true);
-    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT);
+    d_qim->requirePhase(ag, true);
+    d_qim->lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT);
     d_enum_to_active_guard[e] = ag;
   }
 }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index b313846b9..f2188469e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -54,8 +54,10 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
-  TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim);
+  TermDbSygus(QuantifiersState& qs);
   ~TermDbSygus() {}
+  /** Finish init, which sets the inference manager */
+  void finishInit(QuantifiersInferenceManager* qim);
   /** Reset this utility */
   bool reset(Theory::Effort e);
   /** Identify this utility */
@@ -316,8 +318,8 @@ class TermDbSygus {
  private:
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
-  QuantifiersInferenceManager& d_qim;
+  /** Pointer to the quantifiers inference manager */
+  QuantifiersInferenceManager* d_qim;
 
   //------------------------------utilities
   /** sygus explanation */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2d896c089..ca11d491d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -36,11 +37,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermDb::TermDb(QuantifiersState& qs,
-               QuantifiersInferenceManager& qim,
-               QuantifiersRegistry& qr)
+TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_qstate(qs),
-      d_qim(qim),
+      d_qim(nullptr),
       d_qreg(qr),
       d_termsContext(),
       d_termsContextUse(options::termDbCd() ? qs.getSatContext()
@@ -66,6 +65,8 @@ TermDb::~TermDb(){
 
 }
 
+void TermDb::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; }
+
 void TermDb::registerQuantifier( Node q ) {
   Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
   for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
@@ -437,7 +438,7 @@ void TermDb::computeUfTerms( TNode f ) {
             }
             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
           }
-          d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
+          d_qim->addPendingLemma(lem, InferenceId::UNKNOWN);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return;
@@ -1047,7 +1048,7 @@ bool TermDb::reset( Theory::Effort effort ){
           // equality is sent out as a lemma here.
           Trace("term-db-lemma")
               << "Purify equality lemma: " << eq << std::endl;
-          d_qim.addPendingLemma(eq, InferenceId::UNKNOWN);
+          d_qim->addPendingLemma(eq, InferenceId::UNKNOWN);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return false;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 61754ac32..6506a6123 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -78,9 +78,10 @@ class TermDb : public QuantifiersUtil {
 
  public:
   TermDb(QuantifiersState& qs,
-         QuantifiersInferenceManager& qim,
          QuantifiersRegistry& qr);
   ~TermDb();
+  /** Finish init, which sets the inference manager */
+  void finishInit(QuantifiersInferenceManager* qim);
   /** presolve (called once per user check-sat) */
   void presolve();
   /** reset (calculate which terms are active) */
@@ -294,8 +295,8 @@ class TermDb : public QuantifiersUtil {
  private:
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
-  QuantifiersInferenceManager& d_qim;
+  /** Pointer to the quantifiers inference manager */
+  QuantifiersInferenceManager* d_qim;
   /** The quantifiers registry */
   QuantifiersRegistry& d_qreg;
   /** A context for the data structures below, when not context-dependent */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 1377ad23d..d23ff060a 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -22,19 +22,26 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermRegistry::TermRegistry(QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim,
-                           QuantifiersRegistry& qr)
+TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
-      d_termDb(new TermDb(qs, qim, qr)),
+      d_termDb(new TermDb(qs, qr)),
       d_sygusTdb(nullptr)
 {
   if (options::sygus() || options::sygusInst())
   {
     // must be constructed here since it is required for datatypes finistInit
-    d_sygusTdb.reset(new TermDbSygus(qs, qim));
+    d_sygusTdb.reset(new TermDbSygus(qs));
+  }
+}
+
+void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
+{
+  d_termDb->finishInit(qim);
+  if (d_sygusTdb.get())
+  {
+    d_sygusTdb->finishInit(qim);
   }
 }
 
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 624787285..1d9058603 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -39,8 +39,9 @@ class TermRegistry
 
  public:
   TermRegistry(QuantifiersState& qs,
-               QuantifiersInferenceManager& qim,
                QuantifiersRegistry& qr);
+  /** Finish init, which sets the inference manager on modules of this class */
+  void finishInit(QuantifiersInferenceManager* qim);
   /** Presolve */
   void presolve();
 
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index 1466e1026..190e51c54 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/index_trie.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5802e1abc..e054fd309 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -44,9 +44,18 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
                                      ProofNodeManager* pnm)
     : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
       d_qstate(c, u, valuation, logicInfo),
+      d_qreg(),
+      d_treg(d_qstate, d_qreg),
       d_qim(*this, d_qstate, pnm),
-      d_qengine(d_qstate, d_qim, pnm)
+      d_qengine(d_qstate, d_qreg, d_treg, d_qim, pnm)
 {
+  // Finish initializing the term registry by hooking it up to the inference
+  // manager. This is required due to a cyclic dependency between the term
+  // database and the instantiate module. Term database needs inference manager
+  // since it sends out lemmas when term indexing is inconsistent, instantiate
+  // needs term database for entailment checks.
+  d_treg.finishInit(&d_qim);
+
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute("qid", this);
   out.handleUserAttribute( "quant-inst-max-level", this );
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 8b85a1bf6..e9785fcea 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -22,8 +22,10 @@
 #include "expr/node.h"
 #include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory.h"
 #include "theory/valuation.h"
@@ -84,6 +86,10 @@ class TheoryQuantifiers : public Theory {
   QuantifiersProofRuleChecker d_qChecker;
   /** The quantifiers state */
   QuantifiersState d_qstate;
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry d_qreg;
+  /** The term registry */
+  quantifiers::TermRegistry d_treg;
   /** The quantifiers inference manager */
   QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 24919fae0..c41fa36e6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -26,17 +26,17 @@
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_modules.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 
@@ -48,6 +48,8 @@ namespace theory {
 
 QuantifiersEngine::QuantifiersEngine(
     quantifiers::QuantifiersState& qstate,
+    quantifiers::QuantifiersRegistry& qr,
+    quantifiers::TermRegistry& tr,
     quantifiers::QuantifiersInferenceManager& qim,
     ProofNodeManager* pnm)
     : d_qstate(qstate),
@@ -55,8 +57,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_te(nullptr),
       d_decManager(nullptr),
       d_pnm(pnm),
-      d_qreg(),
-      d_treg(qstate, qim, d_qreg),
+      d_qreg(qr),
+      d_treg(tr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 91c21a650..c7c716105 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -24,8 +24,6 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/term_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -49,10 +47,12 @@ class QModelBuilder;
 class QuantifiersInferenceManager;
 class QuantifiersModules;
 class QuantifiersState;
+class QuantifiersRegistry;
 class Skolemize;
 class TermDb;
 class TermDbSygus;
 class TermEnumeration;
+class TermRegistry;
 }
 
 // TODO: organize this more/review this, github issue #1163
@@ -65,6 +65,8 @@ class QuantifiersEngine {
 
  public:
   QuantifiersEngine(quantifiers::QuantifiersState& qstate,
+                    quantifiers::QuantifiersRegistry& qr,
+                    quantifiers::TermRegistry& tr,
                     quantifiers::QuantifiersInferenceManager& qim,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
@@ -270,9 +272,9 @@ public:
   std::vector<QuantifiersModule*> d_modules;
   //------------- quantifiers utilities
   /** The quantifiers registry */
-  quantifiers::QuantifiersRegistry d_qreg;
+  quantifiers::QuantifiersRegistry& d_qreg;
   /** The term registry */
-  quantifiers::TermRegistry d_treg;
+  quantifiers::TermRegistry& d_treg;
   /** all triggers will be stored in this trie */
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */