Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep for...

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 35809b536c8793d5fd17b5776e1ce3ac1d00f5b6..c78ea7b013ae4400799ebebef6d2219cb2a183aa 100644 (file)
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -337,7 +337,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
   while( getNextMatch( f, m, qe ) ){
     if( !d_active_add ){
       m.add( baseMatch );
-      if( qe->addInstantiation( f, m ) ){
+      if( qe->addInstantiation( f, m, false ) ){
         addedLemmas++;
       }
     }else{
@@ -354,7 +354,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
   if( !d_match_pattern.isNull() ){
     InstMatch m( f );
     if( getMatch( f, t, m, qe ) ){
-      if( qe->addInstantiation( f, m ) ){
+      if( qe->addInstantiation( f, m, false ) ){
         return 1;
       }
     }
@@ -647,7 +647,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
     }
   }else{
     //m is an instantiation
-    if( qe->addInstantiation( d_f, m ) ){
+    if( qe->addInstantiation( d_f, m, false ) ){
       addedLemmas++;
       Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
     }
@@ -739,7 +739,7 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
       return 0;
     }
   }
-  return qe->addInstantiation( f, m ) ? 1 : 0;
+  return qe->addInstantiation( f, m, false ) ? 1 : 0;
 }
 
 }/* CVC4::theory::inst namespace */

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d81db8b8dfab3f7a668264adebc8adbcf64a63ce..7ed5b2164588a6d866ed9dfd89e77b14f48cc062 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -911,7 +911,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         }
       }
       //now, make sure that no other member of the class is an instance
-      r_best = getInstance( r_best, eqc );
+      std::hash_map<TNode, Node, TNodeHashFunction> cache;
+      r_best = getInstance( r_best, eqc, cache );
       //store that this representative was chosen at this point
       if( d_rep_score.find( r_best )==d_rep_score.end() ){
         d_rep_score[ r_best ] = d_reset_count;
@@ -1018,17 +1019,20 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N
 
 //helper functions
 
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
+  if(cache.find(n) != cache.end()) {
+    return cache[n];
+  }
   for( size_t i=0; i<n.getNumChildren(); i++ ){
-    Node nn = getInstance( n[i], eqc );
+    Node nn = getInstance( n[i], eqc, cache );
     if( !nn.isNull() ){
-      return nn;
+      return cache[n] = nn;
     }
   }
   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
-    return n;
+    return cache[n] = n;
   }else{
-    return Node::null();
+    return cache[n] = Node::null();
   }
 }
 

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e914280c52eb9d1d9e2010ba521a96284e2978dc..e84c4742ee4406db7bf90d33866500d7ee2138a8 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -297,7 +297,7 @@ private:
   bool d_liberal;
 private:
   /** node contains */
-  Node getInstance( Node n, std::vector< Node >& eqc );
+  Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index );
 public: