From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Nov 2014 09:43:57 +0000 (+0100)
Subject: More preparation for filtering relevant terms in TermDb.
X-Git-Tag: cvc5-1.0.0~6500
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e761324a33a993ae9a268bc2d2ed46f7e86b42d;p=cvc5.git

More preparation for filtering relevant terms in TermDb.
---

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(){}