diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/quantifiers_engine.cpp | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 156 |
1 files changed, 110 insertions, 46 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 902eebe01..ebd6d32ea 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -78,6 +78,10 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_eq_query; } +EqualityQuery* QuantifiersEngine::getEqualityQuery() { + return d_eq_query; +} + Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ return d_te->theoryOf( id )->getInstantiator(); } @@ -96,32 +100,39 @@ Valuation& QuantifiersEngine::getValuation(){ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); - if( e>=Theory::EFFORT_FULL ){ - Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call + for( int i=0; i<(int)d_modules.size(); i++ ){ + if( d_modules[i]->needsCheck( e ) ){ + needsCheck = true; + } } - - d_hasAddedLemma = false; - if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first - if( options::finiteModelFind() ){ - //first, check if we can minimize the model further - if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; + if( needsCheck ){ + Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + //reset relevant information + d_hasAddedLemma = false; + d_term_db->reset( e ); + d_eq_query->reset(); + if( e==Theory::EFFORT_LAST_CALL ){ + //if effort is last call, try to minimize model first + if( options::finiteModelFind() ){ + //first, check if we can minimize the model further + if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ + return; + } } + ++(d_statistics.d_instantiation_rounds_lc); + }else if( e==Theory::EFFORT_FULL ){ + ++(d_statistics.d_instantiation_rounds); } - ++(d_statistics.d_instantiation_rounds_lc); - }else if( e==Theory::EFFORT_FULL ){ - ++(d_statistics.d_instantiation_rounds); - } - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->check( e ); - } - //build the model if not done so already - // this happens if no quantifiers are currently asserted and no model-building module is enabled - if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ - d_te->getModelBuilder()->buildModel( d_model, true ); - } - if( e>=Theory::EFFORT_FULL ){ + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->check( e ); + } + //build the model if not done so already + // this happens if no quantifiers are currently asserted and no model-building module is enabled + if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ + d_te->getModelBuilder()->buildModel( d_model, true ); + } + Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; } } @@ -183,15 +194,6 @@ Node QuantifiersEngine::getNextDecisionRequest(){ return Node::null(); } -void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( getInstantiator( i ) ){ - getInstantiator( i )->resetInstantiationRound( level ); - } - } - getTermDatabase()->reset( level ); -} - void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); @@ -326,13 +328,24 @@ bool QuantifiersEngine::addLemma( Node lem ){ } bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ + Trace("inst-add") << "Add instantiation: " << m << std::endl; //make sure there are values for each variable we are instantiating - m.makeComplete( f, this ); - //make it representative, this is helpful for recognizing duplication - if( mkRep ){ - m.makeRepresentative( this ); + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Node ic = d_term_db->getInstantiationConstant( f, i ); + Node val = m.getValue( ic ); + if( val.isNull() ){ + val = d_term_db->getFreeVariableForInstConstant( ic ); + Trace("inst-add-debug") << "mkComplete " << val << std::endl; + m.set( ic, val ); + } + //make it representative, this is helpful for recognizing duplication + if( mkRep ){ + //pick the best possible representative for instantiation, based on past use and simplicity of term + Node r = d_eq_query->getInternalRepresentative( val ); + Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl; + m.set( ic, r ); + } } - Trace("inst-add") << "Add instantiation: " << m << std::endl; //check for duplication modulo equality if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){ Trace("inst-add") << " -> Already exists." << std::endl; @@ -552,6 +565,10 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss); } +void EqualityQueryQuantifiersEngine::reset(){ + d_int_rep.clear(); + d_reset_count++; +} bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); @@ -624,15 +641,40 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ - //for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - // if( d_qe->getInstantiator( i ) ){ - // if( d_qe->getInstantiator( i )->hasTerm( a ) ){ - // return d_qe->getInstantiator( i )->getInternalRepresentative( a ); - // } - // } - //} - //return a; - return d_qe->getInstantiator( THEORY_UF )->getInternalRepresentative( a ); + if( !options::internalReps() ){ + return d_qe->getInstantiator( THEORY_UF )->getRepresentative( a ); + }else{ + Node r = d_qe->getInstantiator( THEORY_UF )->getRepresentative( a ); + if( d_int_rep.find( r )==d_int_rep.end() ){ + std::vector< Node > eqc; + getEquivalenceClass( r, eqc ); + //find best selection for representative + Node r_best = r; + int r_best_score = getRepScore( r ); + for( size_t i=0; i<eqc.size(); i++ ){ + int score = getRepScore( eqc[i] ); + //score prefers earliest use of this term as a representative + if( score>=0 && ( r_best_score<0 || score<r_best_score ) ){ + r_best = eqc[i]; + r_best_score = score; + } + } + //now, make sure that no other member of the class is an instance + r_best = getInstance( r_best, eqc ); + //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; + } + d_int_rep[r] = r_best; + if( r_best!=a ){ + Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; + Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; + } + return r_best; + }else{ + return d_int_rep[r]; + } + } } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ @@ -657,4 +699,26 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N if( eqc.empty() ){ eqc.push_back( a ); } + //a should be in its equivalence class + Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); +} + +//helper functions + +Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + Node nn = getInstance( n[i], eqc ); + if( !nn.isNull() ){ + return nn; + } + } + if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){ + return n; + }else{ + return Node::null(); + } +} + +int EqualityQueryQuantifiersEngine::getRepScore( Node n ){ + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; } |