diff options
Diffstat (limited to 'src/theory/inst_match.cpp')
-rw-r--r-- | src/theory/inst_match.cpp | 71 |
1 files changed, 21 insertions, 50 deletions
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index 4f1bfe67e..c90483fa3 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -17,8 +17,8 @@ #include "theory/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" +#include "theory/candidate_generator.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" @@ -33,38 +33,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; -bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ) || - ( Options::current()->finiteModelFind && n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ); -} - -void CandidateGeneratorQueue::addCandidate( Node n ) { - if( isLegalCandidate( n ) ){ - d_candidates.push_back( n ); - } -} - -void CandidateGeneratorQueue::reset( Node eqc ){ - if( d_candidate_index>0 ){ - d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); - d_candidate_index = 0; - } - if( !eqc.isNull() ){ - d_candidates.push_back( eqc ); - } -} -Node CandidateGeneratorQueue::getNextCandidate(){ - if( d_candidate_index<(int)d_candidates.size() ){ - Node n = d_candidates[d_candidate_index]; - d_candidate_index++; - return n; - }else{ - d_candidate_index = 0; - d_candidates.clear(); - return Node::null(); - } -} - InstMatch::InstMatch() { } @@ -130,18 +98,21 @@ void InstMatch::debugPrint( const char* c ){ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){ - if( d_map.find( qe->getTermDatabase()->d_inst_constants[f][i] )==d_map.end() ){ - d_map[ qe->getTermDatabase()->d_inst_constants[f][i] ] = qe->getTermDatabase()->getFreeVariableForInstConstant( qe->getTermDatabase()->d_inst_constants[f][i] ); + Node ic = qe->getTermDatabase()->d_inst_constants[f][i]; + if( d_map.find( ic )==d_map.end() ){ + d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); } } } void InstMatch::makeInternal( QuantifiersEngine* qe ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + if( Options::current()->cbqi ){ + for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ + if( it->second.hasAttribute(InstConstantAttribute()) ){ + d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); + if( it->second.hasAttribute(InstConstantAttribute()) ){ + d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + } } } } @@ -203,9 +174,9 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m } if( modEq ){ //check modulo equality if any other instantiation match exists - if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->getRepresentative( n ), - ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en!=n ){ @@ -310,10 +281,10 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ //candidates will be all equalities - d_cg = new uf::inst::CandidateGeneratorTheoryUfLitEq( ith, d_match_pattern ); + d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); }else{ //candidates will be all disequalities - d_cg = new uf::inst::CandidateGeneratorTheoryUfLitDeq( ith, d_match_pattern ); + d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); @@ -322,7 +293,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ }else{ Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class - d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } @@ -331,7 +302,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; //} //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ @@ -785,9 +756,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I } if( modEq ){ //check modulo equality for other possible instantiations - if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( qe->getEqualityQuery()->getRepresentative( n ), - ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en!=n ){ |