summaryrefslogtreecommitdiff
path: root/src/theory/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/inst_match.cpp')
-rw-r--r--src/theory/inst_match.cpp71
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 ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback