More preparation for filtering relevant terms in TermDb.

4 files changed, 73 insertions, 27 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 871d4ddc6..06552196d 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -416,8 +416,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );

         while( !ieqc_i.isFinished() ){

           TNode n = (*ieqc_i);

-          if( isHandledTerm( n ) ){

-            d_op_arg_index[r].addTerm( this, n );

+          if( getTermDatabase()->hasTermCurrent( n ) ){

+            if( isHandledTerm( n ) ){

+              d_op_arg_index[r].addTerm( this, n );

+            }

           }

           ++ieqc_i;

         }

@@ -472,7 +474,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );

           while( !eqc_i.isFinished() ){

             TNode n = (*eqc_i);

-            if( !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){

+            if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){

               if( firstTime ){

                 Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;

                 firstTime = false;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 768ba63de..d465df4c0 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -458,8 +458,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
     //check constraints

     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){

       //apply substitution to the tconstraint

-      Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),

-                                        p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),

+      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),

+                                        p->getTermDatabase()->d_vars[d_q].end(),

                                         terms.begin(), terms.end() );

       cons = it->second ? cons : cons.negate();

       if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){

@@ -1300,7 +1300,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
       if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){

         d_matched_basis = true;

         Node f = getOperator( d_n );

-        TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );

+        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );

         if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){

           success = true;

           d_qni_bound[0] = d_qni_var_num[0];

@@ -1662,7 +1662,7 @@ bool MatchGen::isHandledUfTerm( TNode n ) {
 

 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

   if( isHandledUfTerm( n ) ){

-    return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );

+    return p->getTermDatabase()->getOperator( n );

   }else{

     return Node::null();

   }

@@ -2087,26 +2087,28 @@ void QuantConflictFind::computeRelevantEqr() {
     while( !eqcs_i.isFinished() ){

       //nEqc++;

       Node r = (*eqcs_i);

-      TypeNode rtn = r.getType();

-      if( options::qcfMode()==QCF_MC ){

-        std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );

-        if( itt==d_eqcs.end() ){

-          Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );

-          if( !getEqualityEngine()->hasTerm( mb ) ){

-            Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;

-            Assert( false );

-          }

-          Node mbr = getRepresentative( mb );

-          if( mbr!=r ){

-            d_eqcs[rtn].push_back( mbr );

+      if( getTermDatabase()->hasTermCurrent( r ) ){

+        TypeNode rtn = r.getType();

+        if( options::qcfMode()==QCF_MC ){

+          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );

+          if( itt==d_eqcs.end() ){

+            Node mb = getTermDatabase()->getModelBasisTerm( rtn );

+            if( !getEqualityEngine()->hasTerm( mb ) ){

+              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;

+              Assert( false );

+            }

+            Node mbr = getRepresentative( mb );

+            if( mbr!=r ){

+              d_eqcs[rtn].push_back( mbr );

+            }

+            d_eqcs[rtn].push_back( r );

+            d_model_basis[rtn] = mb;

+          }else{

+            itt->second.push_back( r );

           }

-          d_eqcs[rtn].push_back( r );

-          d_model_basis[rtn] = mb;

         }else{

-          itt->second.push_back( r );

+          d_eqcs[rtn].push_back( r );

         }

-      }else{

-        d_eqcs[rtn].push_back( r );

       }

       ++eqcs_i;

     }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ee39b55d9..b21494f77 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -322,6 +322,21 @@ bool TermDb::hasTermCurrent( Node n ) {
   return true;
 }
 
+void TermDb::setHasTerm( Node n ) {
+  if( inst::Trigger::isAtomicTrigger( n ) ){
+    if( d_has_map.find( n )==d_has_map.end() ){
+      d_has_map[n] = true;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        setHasTerm( n[i] );
+      }
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      setHasTerm( n[i] );
+    }
+  }
+}
+
 void TermDb::reset( Theory::Effort effort ){
   int nonCongruentCount = 0;
   int congruentCount = 0;
@@ -331,21 +346,45 @@ void TermDb::reset( Theory::Effort effort ){
   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);
+    bool addedFirst = false;
+    Node first;
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
     while( !eqc_i.isFinished() ){
-      d_has_map[(*eqc_i)] = true;
+      TNode n = (*eqc_i);
+      if( first.isNull() ){
+        first = n;
+      }else{
+        if( !addedFirst ){
+          addedFirst = true;
+          setHasTerm( first );
+        }
+        setHasTerm( n );
+      }
       ++eqc_i;
     }
     ++eqcs_i;
   }
+  for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+    Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
+    if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
+      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+      for (unsigned i = 0; it != it_end; ++ it, ++i) {
+        Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl;
+        setHasTerm( (*it).assertion );
+      }
+    }
+  }
   */
+  
+  
   //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;
@@ -370,6 +409,7 @@ void TermDb::reset( Theory::Effort effort ){
             alreadyCongruentCount++;
           }
         }else{
+          Trace("term-db-stats-debug") << n << " is not relevant." << std::endl;
           nonRelevantCount++;
         }
       }
@@ -377,7 +417,7 @@ void TermDb::reset( Theory::Effort effort ){
   }
   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;
+  Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << 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 ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3d419ed5c..4dca6b36c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -128,6 +128,8 @@ private:
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** count number of ground terms per operator (user-context dependent) */
   NodeIntMap d_op_ccount;
+  /** set has term */
+  void setHasTerm( Node n );
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}