1 files changed, 7 insertions, 67 deletions

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 ){