Performance optimization for E-matching, working on using QCF module for propagations.

1 files changed, 44 insertions, 22 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 783f6284d..60fa672b3 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -68,35 +68,57 @@ void CandidateGeneratorQE::resetInstantiationRound(){
 void CandidateGeneratorQE::reset( Node eqc ){
   d_term_iter = 0;
   if( eqc.isNull() ){
-    d_using_term_db = true;
+    d_mode = cand_term_db;
   }else{
     //create an equivalence class iterator in eq class eqc
-    d_eqc.clear();
-    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
-    d_using_term_db = false;
+    //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
+
+    eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+    if( ee->hasTerm( eqc ) ){
+      Node rep = ee->getRepresentative( eqc );
+      d_eqc_iter = eq::EqClassIterator( rep, ee );
+      d_mode = cand_term_eqc;
+    }else{
+      d_n = eqc;
+      d_mode = cand_term_ident;
+    }
+    //a should be in its equivalence class
+    //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+  }
+}
+bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
+  if( n.hasOperator() && n.getOperator()==d_op ){
+    if( isLegalCandidate( n ) ){
+      return true;
+    }
   }
+  return false;
 }
 
 Node CandidateGeneratorQE::getNextCandidate(){
-  if( d_term_iter>=0 ){
-    if( d_using_term_db ){
-      //get next candidate term in the uf term database
-      while( d_term_iter<d_term_iter_limit ){
-        Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
-        d_term_iter++;
-        if( isLegalCandidate( n ) ){
-          return n;
-        }
+  if( d_mode==cand_term_db ){
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        return n;
       }
-    }else{
-      while( d_term_iter<(int)d_eqc.size() ){
-        Node n = d_eqc[d_term_iter];
-        d_term_iter++;
-        if( n.hasOperator() && n.getOperator()==d_op ){
-          if( isLegalCandidate( n ) ){
-            return n;
-          }
-        }
+    }
+  }else if( d_mode==cand_term_eqc ){
+    while( !d_eqc_iter.isFinished() ){
+      Node n = *d_eqc_iter;
+      ++d_eqc_iter;
+      if( isLegalOpCandidate( n ) ){
+        return n;
+      }
+    }
+  }else if( d_mode==cand_term_ident ){
+    if( !d_n.isNull() ){
+      Node n = d_n;
+      d_n = Node::null();
+      if( isLegalOpCandidate( n ) ){
+        return n;
       }
     }
   }