From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 24 Mar 2021 22:44:52 +0000 (-0500)
Subject: Use inference manager to access intantiate utility instead of quantifiers engine... 
X-Git-Tag: cvc5-1.0.0~2033
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77b75a69e51b742e1448d754b6886c10ef76e79f;p=cvc5.git

Use inference manager to access intantiate utility instead of quantifiers engine (#6198)

Towards breaking dependencies on quantifers engine.
---

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index dcc0e885b..2c0fba7a6 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -471,32 +471,29 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
 
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert(!d_curr_quant.isNull());
+  Instantiate* inst = d_qim.getInstantiate();
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
   if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
   {
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->getInstantiate()->recordInstantiation(
-        d_curr_quant, subs, false, false);
+    inst->recordInstantiation(d_curr_quant, subs, false, false);
     return true;
-  }else{
-    //check if we need virtual term substitution (if used delta or infinity)
-    bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
-    if (d_quantEngine->getInstantiate()->addInstantiation(
-            d_curr_quant,
-            subs,
-            InferenceId::QUANTIFIERS_INST_CEGQI,
-            false,
-            false,
-            used_vts))
-    {
-      return true;
-    }else{
-      //this should never happen for monotonic selection strategies
-      Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
-      return false;
-    }
   }
+  // check if we need virtual term substitution (if used delta or infinity)
+  bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
+  if (inst->addInstantiation(d_curr_quant,
+                             subs,
+                             InferenceId::QUANTIFIERS_INST_CEGQI,
+                             false,
+                             false,
+                             used_vts))
+  {
+    return true;
+  }
+  // this should never happen for monotonic selection strategies
+  Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
+  return false;
 }
 
 bool InstStrategyCegqi::addPendingLemma(Node lem) const
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f1ed9fe00..04ab464f8 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/skolemize.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"
@@ -602,7 +603,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
           //check each skolem variable
           bool disproven = true;
           std::vector<Node> skolems;
-          d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems);
+          d_qim.getSkolemize()->getSkolemConstants(q, skolems);
           Trace("sg-conjecture") << "    CONJECTURE : ";
           std::vector< Node > ce;
           for (unsigned j = 0; j < skolems.size(); j++)
