1 files changed, 0 insertions, 21 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 060994379..8136bf11e 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1851,27 +1851,6 @@ void QuantConflictFind::assertNode( Node q ) {
   }
 }
 
-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
-  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
-  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-}
-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
-}
-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
-  return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
-}
-Node QuantConflictFind::getRepresentative( Node n ) {
-  if( getEqualityEngine()->hasTerm( n ) ){
-    return getEqualityEngine()->getRepresentative( n );
-  }else{
-    return n;
-  }
-}
-TermDb* QuantConflictFind::getTermDatabase() { 
-  return d_quantEngine->getTermDatabase();
-}
-
 Node QuantConflictFind::evaluateTerm( Node n ) {
   if( MatchGen::isHandledUfTerm( n ) ){
     Node f = MatchGen::getOperator( this, n );