fixed assertion failures in efficient e-matching

diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp
index b9d19d391224d5e27479b1a48311aa616578fa1b..482e460ce7c1c4817dd305e3cbf0ff637b435998 100755 (executable)
--- a/src/theory/rewriterules/efficient_e_matching.cpp
+++ b/src/theory/rewriterules/efficient_e_matching.cpp
@@ -193,7 +193,7 @@ EqClassInfo* EfficientEMatcher::getEquivalenceClassInfo( Node n ) {
   return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];\r
 }\r
 EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){\r
-  Assert( n==d_quantEngine->getEqualityQuery()->getRepresentative( n ) );\r
+  Assert( n==d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ) );\r
   if( d_eqc_ops.find( n )==d_eqc_ops.end() ){\r
     EqClassInfo* eci = new EqClassInfo( d_quantEngine->getSatContext() );\r
     eci->setMember( n, d_quantEngine->getTermDatabase() );\r
@@ -319,7 +319,7 @@ void EfficientEMatcher::computeCandidatesConstants( Node a, EqClassInfo* eci_a,
        itc != end; ++itc ) {\r
       //The constant\r
       Debug("efficient-e-match") << "    Checking constant " << a << std::endl;\r
-      if(d_quantEngine->getEqualityQuery()->getRepresentative(itc->first) != a) continue;\r
+      if(d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(itc->first) != a) continue;\r
       SetNode s;\r
       eq::EqClassIterator eqc_iter( b, d_quantEngine->getEqualityQuery()->getEngine() );\r
       while( !eqc_iter.isFinished() ){\r
@@ -376,7 +376,7 @@ bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode
   bool addedTerm = false;\r
 \r
   if( modEq && d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n )){\r
-    Assert( d_quantEngine->getEqualityQuery()->getRepresentative( n )==n );\r
+    Assert( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n )==n );\r
     //collect modulo equality\r
     //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it\r
     eq::EqClassIterator eqc_iter( n, d_quantEngine->getEqualityQuery()->getEngine() );\r
@@ -399,7 +399,7 @@ bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode
     for( size_t i=0; i<parents.size(); ++i ){\r
       TNode t = parents[i];\r
       if(!CandidateGenerator::isLegalCandidate(t)) continue;\r
-      if( addRep ) t = d_quantEngine->getEqualityQuery()->getRepresentative( t );\r
+      if( addRep ) t = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( t );\r
       terms.insert(t);\r
       addedTerm = true;\r
     }\r
@@ -617,7 +617,7 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler,
   } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){\r
     Node cst = NodeManager::currentNM()->mkConst<bool>(false);\r
     TNode op = pats[0][0].getOperator();\r
-    cst = d_quantEngine->getEqualityQuery()->getRepresentative(cst);\r
+    cst = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(cst);\r
     SetNode ele;\r
     eq::EqClassIterator eqc_iter( cst, d_quantEngine->getEqualityQuery()->getEngine() );\r
     while( !eqc_iter.isFinished() ){\r
@@ -653,7 +653,7 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler,
 \r
 void EfficientEMatcher::outputEqClass( const char* c, Node n ){\r
   if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){\r
-    eq::EqClassIterator eqc_iter( d_quantEngine->getEqualityQuery()->getRepresentative( n ),\r
+    eq::EqClassIterator eqc_iter( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ),\r
                                   d_quantEngine->getEqualityQuery()->getEngine() );\r
     bool firstTime = true;\r
     while( !eqc_iter.isFinished() ){\r