@@ -1102,7 +1103,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
   if( n.getNumChildren()>0 ){
     Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
                               << ")" << std::endl;
-    TermEnumeration* te = d_quantEngine->getTermEnumeration();
+    TermEnumeration* te = d_quantEngine->getTermRegistry().getTermEnumeration();
     // below, we do a fair enumeration of vectors vec of indices whose sum is
     // 1,2,3, ...
     std::vector< int > vec;
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 6206b24a7..4cdce940e 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
@@ -236,7 +237,6 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
-    QuantifiersState& qs = d_quantEngine->getState();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -288,9 +288,9 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
           }
           else if (!itf->second.isNull())
           {
-            if (!qs.areEqual(itf->second, args[k]))
+            if (!d_qstate.areEqual(itf->second, args[k]))
             {
-              if (!d_quantEngine->getTermDatabase()->isEntailed(
+              if (!d_treg.getTermDatabase()->isEntailed(
                       itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
@@ -323,7 +323,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
         {
           if (!itf->second.isNull())
           {
-            Node r = qs.getRepresentative(itf->second);
+            Node r = d_qstate.getRepresentative(itf->second);
             std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
             if (itfr != arg_to_rep.end())
             {
@@ -375,7 +375,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+    return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
   }
 }
 
@@ -389,7 +389,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->getInstantiate()->addInstantiation(
+    return d_qim.getInstantiate()->addInstantiation(
         d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
   }
   else
@@ -476,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
   Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
   uint64_t numLemmas = 0;
   // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
-  TermDb* tdb = d_quantEngine->getTermDatabase();
+  TermDb* tdb = d_treg.getTermDatabase();
   unsigned size = tdb->getNumOperators();
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned j = 0; j < size; j++)
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index 0d0f9498d..efc65cdef 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -36,22 +36,22 @@ namespace inst {
 class Trigger;
 
 /** IMGenerator class
-*
-* Virtual base class for generating InstMatch objects, which correspond to
-* quantifier instantiations. The main use of this class is as a backend utility
-* to Trigger (see theory/quantifiers/ematching/trigger.h).
-*
-* Some functions below take as argument a pointer to the current quantifiers
-* engine, which is used for making various queries about what terms and
-* equalities exist in the current context.
-*
-* Some functions below take a pointer to a parent Trigger object, which is used
-* to post-process and finalize the instantiations through
-* sendInstantiation(...), where the parent trigger will make calls to
-* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
-* point in which instantiate lemmas are enqueued to be sent on the output
-* channel.
-*/
+ *
+ * Virtual base class for generating InstMatch objects, which correspond to
+ * quantifier instantiations. The main use of this class is as a backend utility
+ * to Trigger (see theory/quantifiers/ematching/trigger.h).
+ *
+ * Some functions below take as argument a pointer to the current quantifiers
+ * engine, which is used for making various queries about what terms and
+ * equalities exist in the current context.
+ *
+ * Some functions below take a pointer to a parent Trigger object, which is used
+ * to post-process and finalize the instantiations through
+ * sendInstantiation(...), where the parent trigger will make calls to
+ * Instantiate::addInstantiation(...). The latter function is the entry
+ * point in which instantiate lemmas are enqueued to be sent on the output
+ * channel.
+ */
 class IMGenerator {
 public:
  IMGenerator(Trigger* tparent);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index ad48d9c91..6ae2f915b 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -41,10 +41,6 @@ namespace inst {
  * The implementation traverses the term indices in TermDatabase for adding
  * instantiations, which is more efficient than the techniques required for
  * handling non-simple single triggers.
- *
- * In contrast to other instantiation generators, it does not call
- * IMGenerator::sendInstantiation and for performance reasons instead calls
- * qe->getInstantiate()->addInstantiation(...) directly.
  */
 class InstMatchGeneratorSimple : public IMGenerator
 {
@@ -88,12 +84,12 @@ class InstMatchGeneratorSimple : public IMGenerator
   std::map<size_t, int> d_var_num;
   /** add instantiations, helper function.
    *
-   * m is the current match we are building,
-   * addedLemmas is the number of lemmas we have added via calls to
-   *                qe->getInstantiate()->aaddInstantiation(...),
-   * argIndex is the argument index in d_match_pattern we are currently
-   *              matching,
-   * tat is the term index we are currently traversing.
+   * @param m the current match we are building,
+   * @param addedLemmas the number of lemmas we have added via calls to
+   * Instantiate::addInstantiation(...),
+   * @param argIndex the argument index in d_match_pattern we are currently
+   * matching,
+   * @param tat the term index we are currently traversing.
    */
   void addInstantiations(InstMatch& m,
                          uint64_t& addedLemmas,
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index af0a0bfbc..c93e1a99b 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -154,7 +154,7 @@ uint64_t Trigger::addInstantiations()
 
 bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+  return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
 }
 
 bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 2245e16dd..dd28af380 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -284,8 +284,9 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
 }
 
 FullModelChecker::FullModelChecker(QuantifiersState& qs,
-                                   QuantifiersRegistry& qr)
-    : QModelBuilder(qs, qr)
+                                   QuantifiersRegistry& qr,
+                                   QuantifiersInferenceManager& qim)
+    : QModelBuilder(qs, qr, qim)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -628,7 +629,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
     Trace("fmc") << std::endl;
 
     // consider all entries going to non-true
-    Instantiate* instq = d_qe->getInstantiate();
+    Instantiate* instq = d_qim.getInstantiate();
     for (unsigned i = 0, msize = mcond.size(); i < msize; i++)
     {
       if (d_quant_models[f].d_value[i] == d_true)
@@ -833,6 +834,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
     Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
     int addedLemmas = 0;
     //now do full iteration
+    Instantiate* ie = d_qim.getInstantiate();
     while( !riter.isFinished() ){
       d_triedLemmas++;
       Trace("fmc-exh-debug") << "Inst : ";
@@ -858,7 +860,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if (d_qe->getInstantiate()->addInstantiation(
+        if (ie->addInstantiation(
                 f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
         {
           Trace("fmc-exh-debug")  << " ...success.";
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 904a1b9a0..972c977e8 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -154,7 +154,9 @@ protected:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr);
+  FullModelChecker(QuantifiersState& qs,
+                   QuantifiersRegistry& qr,
+                   QuantifiersInferenceManager& qim);
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 9aa687fbd..a24f72e32 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,13 +30,15 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr)
+QModelBuilder::QModelBuilder(QuantifiersState& qs,
+                             QuantifiersRegistry& qr,
+                             QuantifiersInferenceManager& qim)
     : TheoryEngineModelBuilder(),
       d_addedLemmas(0),
       d_triedLemmas(0),
-      d_qe(nullptr),
       d_qstate(qs),
-      d_qreg(qr)
+      d_qreg(qr),
+      d_qim(qim)
 {
 }
 
@@ -96,6 +98,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
     int tests = 0;
     int bad = 0;
     QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
+    Instantiate* inst = d_qim.getInstantiate();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
       std::vector< Node > vars;
@@ -112,7 +115,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
           {
             terms.push_back( riter.getCurrentTerm( k ) );
           }
-          Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
+          Node n = inst->getInstantiation(f, vars, terms);
           Node val = fm->getValue( n );
           if (!val.isConst() || !val.getConst<bool>())
           {
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 7ba7a66e2..af5dee3cf 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -28,6 +28,7 @@ namespace quantifiers {
 class FirstOrderModel;
 class QuantifiersState;
 class QuantifiersRegistry;
+class QuantifiersInferenceManager;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
@@ -40,9 +41,9 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr);
-  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
-  void finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+  QModelBuilder(QuantifiersState& qs,
+                QuantifiersRegistry& qr,
+                QuantifiersInferenceManager& qim);
 
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
@@ -66,6 +67,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** The quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& d_qim;
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index eb7398f92..b05f25b5e 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -279,7 +279,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       if( !riter.isIncomplete() ){
         int triedLemmas = 0;
         int addedLemmas = 0;
-        Instantiate* inst = d_quantEngine->getInstantiate();
+        Instantiate* inst = d_qim.getInstantiate();
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index c14ce4ad3..c58bcc863 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -194,7 +194,7 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
       mkTermTupleEnumerator(quantifier, &ttec));
   std::vector<Node> terms;
   std::vector<bool> failMask;
-  Instantiate* ie = d_quantEngine->getInstantiate();
+  Instantiate* ie = d_qim.getInstantiate();
   for (enumerator->init(); enumerator->hasNext();)
   {
     if (d_qstate.isInConflict())
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 7bf7cc09b..62f15a6a6 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -37,7 +37,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {}
+QuantInfo::QuantInfo()
+    : d_unassigned_nvar(0), d_una_index(0), d_parent(nullptr), d_mg(nullptr)
+{
+}
 
 QuantInfo::~QuantInfo() {
   delete d_mg;
@@ -49,8 +52,14 @@ QuantInfo::~QuantInfo() {
   d_var_mg.clear();
 }
 
+QuantifiersInferenceManager& QuantInfo::getInferenceManager()
+{
+  Assert(d_parent != nullptr);
+  return d_parent->getInferenceManager();
+}
 
 void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
+  d_parent = p;
   d_q = q;
   d_extra_var.clear();
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
@@ -588,7 +597,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
       }
     }else{
       Node inst =
-          p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
+          getInferenceManager().getInstantiate()->getInstantiation(d_q, terms);
       inst = Rewriter::rewrite(inst);
       Node inst_eval = p->getTermDatabase()->evaluateTerm(
           inst, options::qcfTConstraint(), true);
@@ -2107,7 +2116,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
   }
   // try to make a matches making the body false or propagating
   Trace("qcf-check-debug") << "Get next match..." << std::endl;
-  Instantiate* qinst = d_quantEngine->getInstantiate();
+  Instantiate* qinst = d_qim.getInstantiate();
   while (qi->getNextMatch(this))
   {
     if (d_qstate.isInConflict())
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index fe9aa411b..5b54f8055 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -131,6 +131,8 @@ public:
 public:
   QuantInfo();
   ~QuantInfo();
+  /** Get quantifiers inference manager */
+  QuantifiersInferenceManager& getInferenceManager();
   std::vector< TNode > d_vars;
   std::vector< TypeNode > d_var_types;
   std::map< TNode, int > d_var_num;
@@ -143,6 +145,8 @@ public:
 
   typedef std::map< int, MatchGen * > VarMgMap;
  private:
+  /** The parent who owns this class */
+  QuantConflictFind* d_parent;
   MatchGen * d_mg;
   VarMgMap d_var_mg;
  public:
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index bb35d6d26..1a7697608 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -68,7 +68,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   {
     d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
     modules.push_back(d_i_cbqi.get());
-    qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
+    qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
   if (options::sygus())
   {
@@ -91,16 +91,14 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
     if (tr.useFmcModel())
     {
       Trace("quant-init-debug") << "...make fmc builder." << std::endl;
-      d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
+      d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
     }
     else
     {
       Trace("quant-init-debug")
           << "...make default model builder." << std::endl;
-      d_builder.reset(new QModelBuilder(qs, qr));
+      d_builder.reset(new QModelBuilder(qs, qr, qim));
     }
-    // !!!!!!!!!!!!! temporary (project #15)
-    d_builder->finishInit(qe);
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index f93260f0c..066bcd769 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.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"
@@ -348,7 +349,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index)
       ptn = ptn.getRangeType();
     }
     Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
-    s = d_qe->getTermEnumeration()->getEnumerateTerm(ptn, 0);
+    s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0);
   }
   else
   {
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 831216445..a0058f2d8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -178,7 +178,7 @@ void SynthConjecture::assign(Node q)
   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
                  << std::endl;
   // construct base instantiation
-  d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
+  d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation(
       d_embed_quant, vars, d_candidates));
   if (!d_embedSideCondition.isNull())
   {
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index bbc13b463..52a2787f7 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -246,7 +246,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
   if (quant_e != QEFFORT_STANDARD) return;
 
   FirstOrderModel* model = d_quantEngine->getModel();
-  Instantiate* inst = d_quantEngine->getInstantiate();
+  Instantiate* inst = d_qim.getInstantiate();
   TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
   SygusExplain syexplain(db);
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2cface166..0155eb05a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -112,6 +112,10 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
 {
   return d_qreg;
 }
+quantifiers::TermRegistry& QuantifiersEngine::getTermRegistry()
+{
+  return d_treg;
+}
 
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
@@ -124,26 +128,16 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
 
 /// !!!!!!!!!!!!!! temporary (project #15)
 
-quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
-{
-  return d_treg.getTermDatabase();
-}
 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
 {
   return d_treg.getTermDatabaseSygus();
 }
-quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
-{
-  return d_treg.getTermEnumeration();
-}
-quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
-{
-  return d_qim.getInstantiate();
-}
-quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
+
+quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 {
-  return d_qim.getSkolemize();
+  return d_treg.getTermDatabase();
 }
+
 quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
 {
   return d_tr_trie.get();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 1f1dcc950..cb60c8e88 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -80,22 +80,18 @@ class QuantifiersEngine {
   quantifiers::QuantifiersInferenceManager& getInferenceManager();
   /** The quantifiers registry */
   quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
+  /** The term registry */
+  quantifiers::TermRegistry& getTermRegistry();
   //---------------------- end external interface
   //---------------------- utilities
   /** get the model builder */
   quantifiers::QModelBuilder* getModelBuilder() const;
-  /** get model */
-  quantifiers::FirstOrderModel* getModel() const;
   /** get term database */
   quantifiers::TermDb* getTermDatabase() const;
+  /** get model */
+  quantifiers::FirstOrderModel* getModel() const;
   /** get term database sygus */
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
-  /** get term enumeration utility */
-  quantifiers::TermEnumeration* getTermEnumeration() const;
-  /** get instantiate utility */
-  quantifiers::Instantiate* getInstantiate() const;
-  /** get skolemize utility */
-  quantifiers::Skolemize* getSkolemize() const;
   /** get trigger database */
   quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities