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 871d4ddc65f99dde4116168d3a82e0f87a9636fc..06552196d8049713f1cdac168a03d7aafa261a95 100755 (executable)
--- 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 );\r
         while( !ieqc_i.isFinished() ){\r
           TNode n = (*ieqc_i);\r
-          if( isHandledTerm( n ) ){\r
-            d_op_arg_index[r].addTerm( this, n );\r
+          if( getTermDatabase()->hasTermCurrent( n ) ){\r
+            if( isHandledTerm( n ) ){\r
+              d_op_arg_index[r].addTerm( this, n );\r
+            }\r
           }\r
           ++ieqc_i;\r
         }\r
@@ -472,7 +474,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );\r
           while( !eqc_i.isFinished() ){\r
             TNode n = (*eqc_i);\r
-            if( !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){\r
+            if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){\r
               if( firstTime ){\r
                 Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;\r
                 firstTime = false;\r

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 768ba63dec6f5f6e814f38dc8a193e88fb4ee6ae..d465df4c0acea1c1ef5d16e914167ec48f61f064 100755 (executable)
--- 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\r
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){\r
       //apply substitution to the tconstraint\r
-      Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),\r
-                                        p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),\r
+      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),\r
+                                        p->getTermDatabase()->d_vars[d_q].end(),\r
                                         terms.begin(), terms.end() );\r
       cons = it->second ? cons : cons.negate();\r
       if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
@@ -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 ){\r
         d_matched_basis = true;\r
         Node f = getOperator( d_n );\r
-        TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );\r
+        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );\r
         if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){\r
           success = true;\r
           d_qni_bound[0] = d_qni_var_num[0];\r
@@ -1662,7 +1662,7 @@ bool MatchGen::isHandledUfTerm( TNode n ) {
 \r
 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r
   if( isHandledUfTerm( n ) ){\r
-    return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );\r
+    return p->getTermDatabase()->getOperator( n );\r
   }else{\r
     return Node::null();\r
   }\r
@@ -2087,26 +2087,28 @@ void QuantConflictFind::computeRelevantEqr() {
     while( !eqcs_i.isFinished() ){\r
       //nEqc++;\r
       Node r = (*eqcs_i);\r
-      TypeNode rtn = r.getType();\r
-      if( options::qcfMode()==QCF_MC ){\r
-        std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );\r
-        if( itt==d_eqcs.end() ){\r
-          Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );\r
-          if( !getEqualityEngine()->hasTerm( mb ) ){\r
-            Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;\r
-            Assert( false );\r
-          }\r
-          Node mbr = getRepresentative( mb );\r
-          if( mbr!=r ){\r
-            d_eqcs[rtn].push_back( mbr );\r
+      if( getTermDatabase()->hasTermCurrent( r ) ){\r
+        TypeNode rtn = r.getType();\r
+        if( options::qcfMode()==QCF_MC ){\r
+          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );\r
+          if( itt==d_eqcs.end() ){\r
+            Node mb = getTermDatabase()->getModelBasisTerm( rtn );\r
+            if( !getEqualityEngine()->hasTerm( mb ) ){\r
+              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;\r
+              Assert( false );\r
+            }\r
+            Node mbr = getRepresentative( mb );\r
+            if( mbr!=r ){\r
+              d_eqcs[rtn].push_back( mbr );\r
+            }\r
+            d_eqcs[rtn].push_back( r );\r
+            d_model_basis[rtn] = mb;\r
+          }else{\r
+            itt->second.push_back( r );\r
           }\r
-          d_eqcs[rtn].push_back( r );\r
-          d_model_basis[rtn] = mb;\r
         }else{\r
-          itt->second.push_back( r );\r
+          d_eqcs[rtn].push_back( r );\r
         }\r
-      }else{\r
-        d_eqcs[rtn].push_back( r );\r
       }\r
       ++eqcs_i;\r
     }\r

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ee39b55d9f0b61692ede479ebb547b1321dfa0dc..b21494f77532228d06043475919d10bd7d6df0ba 100644 (file)
--- 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 3d419ed5cce5bb74c0c8e9bbdef8bd0c2287422b..4dca6b36c3e520f111edb7829fc16ab58df23f30 100644 (file)
--- 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(){}