Moving instantiate and skolemize into quantifiers inference manager (#6188)

After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.

8 files changed, 101 insertions, 68 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index be6101b81..fd74e17e8 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.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/quantifiers_engine.h"
 #include "theory/rewriter.h"
@@ -40,17 +41,18 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Instantiate::Instantiate(QuantifiersEngine* qe,
-                         QuantifiersState& qs,
+Instantiate::Instantiate(QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
+                         TermRegistry& tr,
+                         FirstOrderModel* m,
                          ProofNodeManager* pnm)
-    : d_qe(qe),
-      d_qstate(qs),
+    : d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
+      d_treg(tr),
+      d_model(m),
       d_pnm(pnm),
-      d_term_db(nullptr),
       d_total_inst_debug(qs.getUserContext()),
       d_c_inst_match_trie_dom(qs.getUserContext()),
       d_pfInst(pnm ? new CDProof(pnm) : nullptr)
@@ -79,7 +81,6 @@ bool Instantiate::reset(Theory::Effort e)
     }
     d_recorded_inst.clear();
   }
-  d_term_db = d_qe->getTermDatabase();
   return true;
 }
 
@@ -111,7 +112,6 @@ bool Instantiate::addInstantiation(Node q,
   d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
   Assert(!d_qstate.isInConflict());
   Assert(terms.size() == q[0].getNumChildren());
-  Assert(d_term_db != nullptr);
   Trace("inst-add-debug") << "For quantified formula " << q
                           << ", add instantiation: " << std::endl;
   for (unsigned i = 0, size = terms.size(); i < size; i++)
@@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       // pick the best possible representative for instantiation, based on past
       // use and simplicity of term
-      terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i);
+      terms[i] = d_model->getInternalRepresentative(terms[i], q, i);
     }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if (terms[i].isNull())
@@ -188,6 +188,7 @@ bool Instantiate::addInstantiation(Node q,
 #endif
   }
 
+  TermDb* tdb = d_treg.getTermDatabase();
   // Note we check for entailment before checking for term vector duplication.
   // Although checking for term vector duplication is a faster check, it is
   // included automatically with recordInstantiationInternal, hence we prefer
@@ -210,7 +211,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       subs[q[0][i]] = terms[i];
     }
