From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jan 2021 18:43:50 +0000 (-0600)
Subject: Refactor quantifiers engine initialization (#5813)
X-Git-Tag: cvc5-1.0.0~2354
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca648afb2a7574991b1dc9817c1b8e2546548073;p=cvc5.git

Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
---

diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 531dd8d21..c91ba419b 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -84,9 +84,10 @@ QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() {
   }
 }
 
-QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
-    : QuantifiersModule(qe) {
-  d_sqc = new CDSkQuantCache(qe->getUserContext());
+QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe)
+{
+  d_sqc = new CDSkQuantCache(qs.getUserContext());
 }
 
 QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; }
@@ -160,7 +161,8 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
 bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
   Assert(!quants.empty());
   std::sort( quants.begin(), quants.end() );
-  if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){
+  if (d_sqc->add(d_qstate.getUserContext(), quants))
+  {
     //partition into connected components
     if( pconnected && quants.size()>1 ){
       Trace("anti-sk-debug") << "Partition into connected components..." << std::endl;
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 93834d7ce..21faa0361 100644
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -32,8 +32,8 @@ namespace theory {
 namespace quantifiers {
 
 class QuantAntiSkolem : public QuantifiersModule {
-public:
-  QuantAntiSkolem( QuantifiersEngine * qe );
+ public:
+  QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs);
   virtual ~QuantAntiSkolem();
 
   bool sendAntiSkolemizeLemma( std::vector< Node >& quants,
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 16c7476ab..539dc1474 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -49,12 +49,13 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
   return d_parent->rewriteInstantiation(q, terms, inst, doVts);
 }
 
-InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
-    : QuantifiersModule(qe),
+InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
+                                     QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
-      d_added_cbqi_lemma(qe->getUserContext()),
+      d_added_cbqi_lemma(qs.getUserContext()),
       d_vtsCache(new VtsTermCache(qe)),
       d_bv_invert(nullptr)
 {
@@ -68,7 +69,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
   }
   if (options::cegqiNestedQE())
   {
-    d_nestedQe.reset(new NestedQe(qe->getUserContext()));
+    d_nestedQe.reset(new NestedQe(qs.getUserContext()));
   }
 }
 
@@ -168,7 +169,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       d_dstrat[q].reset(
           new DecisionStrategySingleton("CexLiteral",
                                         ceLit,
-                                        d_quantEngine->getSatContext(),
+                                        d_qstate.getSatContext(),
                                         d_quantEngine->getValuation()));
       dlds = d_dstrat[q].get();
     }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 1860962c7..f98ea8549 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -69,7 +69,7 @@ class InstStrategyCegqi : public QuantifiersModule
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 
  public:
-  InstStrategyCegqi(QuantifiersEngine* qe);
+  InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs);
   ~InstStrategyCegqi();
 
   /** whether to do counterexample-guided instantiation for quantifier q */
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index e13902077..2b3bb807a 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,11 +86,12 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
 }
 
 ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
-                                         context::Context* c)
-    : QuantifiersModule(qe),
+                                         QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
       d_notify(*this),
