Work on synchronizing decision=justification and E-matching.

3 files changed, 82 insertions, 51 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 29640e18f..a10181c51 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -101,10 +101,11 @@ Node CandidateGeneratorQE::getNextCandidate(){
     //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];
-      //Assert( d_qe->getEqualityQuery()->hasTerm( n ) );
       d_term_iter++;
       if( isLegalCandidate( n ) ){
-        return n;
+        if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+          return n;
+        }
       }
     }
   }else if( d_mode==cand_term_eqc ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c35adef6a..ee39b55d9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -124,7 +124,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     if( inst::Trigger::isAtomicTrigger( n ) ){
       if( !TermDb::hasInstConstAttr(n) ){
         Trace("term-db") << "register term in db " << n << std::endl;
-        //std::cout << "register trigger term " << n << std::endl;
         Node op = getOperator( n );
         /*
         int occ = d_op_ccount[op];
@@ -174,10 +173,12 @@ void TermDb::computeUfEqcTerms( TNode f ) {
     eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
     for( unsigned i=0; i<d_op_map[f].size(); i++ ){
       TNode n = d_op_map[f][i];
-      if( !n.getAttribute(NoMatchAttribute()) ){
-        computeArgReps( n );
-        TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
-        d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
+      if( hasTermCurrent( n ) ){
+        if( !n.getAttribute(NoMatchAttribute()) ){
+          computeArgReps( n );
+          TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
+          d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
+        }
       }
     }
   }
@@ -315,52 +316,77 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   return false;
 }
 
+bool TermDb::hasTermCurrent( Node n ) { 
+  //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n );
+  //return d_has_map.find( n )!=d_has_map.end(); 
+  return true;
+}
+
 void TermDb::reset( Theory::Effort effort ){
-   int nonCongruentCount = 0;
-   int congruentCount = 0;
-   int alreadyCongruentCount = 0;
-   d_op_nonred_count.clear();
-   d_arg_reps.clear();
-   d_func_map_trie.clear();
-   d_func_map_eqc_trie.clear();
-   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
-   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-     d_op_nonred_count[ it->first ] = 0;
-     if( !it->second.empty() ){
-       for( unsigned i=0; i<it->second.size(); i++ ){
-         Node n = it->second[i];
-         //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) );
-         computeModelBasisArgAttribute( n );
-         if( !n.getAttribute(NoMatchAttribute()) ){
-           computeArgReps( n );
-           if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
-             NoMatchAttribute nma;
-             n.setAttribute(nma,true);
-             Debug("term-db-cong") << n << " is redundant." << std::endl;
-             congruentCount++;
-           }else{
-             nonCongruentCount++;
-             d_op_nonred_count[ it->first ]++;
-           }
-         }else{
-           congruentCount++;
-           alreadyCongruentCount++;
-         }
-       }
-     }
-   }
-   Debug("term-db-cong") << "TermDb: Reset" << std::endl;
-   Debug("term-db-cong") << "Congruent/Non-Congruent = ";
-   Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
-   if( Debug.isOn("term-db") ){
-      Debug("term-db") << "functions : " << std::endl;
-      for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-        if( it->second.size()>0 ){
-          Debug("term-db") << "- " << it->first << std::endl;
-          d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+  int nonCongruentCount = 0;
+  int congruentCount = 0;
+  int alreadyCongruentCount = 0;
+  int nonRelevantCount = 0;
+  d_op_nonred_count.clear();
+  d_arg_reps.clear();
+  d_func_map_trie.clear();
+  d_func_map_eqc_trie.clear();
+  /*
+  //compute has map
+  d_has_map.clear();
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    TNode r = (*eqcs_i);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+    while( !eqc_i.isFinished() ){
+      d_has_map[(*eqc_i)] = true;
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+  */
+  //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
+  for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
+    d_op_nonred_count[ it->first ] = 0;
+    if( !it->second.empty() ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        computeModelBasisArgAttribute( n );
+        if( hasTermCurrent( n ) ){
+          if( !n.getAttribute(NoMatchAttribute()) ){
+            computeArgReps( n );
+            if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
+              NoMatchAttribute nma;
+              n.setAttribute(nma,true);
+              Trace("term-db-stats-debug") << n << " is redundant." << std::endl;
+              congruentCount++;
+            }else{
+              nonCongruentCount++;
+              d_op_nonred_count[ it->first ]++;
+            }
+          }else{
+            congruentCount++;
+            alreadyCongruentCount++;
+          }
+        }else{
+          nonRelevantCount++;
         }
       }
-   }
+    }
+  }
+  Trace("term-db-stats") << "TermDb: Reset" << std::endl;
+  Trace("term-db-stats") << "Congruent/Non-Congruent/Non-Relevant = ";
+  Trace("term-db-stats") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << " / " << nonRelevantCount << std::endl;
+  if( Debug.isOn("term-db") ){
+    Debug("term-db") << "functions : " << std::endl;
+    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
+      if( it->second.size()>0 ){
+        Debug("term-db") << "- " << it->first << std::endl;
+        d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+      }
+    }
+  }
 }
 
 TermArgTrie * TermDb::getTermArgTrie( Node f ) {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1d3757d65..3d419ed5c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -140,6 +140,8 @@ public:
   std::map< Node, int > d_op_nonred_count;
   /** map from APPLY_UF operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
+  /** has map */
+  std::map< Node, bool > d_has_map;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
@@ -170,7 +172,9 @@ public:
   TNode evaluateTerm( TNode n );
   /** is entailed (incomplete check) */
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
-
+  /** has term */
+  bool hasTermCurrent( Node n );
+  
 //for model basis
 private:
   //map from types to model basis terms