From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Jan 2021 19:27:27 +0000 (-0600)
Subject: Use standard equality engine information in quantifiers state (#5824)
X-Git-Tag: cvc5-1.0.0~2344
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3234db4;p=cvc5.git

Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
---

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 5e242659f..71eac49a0 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -77,21 +77,11 @@ const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
   return d_eemanager->getEeTheoryInfo(tid);
 }
 
-eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine()
-{
-  return d_eemanager->getCoreEqualityEngine();
-}
-
 void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
 
 void CombinationEngine::postProcessModel(bool incomplete)
 {
-  // should have a consistent core equality engine
-  eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine();
-  if (mee != nullptr)
-  {
-    AlwaysAssert(mee->consistent());
-  }
+  d_eemanager->notifyModel(incomplete);
   // postprocess with the model
   d_mmanager->postProcessModel(incomplete);
 }
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 4413da603..765a49d68 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -49,15 +49,8 @@ class CombinationEngine
   /** Finish initialization */
   void finishInit();
 
-  //-------------------------- equality engine
   /** Get equality engine theory information for theory with identifier tid. */
   const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
-  /**
-   * Get the "core" equality engine. This is the equality engine that
-   * quantifiers should use.
-   */
-  eq::EqualityEngine* getCoreEqualityEngine();
-  //-------------------------- end equality engine
   //-------------------------- model
   /**
    * Reset the model maintained by this class. This resets all local information
diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h
index 6e40ceb7b..5b8dc3b93 100644
--- a/src/theory/ee_manager.h
+++ b/src/theory/ee_manager.h
@@ -73,17 +73,17 @@ class EqEngineManager
    * Get the equality engine theory information for theory with the given id.
    */
   const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
-  /**
-   * Get the core equality engine, which is the equality engine that the
-   * quantifiers engine should use. This corresponds to the master equality
-   * engine if eeMode is distributed, or the central equality engine if eeMode
-   * is central.
-   */
-  virtual eq::EqualityEngine* getCoreEqualityEngine() = 0;
 
   /** Allocate equality engine that is context-dependent on c with info esi */
   eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
                                              context::Context* c);
+  /**
+   * Notify this class that we are about to terminate with a model. This method
+   * is for debugging only.
+   *
+   * @param incomplete Whether we are answering "unknown" instead of "sat".
+   */
+  virtual void notifyModel(bool incomplete) {}
 
  protected:
   /** Reference to the theory engine */
diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 3fb5fc0ce..496b04a52 100644
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -47,6 +47,19 @@ void EqEngineManagerDistributed::initializeTheories()
     Unhandled() << "Expected shared solver to use equality engine";
   }
 
+  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  if (logicInfo.isQuantified())
+  {
+    // construct the master equality engine
+    Assert(d_masterEqualityEngine == nullptr);
+    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
+    Assert(qe != nullptr);
+    d_masterEENotify.reset(new MasterNotifyClass(qe));
+    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
+                                                        d_te.getSatContext(),
+                                                        "theory::master",
+                                                        false));
+  }
   // allocate equality engines per theory
   for (TheoryId theoryId = theory::THEORY_FIRST;
        theoryId != theory::THEORY_LAST;
@@ -63,48 +76,34 @@ void EqEngineManagerDistributed::initializeTheories()
     EeSetupInfo esi;
     if (!t->needsEqualityEngine(esi))
     {
-      // theory said it doesn't need an equality engine, skip
+      // the theory said it doesn't need an equality engine, skip
+      continue;
+    }
+    if (esi.d_useMaster)
+    {
+      // the theory said it wants to use the master equality engine
+      eet.d_usedEe = d_masterEqualityEngine.get();
       continue;
     }
     // allocate the equality engine
     eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
     // the theory uses the equality engine
     eet.d_usedEe = eet.d_allocEe.get();
+    // if there is a master equality engine
+    if (d_masterEqualityEngine != nullptr)
+    {
+      // set the master equality engine of the theory's equality engine
+      eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get());
+    }
   }
+}
 
-  const LogicInfo& logicInfo = d_te.getLogicInfo();
-  if (logicInfo.isQuantified())
+void EqEngineManagerDistributed::notifyModel(bool incomplete)
+{
+  // should have a consistent master equality engine
+  if (d_masterEqualityEngine.get() != nullptr)
   {
-    // construct the master equality engine
-    Assert(d_masterEqualityEngine == nullptr);
-    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
-    Assert(qe != nullptr);
-    d_masterEENotify.reset(new MasterNotifyClass(qe));
-    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
-                                                        d_te.getSatContext(),
-                                                        "theory::master",
-                                                        false));
-
-    for (TheoryId theoryId = theory::THEORY_FIRST;
-         theoryId != theory::THEORY_LAST;
-         ++theoryId)
-    {
-      Theory* t = d_te.theoryOf(theoryId);
-      if (t == nullptr)
-      {
-        // theory not active, skip
-        continue;
-      }
-      EeTheoryInfo& eet = d_einfo[theoryId];
-      // Get the allocated equality engine, and connect it to the master
-      // equality engine.
-      eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
-      if (eeAlloc != nullptr)
-      {
-        // set the master equality engine of the theory's equality engine
-        eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
-      }
-    }
+    AlwaysAssert(d_masterEqualityEngine->consistent());
   }
 }
 
@@ -114,10 +113,5 @@ void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
   d_quantEngine->eqNotifyNewClass(t);
 }
 
-eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine()
-{
-  return d_masterEqualityEngine.get();
-}
-
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index c7c1e7f4c..9578706d9 100644
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -52,8 +52,9 @@ class EqEngineManagerDistributed : public EqEngineManager
    * per theories and connects them to a master equality engine.
    */
   void initializeTheories() override;
-  /** get the core equality engine */
-  eq::EqualityEngine* getCoreEqualityEngine() override;
+  /** Notify model */
+  void notifyModel(bool incomplete) override;
+
  private:
   /** notify class for master equality engine */
   class MasterNotifyClass : public theory::eq::EqualityEngineNotify
diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h
index 78f2f211e..7770cfc49 100644
--- a/src/theory/ee_setup_info.h
+++ b/src/theory/ee_setup_info.h
@@ -37,13 +37,21 @@ class EqualityEngineNotify;
  */
 struct EeSetupInfo
 {
-  EeSetupInfo() : d_notify(nullptr), d_constantsAreTriggers(true) {}
+  EeSetupInfo()
+      : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false)
+  {
+  }
   /** The notification class of the theory */
   eq::EqualityEngineNotify* d_notify;
   /** The name of the equality engine */
   std::string d_name;
   /** Constants are triggers */
   bool d_constantsAreTriggers;
+  /**
+   * Whether we want our state to use the master equality engine. This should
+   * be true exclusively for the theory of quantifiers.
+   */
+  bool d_useMaster;
 };
 
 }  // namespace theory
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index a8632c02f..411ab36b9 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -663,9 +663,10 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   TypeNode pvtn = pv.getType();
   TypeNode pvtnb = pvtn.getBaseType();
   Node pvr = pv;
-  if (d_qe->getMasterEqualityEngine()->hasTerm(pv))
+  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  if (ee->hasTerm(pv))
   {
-    pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv);
+    pvr = ee->getRepresentative(pv);
   }
   Trace("cegqi-inst-debug") << "[Find instantiation for " << pv
                            << "], rep=" << pvr << ", instantiator is "
@@ -1306,7 +1307,7 @@ void CegInstantiator::processAssertions() {
   d_curr_type_eqc.clear();
 
   // must use master equality engine to avoid value instantiations
-  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
 
   //for each variable
   for( unsigned i=0; i<d_vars.size(); i++ ){
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 0fd5249e8..cdee268d6 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -59,7 +59,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
     if( isExcludedEqc( eqc ) ){
       d_mode = cand_term_none;
     }else{
-      eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+      eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
       if( ee->hasTerm( eqc ) ){
         TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
         if( tat ){
@@ -93,6 +93,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
 Node CandidateGeneratorQE::getNextCandidateInternal()
 {
   if( d_mode==cand_term_db ){
+    eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
     Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
@@ -103,7 +104,7 @@ Node CandidateGeneratorQE::getNextCandidateInternal()
           if( d_exclude_eqc.empty() ){
             return n;
           }else{
-            Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+            Node r = ee->getRepresentative(n);
             if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
               Debug("cand-gen-qe") << "...returning " << n << std::endl;
               return n;
@@ -143,8 +144,9 @@ CandidateGenerator( qe ), d_match_pattern( mpat ){
 }
 
 void CandidateGeneratorQELitDeq::reset( Node eqc ){
-  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
-  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  Node falset = NodeManager::currentNM()->mkConst(false);
+  d_eqc_false = eq::EqClassIterator(falset, ee);
 }
 
 Node CandidateGeneratorQELitDeq::getNextCandidate(){
@@ -177,7 +179,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
 }
 
 void CandidateGeneratorQEAll::reset( Node eqc ) {
-  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
   d_firstTime = true;
 }
 
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index cdfb9c85c..6d13ef2ee 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -231,7 +231,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
-    EqualityQuery* eq = d_quantEngine->getEqualityQuery();
+    quantifiers::QuantifiersState& qs = d_quantEngine->getState();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -283,10 +283,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
           }
           else if (!itf->second.isNull())
           {
-            if (!eq->areEqual(itf->second, args[k]))
+            if (!qs.areEqual(itf->second, args[k]))
             {
               if (!d_quantEngine->getTermDatabase()->isEntailed(
-                      itf->second.eqNode(args[k]), true, eq))
+                      itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
               }
@@ -318,7 +318,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
         {
           if (!itf->second.isNull())
           {
-            Node r = eq->getRepresentative(itf->second);
+            Node r = qs.getRepresentative(itf->second);
             std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
             if (itfr != arg_to_rep.end())
             {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 63731c444..4cdb207f3 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -285,7 +286,7 @@ int InstMatchGenerator::getMatch(
     Trace("matching-fail") << "Internal error for match generator." << std::endl;
     return -2;
   }
-  EqualityQuery* q = qe->getEqualityQuery();
+  quantifiers::QuantifiersState& qs = qe->getState();
   bool success = true;
   std::vector<int> prev;
   // if t is null
@@ -303,7 +304,7 @@ int InstMatchGenerator::getMatch(
       Trace("matching-debug2")
           << "Setting " << ct << " to " << t[i] << "..." << std::endl;
       bool addToPrev = m.get(ct).isNull();
-      if (!m.set(q, ct, t[i]))
+      if (!m.set(qs, ct, t[i]))
       {
         // match is in conflict
         Trace("matching-fail")
@@ -319,7 +320,7 @@ int InstMatchGenerator::getMatch(
     }
     else if (ct == -1)
     {
-      if (!q->areEqual(d_match_pattern[i], t[i]))
+      if (!qs.areEqual(d_match_pattern[i], t[i]))
       {
         Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i]
                                << " and " << t[i] << std::endl;
@@ -335,7 +336,7 @@ int InstMatchGenerator::getMatch(
   if (d_match_pattern.getKind() == INST_CONSTANT)
   {
     bool addToPrev = m.get(d_children_types[0]).isNull();
-    if (!m.set(q, d_children_types[0], t))
+    if (!m.set(qs, d_children_types[0], t))
     {
       success = false;
     }
@@ -371,7 +372,7 @@ int InstMatchGenerator::getMatch(
       {
         if (t.getType().isBoolean())
         {
-          t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t));
+          t_match = nm->mkConst(!qs.areEqual(nm->mkConst(true), t));
         }
         else
         {
@@ -391,7 +392,7 @@ int InstMatchGenerator::getMatch(
     if (!t_match.isNull())
     {
       bool addToPrev = m.get(v).isNull();
-      if (!m.set(q, v, t_match))
+      if (!m.set(qs, v, t_match))
       {
         success = false;
       }
@@ -467,7 +468,7 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
     // we did not properly initialize the candidate generator, thus we fail
     return false;
   }
-  eqc = qe->getEqualityQuery()->getRepresentative( eqc );
+  eqc = qe->getState().getRepresentative(eqc);
   Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
   if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
     d_eq_class = d_eq_class_rel;
@@ -509,7 +510,7 @@ int InstMatchGenerator::getNextMatch(Node f,
   Node t = d_curr_first_candidate;
   do{
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
-    Assert(!qe->inConflict());
+    Assert(!qe->getState().isInConflict());
     //if t not null, try to fit it into match m
     if( !t.isNull() ){
       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
@@ -523,7 +524,8 @@ int InstMatchGenerator::getNextMatch(Node f,
       }
       //get the next candidate term t
       if( success<0 ){
-        t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
+        t = qe->getState().isInConflict() ? Node::null()
+                                          : d_cg->getNextCandidate();
       }else{
         d_curr_first_candidate = d_cg->getNextCandidate();
       }
@@ -554,13 +556,15 @@ uint64_t InstMatchGenerator::addInstantiations(Node f,
       if (sendInstantiation(tparent, m))
       {
         addedLemmas++;
-        if( qe->inConflict() ){
+        if (qe->getState().isInConflict())
+        {
           break;
         }
       }
     }else{
       addedLemmas++;
-      if( qe->inConflict() ){
+      if (qe->getState().isInConflict())
+      {
         break;
       }
     }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index b4a7457a3..371bc3378 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
@@ -174,7 +175,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
           << "...processing " << j << " / " << newMatches.size()
           << ", #lemmas = " << addedLemmas << std::endl;
       processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
-      if (qe->inConflict())
+      if (qe->getState().isInConflict())
       {
         return addedLemmas;
       }
@@ -221,7 +222,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                                        size_t endChildIndex,
                                                        bool modEq)
 {
-  Assert(!qe->inConflict());
+  Assert(!qe->getState().isInConflict());
   if (childIndex == endChildIndex)
   {
     // m is an instantiation
@@ -256,7 +257,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                  childIndex,
                                  endChildIndex,
                                  modEq);
-        if (qe->inConflict())
+        if (qe->getState().isInConflict())
         {
           break;
         }
@@ -280,13 +281,13 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
     {
       return;
     }
-    eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+    quantifiers::QuantifiersState& qs = qe->getState();
     // check modulo equality for other possible instantiations
-    if (!ee->hasTerm(n))
+    if (!qs.hasTerm(n))
     {
       return;
     }
-    eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+    eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
     while (!eqc.isFinished())
     {
       Node en = (*eqc);
@@ -304,7 +305,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                    childIndex,
                                    endChildIndex,
                                    modEq);
-          if (qe->inConflict())
+          if (qe->getState().isInConflict())
           {
             break;
           }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 8c3de21a9..b5ef7792d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -67,6 +67,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
                                                      QuantifiersEngine* qe,
                                                      Trigger* tparent)
 {
+  quantifiers::QuantifiersState& qs = qe->getState();
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
   if (d_eqc.isNull())
@@ -83,16 +84,16 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
     {
       // iterate over all classes except r
       tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
-      if (tat && !qe->inConflict())
+      if (tat && !qs.isInConflict())
       {
-        Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
+        Node r = qs.getRepresentative(d_eqc);
         for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
         {
           if (t.first != r)
           {
             InstMatch m(q);
             addInstantiations(m, qe, addedLemmas, 0, &(t.second));
-            if (qe->inConflict())
+            if (qs.isInConflict())
             {
               break;
             }
@@ -105,7 +106,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
   Debug("simple-trigger-debug")
       << "Adding instantiations based on " << tat << " from " << d_op << " "
       << d_eqc << std::endl;
-  if (tat && !qe->inConflict())
+  if (tat && !qs.isInConflict())
   {
     InstMatch m(q);
     addInstantiations(m, qe, addedLemmas, 0, tat);
@@ -146,6 +147,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     return;
   }
+  quantifiers::QuantifiersState& qs = qe->getState();
   if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
   {
     int v = d_var_num[argIndex];
@@ -162,7 +164,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
           m.setValue(v, t);
           addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
           m.setValue(v, prev);
-          if (qe->inConflict())
+          if (qs.isInConflict())
           {
             break;
           }
@@ -172,7 +174,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // inst constant from another quantified formula, treat as ground term?
   }
-  Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+  Node r = qs.getRepresentative(d_match_pattern[argIndex]);
   std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
   if (it != tat->d_data.end())
   {
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index cd0ab7976..48c02f288 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -98,8 +98,9 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           Trace("inst-engine-debug")
               << " -> unfinished= "
               << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
-              << ", conflict=" << d_quantEngine->inConflict() << std::endl;
-          if( d_quantEngine->inConflict() ){
+              << ", conflict=" << d_qstate.isInConflict() << std::endl;
+          if (d_qstate.isInConflict())
+          {
             return;
           }
           else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
@@ -165,7 +166,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
   {
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     doInstantiationRound(e);
-    if (d_quantEngine->inConflict())
+    if (d_qstate.isInConflict())
     {
       Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
       Trace("inst-engine") << "Conflict, added lemmas = "
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 470120be2..b1caa739e 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -109,7 +109,7 @@ uint64_t Trigger::addInstantiations()
   {
     // for each ground term t that does not exist in the equality engine, we
     // add a purification lemma of the form (k = t).
-    eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine();
+    eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine();
     for (const Node& gt : d_groundTerms)
     {
       if (!ee->hasTerm(gt))
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 0553c1745..4edacb827 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -52,7 +52,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     d_eq_class = Node::null();
     // if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get(d_children_types[0]).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
+    if (!m.set(qe->getState(), d_children_types[0], s))
     {
       return -1;
     }
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index b8515df91..08741ef0f 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -33,7 +33,10 @@ namespace quantifiers {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
     QuantifiersState& qs, QuantifiersEngine* qe)
-    : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0)
+    : d_qe(qe),
+      d_qstate(qs),
+      d_eqi_counter(qs.getSatContext()),
+      d_reset_count(0)
 {
 }
 
@@ -46,51 +49,12 @@ bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
   return true;
 }
 
-bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
-  return getEngine()->hasTerm( a );
-}
-
-Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
-  eq::EqualityEngine* ee = getEngine();
-  if( ee->hasTerm( a ) ){
-    return ee->getRepresentative( a );
-  }else{
-    return a;
-  }
-}
-
-bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else{
-    eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      return ee->areEqual( a, b );
-    }else{
-      return false;
-    }
-  }
-}
-
-bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
-  if( a==b ){
-    return false;
-  }else{
-    eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      return ee->areDisequal( a, b, false );
-    }else{
-      return a.isConst() && b.isConst();
-    }
-  }
-}
-
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
                                                                Node q,
                                                                int index)
 {
   Assert(q.isNull() || q.getKind() == FORALL);
-  Node r = getRepresentative( a );
+  Node r = d_qstate.getRepresentative(a);
   if( options::finiteModelFind() ){
     if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
       //map back from values assigned by model, if any
@@ -99,7 +63,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
         if (!tr.isNull())
         {
           r = tr;
-          r = getRepresentative( r );
+          r = d_qstate.getRepresentative(r);
         }else{
           if( r.getType().isSort() ){
             Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
@@ -129,7 +93,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   // find best selection for representative
   Node r_best;
   std::vector<Node> eqc;
-  getEquivalenceClass(r, eqc);
+  d_qstate.getEquivalenceClass(r, eqc);
   Trace("internal-rep-select")
       << "Choose representative for equivalence class : " << eqc
       << ", type = " << v_tn << std::endl;
@@ -180,30 +144,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   return r_best;
 }
 
-eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
-  return d_qe->getMasterEqualityEngine();
-}
-
-void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
-  eq::EqualityEngine* ee = getEngine();
-  if( ee->hasTerm( a ) ){
-    Node rep = ee->getRepresentative( a );
-    eq::EqClassIterator eqc_iter( rep, ee );
-    while( !eqc_iter.isFinished() ){
-      eqc.push_back( *eqc_iter );
-      eqc_iter++;
-    }
-  }else{
-    eqc.push_back( a );
-  }
-  //a should be in its equivalence class
-  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
-}
-
-TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
-  return d_qe->getTermDatabase()->getCongruentTerm( f, args );
-}
-
 //helper functions
 
 Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index b82b9ae64..a3f895f54 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -29,11 +29,7 @@ namespace quantifiers {
 
 /** EqualityQueryQuantifiersEngine class
  *
- * This is a wrapper class around an equality engine that is used for
- * queries required by algorithms in the quantifiers theory. It uses an equality
- * engine, as determined by the quantifiers engine it points to.
- *
- * The main extension of this class wrt EqualityQuery is the function
+ * The main method of this class is the function
  * getInternalRepresentative, which is used by instantiation-based methods
  * that are agnostic with respect to choosing terms within an equivalence class.
  * Examples of such methods are finite model finding and enumerative
@@ -41,7 +37,7 @@ namespace quantifiers {
  * representative based on the internal heuristic, which is currently based on
  * choosing the term that was previously chosen as a representative earliest.
  */
-class EqualityQueryQuantifiersEngine : public EqualityQuery
+class EqualityQueryQuantifiersEngine : public QuantifiersUtil
 {
  public:
   EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
@@ -52,32 +48,6 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
   void registerQuantifier(Node q) override {}
   /** identify */
   std::string identify() const override { return "EqualityQueryQE"; }
-  /** does the equality engine have term a */
-  bool hasTerm(Node a) override;
-  /** get the representative of a */
-  Node getRepresentative(Node a) override;
-  /** are a and b equal? */
-  bool areEqual(Node a, Node b) override;
-  /** are a and b disequal? */
-  bool areDisequal(Node a, Node b) override;
-  /** get equality engine
-  * This may either be the master equality engine or the model's equality
-  * engine.
-  */
-  eq::EqualityEngine* getEngine() override;
-  /** get list of members in the equivalence class of a */
-  void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
-  /** get congruent term
-  * If possible, returns a term n such that:
-  * (1) n is a term in the equality engine from getEngine().
-  * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
-  * of args[i] for i=1...k
-  * Otherwise, returns the null node.
-  *
-  * Notice that f should be a "match operator", returned by
-  * TermDb::getMatchOperator.
-  */
-  TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
   /** gets the current best representative in the equivalence
    * class of a, based on some heuristic. Currently, the default heuristic
    * chooses terms that were previously chosen as representatives
@@ -97,6 +67,8 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
  private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
+  /** the quantifiers state */
+  QuantifiersState& d_qstate;
   /** quantifiers equality inference */
   context::CDO< unsigned > d_eqi_counter;
   /** internal representatives */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index b2c7bf704..053174d07 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -358,7 +358,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
         Node r = fm->getRepresentative( it->second[a] );
         if( Trace.isOn("fmc-model-debug") ){
           std::vector< Node > eqc;
-          d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc );
+          d_qstate.getEquivalenceClass(r, eqc);
           Trace("fmc-model-debug") << "   " << (it->second[a]==r);
           Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
           //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 4d74c1697..427d82e7c 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -279,14 +279,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       if( !riter.isIncomplete() ){
         int triedLemmas = 0;
         int addedLemmas = 0;
-        EqualityQuery* qy = d_quantEngine->getEqualityQuery();
         Instantiate* inst = d_quantEngine->getInstantiate();
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for (unsigned i = 0; i < riter.getNumTerms(); i++)
           {
-            m.set(qy, i, riter.getCurrentTerm(i));
+            m.set(d_qstate, i, riter.getCurrentTerm(i));
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index b2b58220a..5d6779406 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -45,24 +45,6 @@ void InstMatch::add(InstMatch& m)
   }
 }
 
-bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
-  Assert(d_vals.size() == m.d_vals.size());
-  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
-  {
-    if( !m.d_vals[i].isNull() ){
-      if( d_vals[i].isNull() ){
-        d_vals[i] = m.d_vals[i];
-      }else{
-        if( !q->areEqual( d_vals[i], m.d_vals[i]) ){
-          clear();
-          return false;
-        }
-      }
-    }
-  }
-  return true;
-}
-
 void InstMatch::debugPrint( const char* c ){
   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
   {
@@ -111,20 +93,14 @@ void InstMatch::setValue(size_t i, TNode n)
   Assert(i < d_vals.size());
   d_vals[i] = n;
 }
-bool InstMatch::set(EqualityQuery* q, size_t i, TNode n)
+bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n)
 {
   Assert(i < d_vals.size());
   if( !d_vals[i].isNull() ){
-    if (q->areEqual(d_vals[i], n))
-    {
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    d_vals[i] = n;
-    return true;
+    return qs.areEqual(d_vals[i], n);
   }
+  d_vals[i] = n;
+  return true;
 }
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a51c0ecdc..e3d7909b7 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -24,7 +24,9 @@
 namespace CVC4 {
 namespace theory {
 
-class EqualityQuery;
+namespace quantifiers {
+class QuantifiersState;
+}
 
 namespace inst {
 
@@ -50,13 +52,6 @@ public:
    * not already initialized in this match.
    */
   void add(InstMatch& m);
-  /** merge with match m
-   *
-   * This method returns true if the merge was successful, that is, all jointly
-   * initialized fields of this class and m are equivalent modulo the equalities
-   * given by q.
-   */
-  bool merge( EqualityQuery* q, InstMatch& m );
   /** is this complete, i.e. are all fields non-null? */
   bool isComplete();
   /** is this empty, i.e. are all fields the null node? */
@@ -87,7 +82,7 @@ public:
    * This method returns true if the i^th field was previously uninitialized,
    * or is equivalent to n modulo the equalities given by q.
    */
-  bool set(EqualityQuery* q, size_t i, TNode n);
+  bool set(quantifiers::QuantifiersState& qs, size_t i, TNode n);
 };
 
 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index aaf7cb4bc..0bd5000f1 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -52,12 +52,11 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   }
   if (modEq)
   {
+    quantifiers::QuantifiersState& qs = qe->getState();
     // check modulo equality if any other instantiation match exists
-    if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+    if (!n.isNull() && qs.hasTerm(n))
     {
-      eq::EqClassIterator eqc(
-          qe->getEqualityQuery()->getEngine()->getRepresentative(n),
-          qe->getEqualityQuery()->getEngine());
+      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
       while (!eqc.isFinished())
       {
         Node en = (*eqc);
@@ -331,11 +330,10 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   if (modEq)
   {
     // check modulo equality if any other instantiation match exists
-    if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+    quantifiers::QuantifiersState& qs = qe->getState();
+    if (!n.isNull() && qs.hasTerm(n))
     {
-      eq::EqClassIterator eqc(
-          qe->getEqualityQuery()->getEngine()->getRepresentative(n),
-          qe->getEqualityQuery()->getEngine());
+      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
       while (!eqc.isFinished())
       {
         Node en = (*eqc);
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index a63954838..c978a6952 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -28,7 +28,6 @@ namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
-class EqualityQuery;
 
 namespace inst {
 
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index d1c09a9e8..c0f294528 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -188,7 +188,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
   std::map<TypeNode, std::vector<Node> > term_db_list;
   std::vector<TypeNode> ftypes;
   TermDb* tdb = d_quantEngine->getTermDatabase();
-  EqualityQuery* qy = d_quantEngine->getEqualityQuery();
+  QuantifiersState& qs = d_quantEngine->getState();
   // iterate over substitutions for variables
   for (unsigned i = 0; i < f[0].getNumChildren(); i++)
   {
@@ -212,7 +212,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
           Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
           if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
           {
-            Node rep = qy->getRepresentative(gt);
+            Node rep = qs.getRepresentative(gt);
             if (reps_found.find(rep) == reps_found.end())
             {
               reps_found[rep] = gt;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index bd7a1b122..4359b8b19 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -589,7 +589,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
           p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
       inst = Rewriter::rewrite(inst);
       Node inst_eval = p->getTermDatabase()->evaluateTerm(
-          inst, nullptr, options::qcfTConstraint(), true);
+          inst, options::qcfTConstraint(), true);
       if( Trace.isOn("qcf-instance-check") ){
         Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
         for( unsigned i=0; i<terms.size(); i++ ){
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b561b589b..6ce46ad99 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -38,22 +38,22 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
 
 eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
 {
-  return d_quantEngine->getMasterEqualityEngine();
+  return d_qstate.getEqualityEngine();
 }
 
 bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
 {
-  return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
+  return d_qstate.areEqual(n1, n2);
 }
 
 bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
 {
-  return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
+  return d_qstate.areDisequal(n1, n2);
 }
 
 TNode QuantifiersModule::getRepresentative(TNode n) const
 {
-  return d_quantEngine->getEqualityQuery()->getRepresentative( n );
+  return d_qstate.getRepresentative(n);
 }
 
 QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 16791b130..417e6820d 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -221,32 +221,6 @@ public:
   static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 };
 
-/** EqualityQuery
-* This is a wrapper class around equality engine.
-*/
-class EqualityQuery : public QuantifiersUtil {
-public:
-  EqualityQuery(){}
-  virtual ~EqualityQuery(){};
-  /** extends engine */
-  virtual bool extendsEngine() { return false; }
-  /** contains term */
-  virtual bool hasTerm( Node a ) = 0;
-  /** get the representative of the equivalence class of a */
-  virtual Node getRepresentative( Node a ) = 0;
-  /** returns true if a and b are equal in the current context */
-  virtual bool areEqual( Node a, Node b ) = 0;
-  /** returns true is a and b are disequal in the current context */
-  virtual bool areDisequal( Node a, Node b ) = 0;
-  /** get the equality engine associated with this query */
-  virtual eq::EqualityEngine* getEngine() = 0;
-  /** get the equivalence class of a */
-  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-  /** get the term that exists in EE that is congruent to f with args (f is
-   * returned by TermDb::getMatchOperator(...)) */
-  virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
-};/* class EqualityQuery */
-
 /** Types of bounds that can be inferred for quantified formulas */
 enum BoundVarType
 {
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 2893fd686..1743cafe5 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -51,12 +51,13 @@ RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
   }
 }
 
-void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) {
+void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
+{
   std::map< Node, Node > rterms;
   for( unsigned i=0; i<d_terms.size(); i++ ){
     Node r = d_terms[i];
     if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
-      r = qe->getEqualityQuery()->getRepresentative( d_terms[i] );
+      r = qs.getRepresentative(d_terms[i]);
     }
     if( rterms.find( r )==rterms.end() ){
       rterms[r] = d_terms[i];
@@ -141,7 +142,7 @@ void RelevantDomain::compute(){
         RDomain * r = it2->second;
         RDomain * rp = r->getParent();
         if( r==rp ){
-          r->removeRedundantTerms( d_qe );
+          r->removeRedundantTerms(d_qe->getState());
           for( unsigned i=0; i<r->d_terms.size(); i++ ){
             Trace("rel-dom") << r->d_terms[i] << " ";
           }
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 6da4ce75a..36364191c 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -84,7 +84,7 @@ class RelevantDomain : public QuantifiersUtil
     /** remove redundant terms for d_terms, removes
      * duplicates modulo equality.
      */
-    void removeRedundantTerms( QuantifiersEngine * qe );
+    void removeRedundantTerms(QuantifiersState& qs);
     /** is n in this relevant domain? */
     bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3f33b07b8..c39654aa5 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -258,7 +258,7 @@ void TermDb::addTerm(Node n,
 void TermDb::computeArgReps( TNode n ) {
   if (d_arg_reps.find(n) == d_arg_reps.end())
   {
-    eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+    eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     for (const TNode& nc : n)
     {
       TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
@@ -281,7 +281,7 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   {
     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
   }
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
   for (TNode ff : ops)
   {
     for (const Node& n : d_op_map[ff])
@@ -316,7 +316,6 @@ void TermDb::computeUfTerms( TNode f ) {
   unsigned nonCongruentCount = 0;
   unsigned alreadyCongruentCount = 0;
   unsigned relevantCount = 0;
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
   for (TNode ff : ops)
   {
@@ -330,7 +329,7 @@ void TermDb::computeUfTerms( TNode f ) {
     for (const Node& n : it->second)
     {
       // to be added to term index, term must be relevant, and exist in EE
-      if (!hasTermCurrent(n) || !ee->hasTerm(n))
+      if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
       {
         Trace("term-db-debug") << n << " is not relevant." << std::endl;
         continue;
@@ -358,20 +357,20 @@ void TermDb::computeUfTerms( TNode f ) {
         }
       }
       Trace("term-db-debug") << std::endl;
-      Assert(ee->hasTerm(n));
-      Trace("term-db-debug") << "  and value : " << ee->getRepresentative(n)
-                             << std::endl;
+      Assert(d_qstate.hasTerm(n));
+      Trace("term-db-debug")
+          << "  and value : " << d_qstate.getRepresentative(n) << std::endl;
       Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
-      Assert(ee->hasTerm(at));
+      Assert(d_qstate.hasTerm(at));
       Trace("term-db-debug2") << "...add term returned " << at << std::endl;
-      if (at != n && ee->areEqual(at, n))
+      if (at != n && d_qstate.areEqual(at, n))
       {
         setTermInactive(n);
         Trace("term-db-debug") << n << " is redundant." << std::endl;
         congruentCount++;
         continue;
       }
-      if (ee->areDisequal(at, n, false))
+      if (d_qstate.areDisequal(at, n))
       {
         std::vector<Node> lits;
         lits.push_back(nm->mkNode(EQUAL, at, n));
@@ -512,9 +511,8 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r)
-         || d_quantEngine->getMasterEqualityEngine()->getRepresentative(r)
-                == r);
+  Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
+         || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
@@ -531,7 +529,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
 Node TermDb::evaluateTerm2(TNode n,
                            std::map<TNode, Node>& visited,
                            std::vector<Node>& exp,
-                           EqualityQuery* qy,
                            bool useEntailmentTests,
                            bool computeExp,
                            bool reqHasTerm)
@@ -546,10 +543,10 @@ Node TermDb::evaluateTerm2(TNode n,
   if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
     //do nothing
   }
-  else if (qy->hasTerm(n))
+  else if (d_qstate.hasTerm(n))
   {
     Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
-    ret = qy->getRepresentative(n);
+    ret = d_qstate.getRepresentative(n);
     if (computeExp)
     {
       if (n != ret)
@@ -570,7 +567,6 @@ Node TermDb::evaluateTerm2(TNode n,
       TNode c = evaluateTerm2(n[i],
                               visited,
                               tempExp,
-                              qy,
                               useEntailmentTests,
                               computeExp,
                               reqHasTerm);
@@ -595,7 +591,6 @@ Node TermDb::evaluateTerm2(TNode n,
           ret = evaluateTerm2(n[c == d_true ? 1 : 2],
                               visited,
                               tempExp,
-                              qy,
                               useEntailmentTests,
                               computeExp,
                               reqHasTerm);
@@ -628,7 +623,7 @@ Node TermDb::evaluateTerm2(TNode n,
       if (!f.isNull())
       {
         // if f is congruent to a term indexed by this class
-        TNode nn = qy->getCongruentTerm(f, args);
+        TNode nn = getCongruentTerm(f, args);
         Trace("term-db-eval") << "  got congruent term " << nn
                               << " from DB for " << n << std::endl;
         if (!nn.isNull())
@@ -644,7 +639,7 @@ Node TermDb::evaluateTerm2(TNode n,
               }
             }
           }
-          ret = qy->getRepresentative(nn);
+          ret = d_qstate.getRepresentative(nn);
           Trace("term-db-eval") << "return rep" << std::endl;
           ret_set = true;
           reqHasTerm = false;
@@ -669,7 +664,7 @@ Node TermDb::evaluateTerm2(TNode n,
         ret = Rewriter::rewrite(ret);
         if (ret.getKind() == EQUAL)
         {
-          if (qy->areDisequal(ret[0], ret[1]))
+          if (d_qstate.areDisequal(ret[0], ret[1]))
           {
             ret = d_false;
           }
@@ -706,7 +701,7 @@ Node TermDb::evaluateTerm2(TNode n,
     if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
         && k != FORALL)
     {
-      if (!qy->hasTerm(ret))
+      if (!d_qstate.hasTerm(ret))
       {
         ret = Node::null();
       }
@@ -723,11 +718,14 @@ Node TermDb::evaluateTerm2(TNode n,
   return ret;
 }
 
-
-TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
-  Assert(!qy->extendsEngine());
+TNode TermDb::getEntailedTerm2(TNode n,
+                               std::map<TNode, TNode>& subs,
+                               bool subsRep,
+                               bool hasSubs)
+{
   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
-  if( qy->getEngine()->hasTerm( n ) ){
+  if (d_qstate.hasTerm(n))
+  {
     Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
     return n;
   }else if( n.getKind()==BOUND_VARIABLE ){
@@ -736,18 +734,18 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
       if( it!=subs.end() ){
         Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
         if( subsRep ){
-          Assert(qy->getEngine()->hasTerm(it->second));
-          Assert(qy->getEngine()->getRepresentative(it->second) == it->second);
+          Assert(d_qstate.hasTerm(it->second));
+          Assert(d_qstate.getRepresentative(it->second) == it->second);
           return it->second;
-        }else{
-          return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
         }
+        return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
       }
     }
   }else if( n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
-      if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
-        return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
+      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
+      {
+        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
       }
     }
   }else{
@@ -756,15 +754,15 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
       if( !f.isNull() ){
         std::vector< TNode > args;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
+          TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
           if( c.isNull() ){
             return TNode::null();
           }
-          c = qy->getEngine()->getRepresentative( c );
+          c = d_qstate.getRepresentative(c);
           Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
           args.push_back( c );
         }
-        TNode nn = qy->getCongruentTerm( f, args );
+        TNode nn = getCongruentTerm(f, args);
         Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
         return nn;
       }
@@ -774,77 +772,66 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
 }
 
 Node TermDb::evaluateTerm(TNode n,
-                          EqualityQuery* qy,
                           bool useEntailmentTests,
                           bool reqHasTerm)
 {
-  if( qy==NULL ){
-    qy = d_quantEngine->getEqualityQuery();
-  }
   std::map< TNode, Node > visited;
   std::vector<Node> exp;
-  return evaluateTerm2(
-      n, visited, exp, qy, useEntailmentTests, false, reqHasTerm);
+  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
 }
 
 Node TermDb::evaluateTerm(TNode n,
                           std::vector<Node>& exp,
-                          EqualityQuery* qy,
                           bool useEntailmentTests,
                           bool reqHasTerm)
 {
-  if (qy == NULL)
-  {
-    qy = d_quantEngine->getEqualityQuery();
-  }
   std::map<TNode, Node> visited;
-  return evaluateTerm2(
-      n, visited, exp, qy, useEntailmentTests, true, reqHasTerm);
+  return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
 }
 
-TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
-  if( qy==NULL ){
-    qy = d_quantEngine->getEqualityQuery();
-  }
-  return getEntailedTerm2( n, subs, subsRep, true, qy );
+TNode TermDb::getEntailedTerm(TNode n,
+                              std::map<TNode, TNode>& subs,
+                              bool subsRep)
+{
+  return getEntailedTerm2(n, subs, subsRep, true);
 }
 
-TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
-  if( qy==NULL ){
-    qy = d_quantEngine->getEqualityQuery();
-  }
+TNode TermDb::getEntailedTerm(TNode n)
+{
   std::map< TNode, TNode > subs;
-  return getEntailedTerm2( n, subs, false, false, qy );
+  return getEntailedTerm2(n, subs, false, false);
 }
 
-bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
-  Assert(!qy->extendsEngine());
+bool TermDb::isEntailed2(
+    TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
+{
   Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
   Assert(n.getType().isBoolean());
   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
-    TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
+    TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
     if( !n1.isNull() ){
-      TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
+      TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
       if( !n2.isNull() ){
         if( n1==n2 ){
           return pol;
         }else{
-          Assert(qy->getEngine()->hasTerm(n1));
-          Assert(qy->getEngine()->hasTerm(n2));
+          Assert(d_qstate.hasTerm(n1));
+          Assert(d_qstate.hasTerm(n2));
           if( pol ){
-            return qy->getEngine()->areEqual( n1, n2 );
+            return d_qstate.areEqual(n1, n2);
           }else{
-            return qy->getEngine()->areDisequal( n1, n2, false );
+            return d_qstate.areDisequal(n1, n2);
           }
         }
       }
     }
   }else if( n.getKind()==NOT ){
-    return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
+    return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
   }else if( n.getKind()==OR || n.getKind()==AND ){
     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
+      if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
+      {
         if( simPol ){
           return true;
         }
@@ -858,45 +845,45 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   //Boolean equality here
   }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
-      if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
+      {
         unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
+        return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
       }
     }
   }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
+    TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
     if( !n1.isNull() ){
-      Assert(qy->hasTerm(n1));
+      Assert(d_qstate.hasTerm(n1));
       if( n1==d_true ){
         return pol;
       }else if( n1==d_false ){
         return !pol;
       }else{
-        return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
+        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
       }
     }
   }else if( n.getKind()==FORALL && !pol ){
-    return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
+    return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
   }
   return false;
 }
 
-bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
-  if( qy==NULL ){
-    Assert(d_consistent_ee);
-    qy = d_quantEngine->getEqualityQuery();
-  }
+bool TermDb::isEntailed(TNode n, bool pol)
+{
+  Assert(d_consistent_ee);
   std::map< TNode, TNode > subs;
-  return isEntailed2( n, subs, false, false, pol, qy );
+  return isEntailed2(n, subs, false, false, pol);
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
-  if( qy==NULL ){
-    Assert(d_consistent_ee);
-    qy = d_quantEngine->getEqualityQuery();
-  }
-  return isEntailed2( n, subs, subsRep, true, pol, qy );
+bool TermDb::isEntailed(TNode n,
+                        std::map<TNode, TNode>& subs,
+                        bool subsRep,
+                        bool pol)
+{
+  Assert(d_consistent_ee);
+  return isEntailed2(n, subs, subsRep, true, pol);
 }
 
 bool TermDb::isTermActive( Node n ) {
@@ -971,8 +958,8 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
     std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
     if( it==d_term_elig_eqc.end() ){
       Node h;
-      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+      eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
       while (!eqc_i.isFinished())
       {
         TNode n = (*eqc_i);
@@ -1025,7 +1012,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
 
   Assert(ee->consistent());
   // if higher-order, add equalities for the purification terms now
@@ -1083,7 +1070,7 @@ bool TermDb::reset( Theory::Effort effort ){
       bool addedFirst = false;
       Node first;
       //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
       while( !eqc_i.isFinished() ){
         TNode n = (*eqc_i);
         if( first.isNull() ){
@@ -1125,8 +1112,9 @@ bool TermDb::reset( Theory::Effort effort ){
   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
   for (const Node& n : d_iclosure_processed)
   {
-    if( !ee->hasTerm( n ) ){
-      ee->addTerm( n );
+    if (!ee->hasTerm(n))
+    {
+      ee->addTerm(n);
     }
   }
 
@@ -1141,7 +1129,7 @@ bool TermDb::reset( Theory::Effort effort ){
       if( r.getType().isFunction() ){
         Trace("quant-ho") << "  process function eqc " << r << std::endl;
         Node first;
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
         while( !eqc_i.isFinished() ){
           TNode n = (*eqc_i);
           Node n_use;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index c246ea6fc..244762d24 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -31,22 +31,9 @@ namespace theory {
 
 class QuantifiersEngine;
 
-namespace inst{
-  class Trigger;
-  class HigherOrderTrigger;
-}
-
 namespace quantifiers {
 
-namespace fmcheck {
-  class FullModelChecker;
-}
-
-class TermDbSygus;
-class QuantConflictFind;
-class RelevantDomain;
 class ConjectureGenerator;
-class TermGenerator;
 class TermGenEnv;
 
 /** Term Database
@@ -182,9 +169,9 @@ class TermDb : public QuantifiersUtil {
   /** evaluate term
    *
    * Returns a term n' such that n = n' is entailed based on the equality
-   * information qy.  This function may generate new terms. In particular,
+   * information ee.  This function may generate new terms. In particular,
    * we typically rewrite subterms of n of maximal size to terms that exist in
-   * the equality engine specified by qy.
+   * the equality engine specified by ee.
    *
    * useEntailmentTests is whether to call the theory engine's entailmentTest
    * on literals n for which this call fails to find a term n' that is
@@ -204,59 +191,53 @@ class TermDb : public QuantifiersUtil {
    */
   Node evaluateTerm(TNode n,
                     std::vector<Node>& exp,
-                    EqualityQuery* qy = NULL,
                     bool useEntailmentTests = false,
                     bool reqHasTerm = false);
   /** same as above, without exp */
   Node evaluateTerm(TNode n,
-                    EqualityQuery* qy = NULL,
                     bool useEntailmentTests = false,
                     bool reqHasTerm = false);
   /** get entailed term
    *
-  * If possible, returns a term n' such that:
-  * (1) n' exists in the current equality engine (as specified by qy),
-  * (2) n = n' is entailed in the current context.
-  * It returns null if no such term can be found.
-  * Wrt evaluateTerm, this version does not construct new terms, and
-  * thus is less aggressive.
-  */
-  TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n = n' is entailed in the current context.
+   * It returns null if no such term can be found.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n);
   /** get entailed term
    *
-  * If possible, returns a term n' such that:
-  * (1) n' exists in the current equality engine (as specified by qy),
-  * (2) n * subs = n' is entailed in the current context, where * is denotes
-  * substitution application.
-  * It returns null if no such term can be found.
-  * subsRep is whether the substitution maps to terms that are representatives
-  * according to qy.
-  * Wrt evaluateTerm, this version does not construct new terms, and
-  * thus is less aggressive.
-  */
-  TNode getEntailedTerm(TNode n,
-                        std::map<TNode, TNode>& subs,
-                        bool subsRep,
-                        EqualityQuery* qy = NULL);
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n * subs = n' is entailed in the current context, where * denotes
+   * substitution application.
+   * It returns null if no such term can be found.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to the quantifiers state.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
   /** is entailed
-  * Checks whether the current context entails n with polarity pol, based on the
-  * equality information qy.
-  * Returns true if the entailment can be successfully shown.
-  */
-  bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL);
+   * Checks whether the current context entails n with polarity pol, based on
+   * the equality information in the quantifiers state. Returns true if the
+   * entailment can be successfully shown.
+   */
+  bool isEntailed(TNode n, bool pol);
   /** is entailed
    *
-  * Checks whether the current context entails ( n * subs ) with polarity pol,
-  * based on the equality information qy,
-  * where * denotes substitution application.
-  * subsRep is whether the substitution maps to terms that are representatives
-  * according to qy.
-  */
+   * Checks whether the current context entails ( n * subs ) with polarity pol,
+   * based on the equality information in the quantifiers state,
+   * where * denotes substitution application.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to in the quantifiers state.
+   */
   bool isEntailed(TNode n,
                   std::map<TNode, TNode>& subs,
                   bool subsRep,
-                  bool pol,
-                  EqualityQuery* qy = NULL);
+                  bool pol);
   /** is the term n active in the current context?
    *
   * By default, all terms are active. A term is inactive if:
@@ -354,14 +335,20 @@ class TermDb : public QuantifiersUtil {
   Node evaluateTerm2(TNode n,
                      std::map<TNode, Node>& visited,
                      std::vector<Node>& exp,
-                     EqualityQuery* qy,
                      bool useEntailmentTests,
                      bool computeExp,
                      bool reqHasTerm);
   /** helper for get entailed term */
-  TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+  TNode getEntailedTerm2(TNode n,
+                         std::map<TNode, TNode>& subs,
+                         bool subsRep,
+                         bool hasSubs);
   /** helper for is entailed */
-  bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
+  bool isEntailed2(TNode n,
+                   std::map<TNode, TNode>& subs,
+                   bool subsRep,
+                   bool hasSubs,
+                   bool pol);
   /** compute uf eqc terms :
   * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
   */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 4dd59d12f..1cbb2ce40 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -83,6 +83,13 @@ void TheoryQuantifiers::finishInit()
   d_valuation.setUnevaluatedKind(WITNESS);
 }
 
+bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi)
+{
+  // use the master equality engine
+  esi.d_useMaster = true;
+  return true;
+}
+
 void TheoryQuantifiers::preRegisterTerm(TNode n)
 {
   if (n.getKind() != FORALL)
@@ -164,7 +171,7 @@ bool TheoryQuantifiers::preNotifyFact(
     getQuantifiersEngine()->addTermToDatabase(atom[0], false, true);
     if (!options::lteRestrictInstClosure())
     {
-      getQuantifiersEngine()->getMasterEqualityEngine()->addTerm(atom[0]);
+      d_qstate.getEqualityEngine()->addTerm(atom[0]);
     }
   }
   else
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 8d2366065..2283d5ea8 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -47,6 +47,8 @@ class TheoryQuantifiers : public Theory {
   TheoryRewriter* getTheoryRewriter() override;
   /** finish initialization */
   void finishInit() override;
+  /** needs equality engine */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
   //--------------------------------- end initialization
 
   void preRegisterTerm(TNode n) override;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7cec8721c..2cc904ed1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -39,7 +39,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_qim(qim),
       d_te(nullptr),
       d_decManager(nullptr),
-      d_masterEqualityEngine(nullptr),
       d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
@@ -120,13 +119,10 @@ QuantifiersEngine::QuantifiersEngine(
 
 QuantifiersEngine::~QuantifiersEngine() {}
 
-void QuantifiersEngine::finishInit(TheoryEngine* te,
-                                   DecisionManager* dm,
-                                   eq::EqualityEngine* mee)
+void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
 {
   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_qstate, d_qim, d_modules);
@@ -147,12 +143,16 @@ OutputChannel& QuantifiersEngine::getOutputChannel()
 {
   return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
 }
-/** get default valuation for the quantifiers engine */
 Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
 
-EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+quantifiers::QuantifiersState& QuantifiersEngine::getState()
 {
-  return d_eq_query.get();
+  return d_qstate;
+}
+quantifiers::QuantifiersInferenceManager&
+QuantifiersEngine::getInferenceManager()
+{
+  return d_qim;
 }
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
@@ -352,8 +352,8 @@ void QuantifiersEngine::ppNotifyAssertions(
 
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_statistics.d_time);
-
-  if (!getMasterEqualityEngine()->consistent())
+  Assert(d_qstate.getEqualityEngine() != nullptr);
+  if (!d_qstate.getEqualityEngine()->consistent())
   {
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
@@ -885,8 +885,6 @@ bool QuantifiersEngine::hasAddedLemma() const
   return !d_lemmas_waiting.empty() || d_hasAddedLemma;
 }
 
-bool QuantifiersEngine::inConflict() const { return d_qstate.isInConflict(); }
-
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
@@ -1067,11 +1065,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
 }
 
-eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
-{
-  return d_masterEqualityEngine;
-}
-
 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
   return d_eq_query->getInternalRepresentative(a, q, index);
 }
@@ -1100,7 +1093,7 @@ bool QuantifiersEngine::getSynthSolutions(
 }
 
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
-  eq::EqualityEngine* ee = getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   std::map< TypeNode, int > typ_num;
   while( !eqcs_i.isFinished() ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 126fca01f..74f432585 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -73,12 +73,12 @@ class QuantifiersEngine {
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
+  /** The quantifiers state object */
+  quantifiers::QuantifiersState& getState();
+  /** The quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& getInferenceManager();
   //---------------------- end external interface
   //---------------------- utilities
-  /** get the master equality engine */
-  eq::EqualityEngine* getMasterEqualityEngine() const;
-  /** get equality query */
-  EqualityQuery* getEqualityQuery() const;
   /** get the model builder */
   quantifiers::QModelBuilder* getModelBuilder() const;
   /** get model */
@@ -110,11 +110,8 @@ class QuantifiersEngine {
    *
    * @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);
+  void finishInit(TheoryEngine* te, DecisionManager* dm);
   //---------------------- end private initialization
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -227,8 +224,6 @@ public:
  void markRelevant(Node q);
  /** has added lemma */
  bool hasAddedLemma() const;
- /** is in conflict */
- bool inConflict() const;
  /** get current q effort */
  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
  /** get number of waiting lemmas */
@@ -343,8 +338,6 @@ public:
   TheoryEngine* d_te;
   /** Reference to the decision manager of the theory engine */
   DecisionManager* d_decManager;
-  /** Pointer to the master equality engine */
-  eq::EqualityEngine* d_masterEqualityEngine;
   /** vector of utilities for quantifiers */
   std::vector<QuantifiersUtil*> d_util;
   /** vector of modules for quantifiers */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ba65fe69d..18d9bb572 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -183,8 +183,7 @@ void TheoryEngine::finishInit()
   // finish initializing the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->finishInit(
-        this, d_decManager.get(), d_tc->getCoreEqualityEngine());
+    d_quantEngine->finishInit(this, d_decManager.get());
   }
 
   // finish initializing the theories by linking them with the appropriate
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 47528e1a6..e145baa6a 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -119,6 +119,26 @@ bool TheoryState::areDisequal(TNode a, TNode b) const
   return d_ee->areDisequal(a, b, false);
 }
 
+void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
+{
+  if (d_ee->hasTerm(a))
+  {
+    Node rep = d_ee->getRepresentative(a);
+    eq::EqClassIterator eqc_iter(rep, d_ee);
+    while (!eqc_iter.isFinished())
+    {
+      eqc.push_back(*eqc_iter);
+      eqc_iter++;
+    }
+  }
+  else
+  {
+    eqc.push_back(a);
+  }
+  // a should be in its equivalence class
+  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
+}
+
 eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
 
 void TheoryState::notifyInConflict() { d_conflict = true; }
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 7c2a044bf..891016f0a 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -60,6 +60,8 @@ class TheoryState
    * returns true if the representative of a and b are distinct constants.
    */
   virtual bool areDisequal(TNode a, TNode b) const;
+  /** get list of members in the equivalence class of a */
+  virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const;
   /** get equality engine */
   eq::EqualityEngine* getEqualityEngine() const;
   //-------------------------------------- end equality information