diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 12:43:37 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 12:43:37 +0200 |
commit | 7443276e61db276e5ba48d605cb6b08a35c5a100 (patch) | |
tree | 6229f2d75a6f58c09fa185771b696af728d58e42 /src/theory | |
parent | a5726277ce0388f07edcdaef573c0de2e88f37e7 (diff) |
Fix performance issue with variable triggers + instantiation restrictions.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 9 |
3 files changed, 20 insertions, 4 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 7d2544b6f..48041e894 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -202,12 +202,18 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); if( !nh.isNull() ){ - if( options::instMaxLevel()!=-1 ){ + if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); + //don't consider this if already the instantiation is ineligible + if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ + nh = Node::null(); + } + } + if( !nh.isNull() ){ + d_firstTime = false; + //an equivalence class with the same type as the pattern, return it + return nh; } - d_firstTime = false; - //an equivalence class with the same type as the pattern, return it - return nh; } } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index ea3e18be1..3b31bad13 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -140,6 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e; int e_use = e; if( e_use>=0 ){ + Trace("inst-engine-debug") << "inst-engine : " << f << std::endl; //check each instantiation strategy for( size_t i=0; i<d_instStrategies.size(); ++i ){ InstStrategy* is = d_instStrategies[i]; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ba75af873..8dec3898c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -991,8 +991,14 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { eq::EqualityEngine* ee = getMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); + TypeNode tr = r.getType(); + if( typ_num.find( tr )==typ_num.end() ){ + typ_num[tr] = 0; + } + typ_num[tr]++; bool firstTime = true; Trace(c) << " " << r; Trace(c) << " : { "; @@ -1013,6 +1019,9 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { ++eqcs_i; } Trace(c) << std::endl; + for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){ + Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl; + } } void EqualityQueryQuantifiersEngine::reset(){ |