diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-07 19:17:11 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-07 19:17:11 -0400 |
commit | 4145ab467a6aaf25c61d0b614000d9d2d4b0321b (patch) | |
tree | 9397566172f1d6f09c9e7ef816f756efaed6c53b | |
parent | f3a1c9f4a2d233cd0a3904749d0a5499f7f2c9d9 (diff) | |
parent | fc788d5125fed8257544e74ab8898344b1e7b19d (diff) |
Merge remote-tracking branch 'upstream/master' into sets-mergable
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
3 files changed, 15 insertions, 11 deletions
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 35809b536..c78ea7b01 100644 --- 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 d81db8b8d..7ed5b2164 100644 --- 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 e914280c5..e84c4742e 100644 --- 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: |