-      d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
-      d_ee_conjectures(c),
+      d_uequalityEngine(
+          d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
+      d_ee_conjectures(qs.getSatContext()),
       d_conj_count(0),
       d_subs_confirmCount(0),
       d_subs_unkCount(0),
@@ -163,7 +164,7 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo
   if( eqc_i!=d_eqc_info.end() ){
     return eqc_i->second;
   }else if( doMake ){
-    EqcInfo* ei = new EqcInfo( d_quantEngine->getSatContext() );
+    EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
     d_eqc_info[n] = ei;
     return ei;
   }else{
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 0c8106ad5..79c6f3f29 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -433,8 +433,9 @@ private:  //information about ground equivalence classes
   bool d_hasAddedLemma;
   //flush the waiting conjectures
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
-public:
-  ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
+
+ public:
+  ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs);
   ~ConjectureGenerator();
 
   /* needs check */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 7eb5a1378..d4904ebe8 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -34,8 +34,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
-    : QuantifiersModule(qe),
+InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
+                                         QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 9304c84ae..f22da6ec1 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -48,7 +48,7 @@ class InstantiationEngine : public QuantifiersModule {
   void doInstantiationRound(Theory::Effort effort);
 
  public:
-  InstantiationEngine(QuantifiersEngine* qe);
+  InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs);
   ~InstantiationEngine();
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 0b4539d7a..3887c583b 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -33,8 +33,8 @@ namespace theory {
 namespace quantifiers {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
-    context::Context* c, QuantifiersEngine* qe)
-    : d_qe(qe), d_eqi_counter(c), d_reset_count(0)
+    QuantifiersState& qs, QuantifiersEngine* qe)
+    : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0)
 {
 }
 
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index b11dbe033..b82b9ae64 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -21,6 +21,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_state.h"
 
 namespace CVC4 {
 namespace theory {
@@ -43,7 +44,7 @@ namespace quantifiers {
 class EqualityQueryQuantifiersEngine : public EqualityQuery
 {
  public:
-  EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
+  EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
   bool reset(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index ba91960e1..8f587c09d 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -34,11 +34,11 @@ namespace theory {
 namespace quantifiers {
 
 FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
-                                 context::Context* c,
+                                 QuantifiersState& qs,
                                  std::string name)
-    : TheoryModel(c, name, true),
+    : TheoryModel(qs.getSatContext(), name, true),
       d_qe(qe),
-      d_forall_asserts(c),
+      d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {
 }
@@ -335,9 +335,11 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
   return n.getAttribute(ModelBasisArgAttribute());
 }
 
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(qe, c, name){
-
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
+                                       QuantifiersState& qs,
+                                       std::string name)
+    : FirstOrderModel(qe, qs, name)
+{
 }
 
 FirstOrderModelFmc::~FirstOrderModelFmc()
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index a26401dd1..e4236a95d 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,6 +19,7 @@
 
 #include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
 
@@ -54,7 +55,9 @@ typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 class FirstOrderModel : public TheoryModel
 {
  public:
-  FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
+  FirstOrderModel(QuantifiersEngine* qe,
+                  QuantifiersState& qs,
+                  std::string name);
 
   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
   /** assert quantifier */
@@ -198,7 +201,9 @@ class FirstOrderModelFmc : public FirstOrderModel
   void processInitializeModelForTerm(Node n) override;
 
  public:
-  FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
+  FirstOrderModelFmc(QuantifiersEngine* qe,
+                     QuantifiersState& qs,
+                     std::string name);
   ~FirstOrderModelFmc() override;
   FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
   // initialize the model
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 2d6af9a63..51f88ad44 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -84,8 +84,8 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   return lem;
 }
 
-BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe)
-    : QuantifiersModule(qe)
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe)
 {
 }
 
@@ -493,8 +493,8 @@ void BoundedIntegers::checkOwnership(Node f)
             d_ranges.push_back( r );
             d_rms[r].reset(
                 new IntRangeDecisionHeuristic(r,
-                                              d_quantEngine->getSatContext(),
-                                              d_quantEngine->getUserContext(),
+                                              d_qstate.getSatContext(),
+                                              d_qstate.getUserContext(),
                                               d_quantEngine->getValuation(),
                                               isProxy));
             d_quantEngine->getTheoryEngine()
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index bc509d78a..ff971bc12 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -159,8 +159,9 @@ private:
     }
   };
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-public:
-  BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+  BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs);
   virtual ~BoundedIntegers();
 
   void presolve() override;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 173803a7f..effb5938c 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -280,9 +280,8 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-
-FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
-QModelBuilder( c, qe ){
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : QModelBuilder(qe)
+{
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index c49cd596b..89a472948 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -147,8 +147,9 @@ private:
   void mkCondVec( Node n, std::vector< Node > & cond );
   Node evaluateInterpreted( Node n, std::vector< Node > & vals );
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
-public:
-  FullModelChecker( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+  FullModelChecker(QuantifiersEngine* qe);
 
   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 796ee85fa..4f34c3baa 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -29,11 +29,13 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
+QModelBuilder::QModelBuilder(QuantifiersEngine* qe)
     : TheoryEngineModelBuilder(qe->getTheoryEngine()),
       d_qe(qe),
       d_addedLemmas(0),
-      d_triedLemmas(0) {}
+      d_triedLemmas(0)
+{
+}
 
 bool QModelBuilder::optUseModel() {
   return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 052f6f802..16e6f2a0b 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -29,7 +29,7 @@ namespace quantifiers {
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
-protected:
+ protected:
   //quantifiers engine
   QuantifiersEngine* d_qe;
   // must call preProcessBuildModelStd
@@ -38,8 +38,9 @@ protected:
   /** number of lemmas generated while building model */
   unsigned d_addedLemmas;
   unsigned d_triedLemmas;
-public:
-  QModelBuilder( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+  QModelBuilder(QuantifiersEngine* qe);
 
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 07840655a..8803fdb2c 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -35,12 +35,12 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 //Model Engine constructor
-ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
-QuantifiersModule( qe ),
-d_incomplete_check(true),
-d_addedLemmas(0),
-d_triedLemmas(0),
-d_totalLemmas(0)
+ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
+      d_incomplete_check(true),
+      d_addedLemmas(0),
+      d_triedLemmas(0),
+      d_totalLemmas(0)
 {
 
 }
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 6d9d3bfe3..5616eaf5e 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -43,8 +43,9 @@ private:
   int d_triedLemmas;
   int d_totalLemmas;
 public:
-  ModelEngine( context::Context* c, QuantifiersEngine* qe );
-  virtual ~ModelEngine();
+ ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+ virtual ~ModelEngine();
+
 public:
  bool needsCheck(Theory::Effort e) override;
  QEffort needsModel(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 9d84ea575..c064819fc 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -32,8 +32,10 @@ using namespace inst;
 
 namespace quantifiers {
 
-InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd)
-    : QuantifiersModule(qe), d_rd(rd), d_fullSaturateLimit(-1)
+InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
+                                   QuantifiersState& qs,
+                                   RelevantDomain* rd)
+    : QuantifiersModule(qs, qe), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index a77eb8a90..a24aeedab 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -62,7 +62,9 @@ namespace quantifiers {
 class InstStrategyEnum : public QuantifiersModule
 {
  public:
-  InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd);
+  InstStrategyEnum(QuantifiersEngine* qe,
+                   QuantifiersState& qs,
+                   RelevantDomain* rd);
   ~InstStrategyEnum() {}
   /** Presolve */
   void presolve() override;
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 7592f22c7..b123c3e15 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -36,14 +36,15 @@ namespace theory {
 namespace quantifiers {
 
 Instantiate::Instantiate(QuantifiersEngine* qe,
-                         context::UserContext* u,
+                         QuantifiersState& qs,
                          ProofNodeManager* pnm)
     : d_qe(qe),
+      d_qstate(qs),
       d_pnm(pnm),
       d_term_db(nullptr),
       d_term_util(nullptr),
-      d_total_inst_debug(u),
-      d_c_inst_match_trie_dom(u),
+      d_total_inst_debug(qs.getUserContext()),
+      d_c_inst_match_trie_dom(qs.getUserContext()),
       d_pfInst(pnm ? new CDProof(pnm) : nullptr)
 {
 }
@@ -429,7 +430,7 @@ bool Instantiate::existsInstantiation(Node q,
     if (it != d_c_inst_match_trie.end())
     {
       return it->second->existsInstMatch(
-          d_qe, q, terms, d_qe->getUserContext(), modEq);
+          d_qe, q, terms, d_qstate.getUserContext(), modEq);
     }
   }
   else
@@ -524,11 +525,11 @@ bool Instantiate::recordInstantiationInternal(Node q,
     }
     else
     {
-      imt = new inst::CDInstMatchTrie(d_qe->getUserContext());
+      imt = new inst::CDInstMatchTrie(d_qstate.getUserContext());
       d_c_inst_match_trie[q] = imt;
     }
     d_c_inst_match_trie_dom.insert(q);
-    return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq);
+    return imt->addInstMatch(d_qe, q, terms, d_qstate.getUserContext(), modEq);
   }
   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
   return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 4cc3c3d6d..3a51c8904 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -89,7 +89,7 @@ class Instantiate : public QuantifiersUtil
 
  public:
   Instantiate(QuantifiersEngine* qe,
-              context::UserContext* u,
+              QuantifiersState& qs,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -341,6 +341,8 @@ class Instantiate : public QuantifiersUtil
 
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** cache of term database for quantifiers engine */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index fa8982760..23942ba7e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1837,9 +1837,10 @@ bool MatchGen::isHandled( TNode n ) {
   return true;
 }
 
-QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
-    : QuantifiersModule(qe),
-      d_conflict(c, false),
+QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
+                                     QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
+      d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
       d_effort(EFFORT_INVALID)
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 90385865b..f90f1db18 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -230,8 +230,9 @@ private:  //for equivalence classes
  public:
   bool areMatchEqual( TNode n1, TNode n2 );
   bool areMatchDisequal( TNode n1, TNode n2 );
-public:
-  QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
+
+ public:
+  QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs);
 
   /** register quantifier */
   void registerQuantifier(Node q) override;
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 615ff987a..588d4de76 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -25,10 +25,9 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-
-QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
-
+QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe), d_added_split(qs.getUserContext())
+{
 }
 
 void QuantDSplit::checkOwnership(Node q)
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 12cf5e5af..6f9e74fad 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -49,7 +49,7 @@ class QuantDSplit : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  QuantDSplit( QuantifiersEngine * qe, context::Context* c );
+  QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs);
   /** determine whether this quantified formula will be reduced */
   void checkOwnership(Node q) override;
   /* whether this module needs to check this round */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 23815dc37..cbaa8bfe6 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -18,13 +18,17 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
 
 namespace CVC4 {
 namespace theory {
 
+QuantifiersModule::QuantifiersModule(quantifiers::QuantifiersState& qs,
+                                     QuantifiersEngine* qe)
+    : d_quantEngine(qe), d_qstate(qs)
+{
+}
+
 QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
 {
   return QEFFORT_NONE;
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 507c71698..240282d3d 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -21,6 +21,7 @@
 #include <map>
 #include <vector>
 
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -57,7 +58,7 @@ class QuantifiersModule {
   };
 
  public:
-  QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  QuantifiersModule(quantifiers::QuantifiersState& qs, QuantifiersEngine* qe);
   virtual ~QuantifiersModule(){}
   /** Presolve.
    *
@@ -156,6 +157,8 @@ class QuantifiersModule {
  protected:
   /** pointer to the quantifiers engine that owns this module */
   QuantifiersEngine* d_quantEngine;
+  /** The state of the quantifiers engine */
+  quantifiers::QuantifiersState& d_qstate;
 };/* class QuantifiersModule */
 
 /** Quantifiers utility
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 9dbca674e..d8b4062fc 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -39,71 +39,71 @@ QuantifiersModules::QuantifiersModules()
 }
 QuantifiersModules::~QuantifiersModules() {}
 void QuantifiersModules::initialize(QuantifiersEngine* qe,
-                                    context::Context* c,
+                                    QuantifiersState& qs,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
+    d_qcf.reset(new QuantConflictFind(qe, qs));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c));
+    d_sg_gen.reset(new ConjectureGenerator(qe, qs));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
+    d_inst_engine.reset(new InstantiationEngine(qe, qs));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
+    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs));
     modules.push_back(d_i_cbqi.get());
     qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
   if (options::sygus())
   {
-    d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
+    d_synth_e.reset(new SynthEngine(qe, qs));
     modules.push_back(d_synth_e.get());
   }
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
+    d_bint.reset(new BoundedIntegers(qe, qs));
     modules.push_back(d_bint.get());
   }
   if (options::finiteModelFind() || options::fmfBound())
   {
-    d_model_engine.reset(new quantifiers::ModelEngine(c, qe));
+    d_model_engine.reset(new ModelEngine(qe, qs));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new quantifiers::QuantDSplit(qe, c));
+    d_qsplit.reset(new QuantDSplit(qe, qs));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAntiSkolem())
   {
-    d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe));
+    d_anti_skolem.reset(new QuantAntiSkolem(qe, qs));
     modules.push_back(d_anti_skolem.get());
   }
   if (options::quantAlphaEquiv())
   {
-    d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe));
+    d_alpha_equiv.reset(new AlphaEquivalence(qe));
   }
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
-    d_rel_dom.reset(new quantifiers::RelevantDomain(qe));
-    d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
+    d_rel_dom.reset(new RelevantDomain(qe));
+    d_fs.reset(new InstStrategyEnum(qe, qs, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new quantifiers::SygusInst(qe));
+    d_sygus_inst.reset(new SygusInst(qe, qs));
     modules.push_back(d_sygus_inst.get());
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index a4c5dfb6e..e83a13ea7 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -53,37 +53,38 @@ class QuantifiersModules
    * a pointer to each module it constructs to modules.
    */
   void initialize(QuantifiersEngine* qe,
-                  context::Context* c,
+                  QuantifiersState& qs,
                   std::vector<QuantifiersModule*>& modules);
+
  private:
   //------------------------------ quantifier utilities
   /** relevant domain */
-  std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+  std::unique_ptr<RelevantDomain> d_rel_dom;
   //------------------------------ quantifiers modules
   /** alpha equivalence */
-  std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
+  std::unique_ptr<AlphaEquivalence> d_alpha_equiv;
   /** instantiation engine */
-  std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
+  std::unique_ptr<InstantiationEngine> d_inst_engine;
   /** model engine */
-  std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
+  std::unique_ptr<ModelEngine> d_model_engine;
   /** bounded integers utility */
-  std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
+  std::unique_ptr<BoundedIntegers> d_bint;
   /** Conflict find mechanism for quantifiers */
-  std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
+  std::unique_ptr<QuantConflictFind> d_qcf;
   /** subgoal generator */
-  std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+  std::unique_ptr<ConjectureGenerator> d_sg_gen;
   /** ceg instantiation */
-  std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
+  std::unique_ptr<SynthEngine> d_synth_e;
   /** full saturation */
-  std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
+  std::unique_ptr<InstStrategyEnum> d_fs;
   /** counterexample-based quantifier instantiation */
-  std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
+  std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
   /** quantifiers splitting */
-  std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
+  std::unique_ptr<QuantDSplit> d_qsplit;
   /** quantifiers anti-skolemization */
-  std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+  std::unique_ptr<QuantAntiSkolem> d_anti_skolem;
   /** SyGuS instantiation engine */
-  std::unique_ptr<quantifiers::SygusInst> d_sygus_inst;
+  std::unique_ptr<SygusInst> d_sygus_inst;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 61dd0c15e..901b7ad82 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -29,13 +29,14 @@ namespace theory {
 namespace quantifiers {
 
 Skolemize::Skolemize(QuantifiersEngine* qe,
-                     context::UserContext* u,
+                     QuantifiersState& qs,
                      ProofNodeManager* pnm)
     : d_quantEngine(qe),
-      d_skolemized(u),
+      d_skolemized(qs.getUserContext()),
       d_pnm(pnm),
       d_epg(pnm == nullptr ? nullptr
-                           : new EagerProofGenerator(pnm, u, "Skolemize::epg"))
+                           : new EagerProofGenerator(
+                                 pnm, qs.getUserContext(), "Skolemize::epg"))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index cb81a5c3a..8cf3e3176 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -64,9 +64,7 @@ class Skolemize
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersEngine* qe,
-            context::UserContext* u,
-            ProofNodeManager* pnm);
+  Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 4588e8952..42e7e2f13 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -29,8 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
-    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
+CegisUnif::CegisUnif(QuantifiersEngine* qe,
+                     QuantifiersState& qs,
+                     SynthConjecture* p)
+    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
 {
 }
 
@@ -398,8 +400,8 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
-    QuantifiersEngine* qe, SynthConjecture* parent)
-    : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
+    QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
+    : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
       d_qe(qe),
       d_parent(parent)
 {
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index aca85a691..ee9ae0132 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -47,7 +47,9 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent);
+  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
+                                QuantifiersState& qs,
+                                SynthConjecture* parent);
   /** Make the n^th literal of this strategy (G_uq_n).
    *
    * This call may add new lemmas of the form described above
@@ -202,7 +204,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
+  CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p);
   ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ad125a70f..b007f8716 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -43,8 +43,10 @@ namespace theory {
 namespace quantifiers {
 
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
+                                 QuantifiersState& qs,
                                  SygusStatistics& s)
     : d_qe(qe),
+      d_qstate(qs),
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
@@ -56,7 +58,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
-      d_ceg_cegisUnif(new CegisUnif(qe, this)),
+      d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
       d_sygus_ccore(new CegisCoreConnective(qe, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
@@ -235,7 +237,7 @@ void SynthConjecture::assign(Node q)
   d_feasible_strategy.reset(
       new DecisionStrategySingleton("sygus_feasible",
                                     d_feasible_guard,
-                                    d_qe->getSatContext(),
+                                    d_qstate.getSatContext(),
                                     d_qe->getValuation()));
   d_qe->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 7786f57ad..1d43e30ff 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -82,7 +82,9 @@ class EnumValGenerator
 class SynthConjecture
 {
  public:
-  SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s);
+  SynthConjecture(QuantifiersEngine* qe,
+                  QuantifiersState& qs,
+                  SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
   void presolve();
@@ -199,6 +201,8 @@ class SynthConjecture
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f49cc962f..09a6add1c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -30,14 +30,14 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
-    : QuantifiersModule(qe),
+SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
       d_tds(qe->getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, d_statistics)));
+      new SynthConjecture(d_quantEngine, qs, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -159,7 +159,7 @@ void SynthEngine::assignConjecture(Node q)
   if (d_conjs.back()->isAssigned())
   {
     d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-        new SynthConjecture(d_quantEngine, d_statistics)));
+        new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 25981748e..e3cf2e47b 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -33,7 +33,7 @@ class SynthEngine : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  public:
-  SynthEngine(QuantifiersEngine* qe, context::Context* c);
+  SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs);
   ~SynthEngine();
   /** presolve
    *
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index ccc23f109..210ebb921 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -46,8 +46,9 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
   return os;
 }
 
-TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
+TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs)
     : d_quantEngine(qe),
+      d_qstate(qs),
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
       d_eval(new Evaluator),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index e082cf15b..1bf6b6ca7 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -54,7 +54,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
-  TermDbSygus(context::Context* c, QuantifiersEngine* qe);
+  TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs);
   ~TermDbSygus() {}
   /** Reset this utility */
   bool reset(Theory::Effort e);
@@ -316,6 +316,8 @@ class TermDbSygus {
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
 
   //------------------------------utilities
   /** sygus explanation */
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 50c983ee7..12ce544d3 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -180,11 +180,11 @@ void addSpecialValues(
 
 }  // namespace
 
-SygusInst::SygusInst(QuantifiersEngine* qe)
-    : QuantifiersModule(qe),
-      d_ce_lemma_added(qe->getUserContext()),
-      d_global_terms(qe->getUserContext()),
-      d_notified_assertions(qe->getUserContext())
+SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
+      d_ce_lemma_added(qs.getUserContext()),
+      d_global_terms(qs.getUserContext()),
+      d_notified_assertions(qs.getUserContext())
 {
 }
 
@@ -518,7 +518,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
   DecisionStrategy* ds =
       new DecisionStrategySingleton("CeLiteral",
                                     lit,
-                                    d_quantEngine->getSatContext(),
+                                    d_qstate.getSatContext(),
                                     d_quantEngine->getValuation());
 
   d_dstrat[q].reset(ds);
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 0358b4984..10363f5a2 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -62,7 +62,7 @@ namespace quantifiers {
 class SygusInst : public QuantifiersModule
 {
  public:
-  SygusInst(QuantifiersEngine* qe);
+  SygusInst(QuantifiersEngine* qe, QuantifiersState& qs);
   ~SygusInst() = default;
 
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0ed488891..047a3cd41 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -33,10 +33,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermDb::TermDb(context::Context* c, context::UserContext* u,
-               QuantifiersEngine* qe)
-    : d_quantEngine(qe),
-      d_inactive_map(c) {
+TermDb::TermDb(QuantifiersState& qs, QuantifiersEngine* qe)
+    : d_quantEngine(qe), d_inactive_map(qs.getSatContext())
+{
   d_consistent_ee = true;
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index dff595757..afb8d0c0c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -76,7 +76,7 @@ class TermDb : public QuantifiersUtil {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  public:
-  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+  TermDb(QuantifiersState& qs, QuantifiersEngine* qe);
   ~TermDb();
   /** presolve (called once per user check-sat) */
   void presolve();
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 387a3e9d8..aaf8f347c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -43,7 +43,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
                                      const LogicInfo& logicInfo,
                                      ProofNodeManager* pnm)
     : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
-      d_qstate(c, u, valuation)
+      d_qstate(c, u, valuation),
+      d_qengine(d_qstate, pnm)
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute("qid", this);
@@ -59,6 +60,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   }
   // indicate we are using the quantifiers theory state object
   d_theoryState = &d_qstate;
+
+  // 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.
+  d_quantEngine = &d_qengine;
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index b46390284..82a588009 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory.h"
 #include "theory/valuation.h"
 
@@ -80,6 +81,8 @@ class TheoryQuantifiers : public Theory {
   QuantifiersProofRuleChecker d_qChecker;
   /** The quantifiers state */
   QuantifiersState d_qstate;
+  /** The quantifiers engine, which lives here */
+  QuantifiersEngine d_qengine;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8b3ea8622..f60bb724f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,37 +30,34 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-QuantifiersEngine::QuantifiersEngine(TheoryEngine* te,
-                                     DecisionManager& dm,
+QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate,
                                      ProofNodeManager* pnm)
-    : d_te(te),
-      d_context(te->getSatContext()),
-      d_userContext(te->getUserContext()),
-      d_decManager(dm),
+    : d_qstate(qstate),
+      d_te(nullptr),
+      d_decManager(nullptr),
       d_masterEqualityEngine(nullptr),
-      d_eq_query(
-          new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)),
+      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
       d_term_util(new quantifiers::TermUtil(this)),
       d_term_canon(new expr::TermCanonize),
-      d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)),
+      d_term_db(new quantifiers::TermDb(qstate, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
-      d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)),
-      d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)),
+      d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
+      d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
-      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)
+      d_conflict_c(qstate.getSatContext(), false),
+      d_quants_prereg(qstate.getUserContext()),
+      d_quants_red(qstate.getUserContext()),
+      d_lemmas_produced_c(qstate.getUserContext()),
+      d_ierCounter_c(qstate.getSatContext()),
+      d_presolve(qstate.getUserContext(), true),
+      d_presolve_in(qstate.getUserContext()),
+      d_presolve_cache(qstate.getUserContext()),
+      d_presolve_cache_wq(qstate.getUserContext()),
+      d_presolve_cache_wic(qstate.getUserContext())
 {
   //---- utilities
   d_util.push_back(d_eq_query.get());
@@ -71,7 +68,7 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te,
   if (options::sygus() || options::sygusInst())
   {
     // must be constructed here since it is required for datatypes finistInit
-    d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this));
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate));
   }
 
   d_util.push_back(d_instantiate.get());
