1 files changed, 35 insertions, 31 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index da60561ad..59082b55f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -172,39 +172,37 @@ class QuantifiersEnginePrivate
   }
 };
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c,
-                                     context::UserContext* u,
-                                     TheoryEngine* te,
+QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
                                      ProofNodeManager* pnm)
     : d_te(te),
+      d_context(te->getSatContext()),
+      d_userContext(te->getUserContext()),
+      d_decManager(dm),
       d_masterEqualityEngine(nullptr),
-      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
+      d_eq_query(
+          new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
       d_qepr(nullptr),
       d_term_util(new quantifiers::TermUtil(this)),
       d_term_canon(new expr::TermCanonize),
-      d_term_db(new quantifiers::TermDb(c, u, this)),
+      d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
-      d_instantiate(new quantifiers::Instantiate(this, u, pnm)),
-      d_skolemize(new quantifiers::Skolemize(this, u)),
+      d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)),
+      d_skolemize(new quantifiers::Skolemize(this, d_userContext)),
       d_term_enum(new quantifiers::TermEnumeration),
-      d_conflict_c(c, false),
-      // d_quants(u),
-      d_quants_prereg(u),
-      d_quants_red(u),
-      d_lemmas_produced_c(u),
-      d_ierCounter_c(c),
-      // d_ierCounter(c),
-      // d_ierCounter_lc(c),
-      // d_ierCounterLastLc(c),
-      d_presolve(u, true),
-      d_presolve_in(u),
-      d_presolve_cache(u),
-      d_presolve_cache_wq(u),
-      d_presolve_cache_wic(u)
+      d_conflict_c(d_context, false),
+      d_quants_prereg(d_userContext),
+      d_quants_red(d_userContext),
+      d_lemmas_produced_c(d_userContext),
+      d_ierCounter_c(d_context),
+      d_presolve(d_userContext, true),
+      d_presolve_in(d_userContext),
+      d_presolve_cache(d_userContext),
+      d_presolve_cache_wq(d_userContext),
+      d_presolve_cache_wic(d_userContext)
 {
   // initialize the private utility
   d_private.reset(new QuantifiersEnginePrivate);
@@ -217,7 +215,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 
   if (options::sygus() || options::sygusInst())
   {
-    d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this));
   }
 
   d_util.push_back(d_instantiate.get());
@@ -245,7 +243,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 
   bool needsBuilder = false;
-  d_private->initialize(this, c, d_modules, needsBuilder);
+  d_private->initialize(this, d_context, d_modules, needsBuilder);
 
   if (d_private->d_rel_dom.get())
   {
@@ -261,16 +259,18 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, c, "FirstOrderModelFmc"));
-      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
+          this, d_context, "FirstOrderModelFmc"));
+      d_builder.reset(
+          new quantifiers::fmcheck::FullModelChecker(d_context, this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(
-          new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(c, this));
+          new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(d_context, this));
     }
   }else{
-    d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
+    d_model.reset(
+        new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
   }
 }
 
@@ -281,14 +281,18 @@ void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
   d_masterEqualityEngine = mee;
 }
 
-context::Context* QuantifiersEngine::getSatContext()
+TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
+
+DecisionManager* QuantifiersEngine::getDecisionManager()
 {
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
+  return &d_decManager;
 }
 
+context::Context* QuantifiersEngine::getSatContext() { return d_context; }
+
 context::UserContext* QuantifiersEngine::getUserContext()
 {
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext();
+  return d_userContext;
 }
 
 OutputChannel& QuantifiersEngine::getOutputChannel()