-    if (d_term_db->isEntailed(q[1], subs, false, true))
+    if (tdb->isEntailed(q[1], subs, false, true))
     {
       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
       ++(d_statistics.d_inst_duplicate_ent);
@@ -223,7 +224,7 @@ bool Instantiate::addInstantiation(Node q,
   {
     for (Node& t : terms)
     {
-      if (!d_term_db->isTermEligibleForInstantiation(t, q))
+      if (!tdb->isTermEligibleForInstantiation(t, q))
       {
         return false;
       }
@@ -408,6 +409,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     // will never succeed with 1 variable
     return false;
   }
+  TermDb* tdb = d_treg.getTermDatabase();
   Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
   // set up information for below
   std::vector<Node>& vars = d_qreg.d_vars[q];
@@ -441,7 +443,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     if (options::instNoEntail())
     {
       Trace("inst-exp-fail") << "  check entailment" << std::endl;
-      success = d_term_db->isEntailed(q[1], subs, false, true);
+      success = tdb->isEntailed(q[1], subs, false, true);
       Trace("inst-exp-fail") << "  entailed: " << success << std::endl;
     }
     // check whether the instantiation rewrites to the same thing
@@ -615,9 +617,9 @@ Node Instantiate::getTermForType(TypeNode tn)
 {
   if (tn.isClosedEnumerable())
   {
-    return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+    return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
   }
-  return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+  return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn);
 }
 
 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
@@ -704,7 +706,7 @@ void Instantiate::debugPrint(std::ostream& out)
     for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
     {
       Node name;
-      if (!d_qe->getNameForQuant(i.first, name, req))
+      if (!d_qreg.getNameForQuant(i.first, name, req))
       {
         continue;
       }
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index abdee69ef..8e556b648 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -32,15 +32,13 @@ namespace CVC4 {
 class LazyCDProof;
 
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
-class TermDb;
+class TermRegistry;
 class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
+class FirstOrderModel;
 
 /** Instantiation rewriter
  *
@@ -95,10 +93,11 @@ class Instantiate : public QuantifiersUtil
   typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
 
  public:
-  Instantiate(QuantifiersEngine* qe,
-              QuantifiersState& qs,
+  Instantiate(QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
+              TermRegistry& tr,
+              FirstOrderModel* m,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -311,18 +310,18 @@ class Instantiate : public QuantifiersUtil
    */
   static Node ensureType(Node n, TypeNode tn);
 
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** The quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
+  /** Pointer to the model */
+  FirstOrderModel* d_model;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
-  /** cache of term database for quantifiers engine */
-  TermDb* d_term_db;
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 8469720c4..9a82265f9 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -14,18 +14,38 @@
 
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/skolemize.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 QuantifiersInferenceManager::QuantifiersInferenceManager(
-    Theory& t, QuantifiersState& state, ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers")
+    Theory& t,
+    QuantifiersState& state,
+    QuantifiersRegistry& qr,
+    TermRegistry& tr,
+    FirstOrderModel* m,
+    ProofNodeManager* pnm)
+    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
+      d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)),
+      d_skolemize(new Skolemize(state, pnm))
 {
 }
 
 QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
 
+Instantiate* QuantifiersInferenceManager::getInstantiate()
+{
+  return d_instantiate.get();
+}
+
+Skolemize* QuantifiersInferenceManager::getSkolemize()
+{
+  return d_skolemize.get();
+}
+
 void QuantifiersInferenceManager::doPending()
 {
   doPendingLemmas();
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index 76b7d0982..aa7fc1b6a 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -24,6 +24,11 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class Instantiate;
+class Skolemize;
+class QuantifiersRegistry;
+class TermRegistry;
+class FirstOrderModel;
 /**
  * The quantifiers inference manager.
  */
@@ -32,12 +37,25 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
  public:
   QuantifiersInferenceManager(Theory& t,
                               QuantifiersState& state,
+                              QuantifiersRegistry& qr,
+                              TermRegistry& tr,
+                              FirstOrderModel* m,
                               ProofNodeManager* pnm);
   ~QuantifiersInferenceManager();
+  /** get instantiate utility */
+  Instantiate* getInstantiate();
+  /** get skolemize utility */
+  Skolemize* getSkolemize();
   /**
    * Do all pending lemmas, then do all pending phase requirements.
    */
   void doPending();
+
+ private:
+  /** instantiate utility */
+  std::unique_ptr<Instantiate> d_instantiate;
+  /** skolemize utility */
+  std::unique_ptr<Skolemize> d_skolemize;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5bcc80eb0..092689b5f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -41,15 +41,9 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
       d_qstate(c, u, valuation, logicInfo),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
-      d_qim(*this, d_qstate, pnm)
+      d_qim(nullptr),
+      d_qengine(nullptr)
 {
-  // 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 );
@@ -62,10 +56,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
     // add the proof rules
     d_qChecker.registerTo(pc);
   }
-  // indicate we are using the quantifiers theory state object
-  d_theoryState = &d_qstate;
-  // use the inference manager as the official inference manager
-  d_inferManager = &d_qim;
 
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug")
@@ -73,18 +63,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   // Finite model finding requires specialized ways of building the model.
   // We require constructing the model here, since it is required for
   // initializing the CombinationEngine and the rest of quantifiers engine.
-  if (options::finiteModelFind() || options::fmfBound())
+  if ((options::finiteModelFind() || options::fmfBound())
+      && QuantifiersModules::useFmcModel())
   {
-    if (QuantifiersModules::useFmcModel())
-    {
-      d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
-    }
-    else
-    {
-      d_qmodel.reset(new quantifiers::FirstOrderModel(
-          d_qstate, d_qreg, d_treg, "FirstOrderModel"));
-    }
+    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+        d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
   }
   else
   {
@@ -92,13 +75,27 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
         d_qstate, d_qreg, d_treg, "FirstOrderModel"));
   }
 
+  d_qim.reset(new QuantifiersInferenceManager(
+      *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), 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.get());
+
   // construct the quantifiers engine
   d_qengine.reset(new QuantifiersEngine(
-      d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm));
+      d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm));
 
   //!!!!!!!!!!!!!! temporary (project #15)
   d_qmodel->finishInit(d_qengine.get());
 
+  // indicate we are using the quantifiers theory state object
+  d_theoryState = &d_qstate;
+  // use the inference manager as the official inference manager
+  d_inferManager = d_qim.get();
   // Set the pointer to the quantifiers engine, which this theory owns. This
   // pointer will be retreived by TheoryEngine and set to all theories
   // post-construction.
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 9714ec718..2371b00ce 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -94,7 +94,7 @@ class TheoryQuantifiers : public Theory {
   /** The term registry */
   TermRegistry d_treg;
   /** The quantifiers inference manager */
-  QuantifiersInferenceManager d_qim;
+  std::unique_ptr<QuantifiersInferenceManager> d_qim;
   /** The quantifiers engine, which lives here */
   std::unique_ptr<QuantifiersEngine> d_qengine;
 };/* class TheoryQuantifiers */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 68962de72..9ca8226bc 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,9 +62,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_treg(tr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(qm),
-      d_instantiate(
-          new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
-      d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext())
 {
@@ -73,7 +70,7 @@ QuantifiersEngine::QuantifiersEngine(
   // quantifiers registry must come before the remaining utilities
   d_util.push_back(&d_qreg);
   d_util.push_back(tr.getTermDatabase());
-  d_util.push_back(d_instantiate.get());
+  d_util.push_back(qim.getInstantiate());
 }
 
 QuantifiersEngine::~QuantifiersEngine() {}
@@ -125,6 +122,9 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
 {
   return d_model;
 }
+
+/// !!!!!!!!!!!!!! temporary (project #15)
+
 quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 {
   return d_treg.getTermDatabase();
@@ -139,16 +139,17 @@ quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
 }
 quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
 {
-  return d_instantiate.get();
+  return d_qim.getInstantiate();
 }
 quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
 {
-  return d_skolemize.get();
+  return d_qim.getSkolemize();
 }
 inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
 {
   return d_tr_trie.get();
 }
+/// !!!!!!!!!!!!!!
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
@@ -468,7 +469,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       {
         Options& sopts = smt::currentSmtEngine()->getOptions();
         std::ostream& out = *sopts.getOut();
-        d_instantiate->debugPrint(out);
+        d_qim.getInstantiate()->debugPrint(out);
       }
     }
     if( Trace.isOn("quant-engine") ){
@@ -491,7 +492,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       d_qim.setIncomplete();
     }
     //output debug stats
-    d_instantiate->debugPrintModel();
+    d_qim.getInstantiate()->debugPrintModel();
   }
 }
 
@@ -611,7 +612,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   }
   if( !pol ){
     // do skolemization
-    TrustNode lem = d_skolemize->process(f);
+    TrustNode lem = d_qim.getSkolemize()->process(f);
     if (!lem.isNull())
     {
       if (Trace.isOn("quantifiers-sk-debug"))
@@ -645,11 +646,11 @@ void QuantifiersEngine::markRelevant( Node q ) {
 }
 
 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
-  d_instantiate->getInstantiationTermVectors(q, tvecs);
+  d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs);
 }
 
 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
-  d_instantiate->getInstantiationTermVectors(insts);
+  d_qim.getInstantiate()->getInstantiationTermVectors(insts);
 }
 
 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
@@ -663,13 +664,13 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
 
 void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
-  d_instantiate->getInstantiatedQuantifiedFormulas(qs);
+  d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
 }
 
 void QuantifiersEngine::getSkolemTermVectors(
     std::map<Node, std::vector<Node> >& sks) const
 {
-  d_skolemize->getSkolemTermVectors(sks);
+  d_qim.getSkolemize()->getSkolemTermVectors(sks);
 }
 
 QuantifiersEngine::Statistics::Statistics()
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4d3029ca9..b6562caa7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -237,10 +237,6 @@ public:
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** instantiate utility */
-  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
-  /** skolemize utility */
-  std::unique_ptr<quantifiers::Skolemize> d_skolemize;
   //------------- end quantifiers utilities
   /**
    * The modules utility, which contains all of the quantifiers modules.