@@ -106,53 +103,43 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te,
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, d_context, "FirstOrderModelFmc"));
-      d_builder.reset(
-          new quantifiers::fmcheck::FullModelChecker(d_context, this));
+          this, qstate, "FirstOrderModelFmc"));
+      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(
-          new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(d_context, this));
+          new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(this));
     }
   }else{
     d_model.reset(
-        new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
+        new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
   }
 }
 
 QuantifiersEngine::~QuantifiersEngine() {}
 
-void QuantifiersEngine::finishInit()
+void QuantifiersEngine::finishInit(TheoryEngine* te,
+                                   DecisionManager* dm,
+                                   eq::EqualityEngine* mee)
 {
-  // Initialize the modules and the utilities here. We delay their
-  // initialization to here, since this is after TheoryQuantifiers finishInit,
-  // which has initialized the state and inference manager of this engine.
+  d_te = te;
+  d_decManager = dm;
+  d_masterEqualityEngine = mee;
+  // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(this, d_context, d_modules);
+  d_qmodules->initialize(this, d_qstate, d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
   }
 }
 
-void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
-{
-  d_masterEqualityEngine = mee;
-}
-
 TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
 
 DecisionManager* QuantifiersEngine::getDecisionManager()
 {
-  return &d_decManager;
-}
-
-context::Context* QuantifiersEngine::getSatContext() { return d_context; }
-
-context::UserContext* QuantifiersEngine::getUserContext()
-{
-  return d_userContext;
+  return d_decManager;
 }
 
 OutputChannel& QuantifiersEngine::getOutputChannel()
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0c3bb181e..7ed183342 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
@@ -59,20 +60,14 @@ class QuantifiersEngine {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
+  QuantifiersEngine(quantifiers::QuantifiersState& qstate,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
-  /** finish initialize */
-  void finishInit();
   //---------------------- external interface
   /** get theory engine */
   TheoryEngine* getTheoryEngine() const;
   /** Get the decision manager */
   DecisionManager* getDecisionManager();
-  /** get default sat context for quantifiers engine */
-  context::Context* getSatContext();
-  /** get default sat context for quantifiers engine */
-  context::UserContext* getUserContext();
   /** get default output channel for the quantifiers engine */
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
@@ -110,8 +105,19 @@ class QuantifiersEngine {
   //---------------------- end utilities
  private:
   //---------------------- private initialization
-  /** Set the master equality engine */
-  void setMasterEqualityEngine(eq::EqualityEngine* mee);
+  /**
+   * Finish initialize, which passes pointers to the objects that quantifiers
+   * engine needs but were not available when it was created. This is
+   * called after theories have been created but before they have finished
+   * initialization.
+   *
+   * @param te The theory engine
+   * @param dm The decision manager of the theory engine
+   * @param mee The master equality engine of the theory engine
+   */
+  void finishInit(TheoryEngine* te,
+                  DecisionManager* dm,
+                  eq::EqualityEngine* mee);
   //---------------------- end private initialization
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -329,14 +335,12 @@ public:
   Statistics d_statistics;
 
  private:
+  /** The quantifiers state object */
+  quantifiers::QuantifiersState& d_qstate;
   /** Pointer to theory engine object */
   TheoryEngine* d_te;
-  /** The SAT context */
-  context::Context* d_context;
-  /** The user context */
-  context::UserContext* d_userContext;
   /** Reference to the decision manager of the theory engine */
-  DecisionManager& d_decManager;
+  DecisionManager* d_decManager;
   /** Pointer to the master equality engine */
   eq::EqualityEngine* d_masterEqualityEngine;
   /** vector of utilities for quantifiers */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 5bea454e8..fef3fdc67 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -68,8 +68,7 @@ Theory::Theory(TheoryId id,
       d_facts(satContext),
       d_factsHead(satContext, 0),
       d_sharedTermsIndex(satContext, 0),
-      d_careGraph(NULL),
-      d_quantEngine(NULL),
+      d_careGraph(nullptr),
       d_decManager(nullptr),
       d_instanceName(name),
       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
@@ -82,6 +81,7 @@ Theory::Theory(TheoryId id,
       d_allocEqualityEngine(nullptr),
       d_theoryState(nullptr),
       d_inferManager(nullptr),
+      d_quantEngine(nullptr),
       d_pnm(pnm)
 {
   smtStatisticsRegistry()->registerStat(&d_checkTime);
@@ -115,7 +115,6 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee)
 
 void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
 {
-  Assert(d_quantEngine == nullptr);
   // quantifiers engine may be null if not in quantified logic
   d_quantEngine = qe;
 }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 0eb3d9a33..fa26ab65e 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -140,12 +140,6 @@ class Theory {
   /** The care graph the theory will use during combination. */
   CareGraph* d_careGraph;
 
-  /**
-   * Pointer to the quantifiers engine (or NULL, if quantifiers are not
-   * supported or not enabled). Not owned by the theory.
-   */
-  QuantifiersEngine* d_quantEngine;
-
   /** Pointer to the decision manager. */
   DecisionManager* d_decManager;
 
@@ -234,6 +228,12 @@ class Theory {
    */
   TheoryInferenceManager* d_inferManager;
 
+  /**
+   * Pointer to the quantifiers engine (or NULL, if quantifiers are not
+   * supported or not enabled). Not owned by the theory.
+   */
+  QuantifiersEngine* d_quantEngine;
+
   /** Pointer to proof node manager */
   ProofNodeManager* d_pnm;
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 27ae0018e..16d68ea5c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -169,8 +169,10 @@ void TheoryEngine::finishInit()
   // initialize the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    // initialize the quantifiers engine
-    d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
+    // get the quantifiers engine, which is initialized by the quantifiers
+    // theory
+    d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
+    Assert(d_quantEngine != nullptr);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.
@@ -178,10 +180,11 @@ void TheoryEngine::finishInit()
   // get pointer to the shared solver
   d_sharedSolver = d_tc->getSharedSolver();
 
-  // set the core equality engine on quantifiers engine
+  // finish initializing the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
+    d_quantEngine->finishInit(
+        this, d_decManager.get(), d_tc->getCoreEqualityEngine());
   }
 
   // finish initializing the theories by linking them with the appropriate
@@ -205,12 +208,6 @@ void TheoryEngine::finishInit()
     // finish initializing the theory
     t->finishInit();
   }
-
-  // finish initializing the quantifiers engine
-  if (d_logicInfo.isQuantified())
-  {
-    d_quantEngine->finishInit();
-  }
 }
 
 ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
@@ -283,8 +280,6 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
-  delete d_quantEngine;
-
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index df57d9903..0be511e47 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -156,9 +156,7 @@ class TheoryEngine {
   std::unique_ptr<theory::CombinationEngine> d_tc;
   /** The shared solver of the above combination engine. */
   theory::SharedSolver* d_sharedSolver;
-  /**
-   * The quantifiers engine
-   */
+  /** The quantifiers engine, which is owned by the quantifiers theory */
   theory::QuantifiersEngine* d_quantEngine;
   /**
    * The decision manager