diff options
Diffstat (limited to 'src/theory/quantifiers')
26 files changed, 438 insertions, 399 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 3d98674a8..8272ce168 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -42,10 +42,6 @@ void FirstOrderModel::reset(){ TheoryModel::reset(); } -void FirstOrderModel::addTerm( Node n ){ - TheoryModel::addTerm( n ); -} - void FirstOrderModel::initialize( bool considerAxioms ){ //rebuild models d_uf_model_tree.clear(); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 3779579fd..50a941968 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -33,8 +33,6 @@ class TermDb; class FirstOrderModel : public TheoryModel { private: - //add term function - void addTerm( Node n ); //for initialize model void initializeModelForTerm( Node n ); /** whether an axiom is asserted */ diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index b5f92c5f8..dea371e9c 100755..100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -1,13 +1,11 @@ /********************* */ /*! \file inst_gen.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index c8de2c642..930133954 100755..100644 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -1,13 +1,11 @@ /********************* */ /*! \file inst_gen.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -52,10 +50,10 @@ public: int getNumMatches() { return d_matches.size(); } bool getMatch( EqualityQuery* q, int i, InstMatch& m ); Node getMatchValue( int i ) { return d_match_values[i]; } -}; +};/* class InstGenProcess */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index dcd7a1b79..85a96f90a 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -103,12 +103,12 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } } -void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ - EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); - } -} +//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ +// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); +// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ +// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); +// } +//} void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8b2d9726b..b9e61be20 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -58,7 +58,7 @@ public: /** make complete */ void makeComplete( Node f, QuantifiersEngine* qe ); /** make internal representative */ - void makeInternalRepresentative( QuantifiersEngine* qe ); + //void makeInternalRepresentative( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** get value */ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2822597e1..386834385 100755..100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -1,15 +1,16 @@ /********************* */ /*! \file inst_match_generator.cpp -** \verbatim -** Original author: ajreynol -** Major contributors: bobot -** Minor contributors (to current version): barrett, mdeters -** This file is part of the CVC4 prototype. -** Copyright (c) 2009-2012 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief Implementation of inst match generator class + ** \verbatim + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "theory/quantifiers/inst_match_generator.h" @@ -29,116 +30,111 @@ namespace theory { namespace inst { -InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ - initializePattern( pat, qe ); -} - -InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ - if( pats.size()==1 ){ - initializePattern( pats[0], qe ); - }else{ - initializePatterns( pats, qe ); - } +InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){ + d_active_add = false; + Assert( pat.hasAttribute(InstConstantAttribute()) ); + d_pattern = pat; + d_match_pattern = pat; + d_next = NULL; } -void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){ - int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy; - for( int i=0; i<(int)pats.size(); i++ ){ - d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) ); +void InstMatchGenerator::setActiveAdd(){ + d_active_add = true; + if( d_next!=NULL ){ + d_next->setActiveAdd(); } - d_pattern = Node::null(); - d_match_pattern = Node::null(); - d_cg = NULL; } -void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ - Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; - Assert( pat.hasAttribute(InstConstantAttribute()) ); - d_pattern = pat; - d_match_pattern = pat; - if( d_match_pattern.getKind()==NOT ){ - //we want to add the children of the NOT - d_match_pattern = d_pattern[0]; - } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); - //swap sides - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[1]; - }else{ - d_match_pattern = d_pattern[0][0]; - } - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[0]; +void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){ + if( !d_pattern.isNull() ){ + Debug("inst-match-gen") << "Pattern term is " << d_pattern << std::endl; + if( d_match_pattern.getKind()==NOT ){ + //we want to add the children of the NOT + d_match_pattern = d_pattern[0]; + } + if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ + if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ + Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); + //swap sides + Node pat = d_pattern; + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); + d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; + if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[1]; + }else{ + d_match_pattern = d_pattern[0][0]; + } + }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ + Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); + if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[0]; + } } } - } - int childMatchPolicy = MATCH_GEN_DEFAULT; - for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ - if( d_match_pattern[i].getKind()!=INST_CONSTANT ){ - d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) ); - d_children_index.push_back( i ); + int childMatchPolicy = MATCH_GEN_DEFAULT; + for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ + if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( d_match_pattern[i].getKind()!=INST_CONSTANT ){ + InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy ); + d_children.push_back( cimg ); + d_children_index.push_back( i ); + gens.push_back( cimg ); + } } } - } - Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; + Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - //create candidate generator - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ - Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); - //we will be producing candidates via literal matching heuristics - if( d_pattern.getKind()!=NOT ){ - //candidates will be all equalities - d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); - }else{ - //candidates will be all disequalities - 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 ); - if( d_pattern.getKind()==NOT ){ - Unimplemented("Disequal generator unimplemented"); - }else{ - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class + //create candidate generator + if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); + //we will be producing candidates via literal matching heuristics + if( d_pattern.getKind()!=NOT ){ + //candidates will be all equalities + d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); + }else{ + //candidates will be all disequalities + 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 ); + if( d_pattern.getKind()==NOT ){ + Unimplemented("Disequal generator unimplemented"); + }else{ + Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); + //we are matching only in a particular equivalence class + 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]; + } + }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ + //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ + //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 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]; - } - }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ - //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 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 ) ){ - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + d_cg = new CandidateGeneratorQueue; + if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ + Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; + }else{ + Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + } + //we will treat this as match gen internal arithmetic + d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; } - //we will treat this as match gen internal arithmetic - d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; } } } /** get match (not modulo equality) */ -bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){ +bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m.size() << ")" << ", " << d_children.size() << std::endl; + << m << ")" << ", " << d_children.size() << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; @@ -148,9 +144,8 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) return false; }else{ EqualityQuery* q = qe->getEqualityQuery(); - //add m to partial match vector - std::vector< InstMatch > partial; - partial.push_back( InstMatch( &m ) ); + //save previous match + InstMatch prev( &m ); //if t is null Assert( !t.isNull() ); Assert( !t.hasAttribute(InstConstantAttribute()) ); @@ -160,13 +155,13 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){ + if( !m.setMatch( q, d_match_pattern[i], t[i] ) ){ //match is in conflict Debug("matching-debug") << "Match in conflict " << t[i] << " and " << d_match_pattern[i] << " because " - << partial[0].get(d_match_pattern[i]) + << m.get(d_match_pattern[i]) << std::endl; - Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl; + Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl; return false; } } @@ -184,48 +179,25 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) for( int i=0; i<(int)d_children.size(); i++ ){ Node rep = q->getRepresentative( t[ d_children_index[i] ] ); reps.push_back( rep ); - d_children[i]->d_cg->reset( rep ); + d_children[i]->reset( rep, qe ); } - - //combine child matches - int index = 0; - while( index>=0 && index<(int)d_children.size() ){ - partial.push_back( InstMatch( &partial[index] ) ); - if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){ - index++; - }else{ - d_children[index]->d_cg->reset( reps[index] ); - partial.pop_back(); - if( !partial.empty() ){ - partial.pop_back(); - } - index--; + bool success = true; + if( d_next!=NULL ){ + success = d_next->getNextMatch( f, m, qe ); + }else{ + if( d_active_add ){ + Trace("active-add") << "Active Adding instantiation " << m << std::endl; + success = qe->addInstantiation( f, m ); + Trace("active-add") << "Success = " << success << std::endl; } } - if( index>=0 ){ - m = partial.back(); - return true; - }else{ - return false; + if( !success ){ + m = InstMatch( &prev ); } + return success; } } -bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){ - bool success = false; - Node t; - do{ - //get the next candidate term t - t = d_cg->getNextCandidate(); - //if t not null, try to fit it into match m - if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ - success = getMatch( t, m, qe ); - } - }while( !success && !t.isNull() ); - if (saveMatched) m.d_matched = t; - return success; -} - bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl; if( !d_arith_coeffs.empty() ){ @@ -298,74 +270,57 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ } void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ - if( d_match_pattern.isNull() ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->reset( eqc, qe ); - } - d_partial.clear(); - }else{ - if( !d_eq_class.isNull() ){ - //we have a specific equivalence class in mind - //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term - //just look in equivalence class of the RHS - d_cg->reset( d_eq_class ); - }else{ - d_cg->reset( eqc ); - } + if( !eqc.isNull() ){ + d_eq_class = eqc; } + //we have a specific equivalence class in mind + //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term + //just look in equivalence class of the RHS + d_cg->reset( d_eq_class ); } -bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ +bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ m.d_matched = Node::null(); - if( d_match_pattern.isNull() ){ - int index = (int)d_partial.size(); - while( index>=0 && index<(int)d_children.size() ){ - if( index>0 ){ - d_partial.push_back( InstMatch( &d_partial[index-1] ) ); - }else{ - d_partial.push_back( InstMatch() ); - } - if( d_children[index]->getNextMatch( d_partial[index], qe ) ){ - index++; - }else{ - d_children[index]->reset( Node::null(), qe ); - d_partial.pop_back(); - if( !d_partial.empty() ){ - d_partial.pop_back(); - } - index--; - } - } - if( index>=0 ){ - m = d_partial.back(); - d_partial.pop_back(); - return true; - }else{ - return false; + //Debug("matching") << this << " " << d_pattern << " get next match 2 " << m << " in eq class " << d_eq_class << std::endl; + bool success = false; + Node t; + do{ + //get the next candidate term t + t = d_cg->getNextCandidate(); + //if t not null, try to fit it into match m + if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ + success = getMatch( f, t, m, qe ); } - }else{ - bool res = getNextMatch2( m, qe, true ); - Assert(!res || !m.d_matched.isNull()); - return res; + }while( !success && !t.isNull() ); + m.d_matched = t; + if( !success ){ + //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl; + //we failed, must reset + reset( d_eq_class, qe ); } + return success; } int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - //now, try to add instantiation for each match produced + //try to add instantiation for each match produced int addedLemmas = 0; InstMatch m; - while( getNextMatch( m, qe ) ){ - //m.makeInternal( d_quantEngine->getEqualityQuery() ); - m.add( baseMatch ); - if( qe->addInstantiation( f, m ) ){ - addedLemmas++; - if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ - return addedLemmas; + while( getNextMatch( f, m, qe ) ){ + if( !d_active_add ){ + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + m.add( baseMatch ); + if( qe->addInstantiation( f, m ) ){ + addedLemmas++; + if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ + return addedLemmas; + } } + m.clear(); + }else{ + addedLemmas++; } - m.clear(); } //return number of lemmas added return addedLemmas; @@ -375,7 +330,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); if( !d_match_pattern.isNull() ){ InstMatch m; - if( getMatch( t, m, qe ) ){ + if( getMatch( f, t, m, qe ) ){ if( qe->addInstantiation( f, m ) ){ return 1; } @@ -388,6 +343,40 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ return 0; } + +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ) { + std::vector< Node > pats; + pats.push_back( pat ); + return mkInstMatchGenerator( pats, qe ); +} + +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ) { + size_t pCounter = 0; + InstMatchGenerator* prev = NULL; + InstMatchGenerator* oinit = NULL; + while( pCounter<pats.size() ){ + size_t counter = 0; + std::vector< InstMatchGenerator* > gens; + InstMatchGenerator* init = new InstMatchGenerator(pats[pCounter]); + if(pCounter==0){ + oinit = init; + } + gens.push_back(init); + //chain the resulting match generators together + while (counter<gens.size()) { + InstMatchGenerator* curr = gens[counter]; + if( prev ){ + prev->d_next = curr; + } + curr->initialize(qe, gens); + prev = curr; + counter++; + } + pCounter++; + } + return oinit; +} + /** constructors */ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) : d_f( f ){ @@ -408,7 +397,7 @@ d_f( f ){ for( int i=0; i<(int)pats.size(); i++ ){ Node n = pats[i]; //make the match generator - d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) ); + d_children.push_back( InstMatchGenerator::mkInstMatchGenerator( n, qe ) ); //compute unique/shared variables std::vector< int > unique_vars; std::map< int, bool > shared_vars; @@ -473,7 +462,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; std::vector< InstMatch > newMatches; InstMatch m; - while( d_children[i]->getNextMatch( m, qe ) ){ + while( d_children[i]->getNextMatch( f, m, qe ) ){ m.makeRepresentative( qe ); newMatches.push_back( InstMatch( &m ) ); m.clear(); @@ -595,7 +584,7 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ InstMatch m; //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){ + if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){ processNewMatch( qe, m, i, addedLemmas ); } } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index dd3663e0a..b201fa60f 100755..100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_match_generator.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -38,11 +38,13 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; /** get the next match. must call reset( eqc ) before this function. */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0; /** add instantiations directly */ virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; /** add ground term t, called when t is added to term db */ virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; + /** set active add */ + virtual void setActiveAdd() {} };/* class IMGenerator */ class CandidateGenerator; @@ -56,15 +58,14 @@ private: /** children generators */ std::vector< InstMatchGenerator* > d_children; std::vector< int > d_children_index; - /** partial vector */ - std::vector< InstMatch > d_partial; + /** the next generator in order */ + InstMatchGenerator* d_next; /** eq class */ Node d_eq_class; /** for arithmetic matching */ std::map< Node, Node > d_arith_coeffs; /** initialize pattern */ - void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ); - void initializePattern( Node pat, QuantifiersEngine* qe ); + void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ); public: enum { //options for producing matches @@ -75,10 +76,6 @@ public: MATCH_GEN_INTERNAL_ERROR, }; private: - /** get the next match. must call d_cg->reset( ... ) before using. - only valid for use where !d_match_pattern.isNull(). - */ - bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); /** for arithmetic */ bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: @@ -86,11 +83,10 @@ public: d_match_pattern and t should have the same shape. only valid for use where !d_match_pattern.isNull(). */ - bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); + bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ); /** constructors */ - InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); - InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + InstMatchGenerator( Node pat, int matchOption = 0 ); /** destructor */ ~InstMatchGenerator(){} /** The pattern we are producing matches for. @@ -105,11 +101,17 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ int addTerm( Node f, Node t, QuantifiersEngine* qe ); + + bool d_active_add; + void setActiveAdd(); + + static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ); + static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ); };/* class InstMatchGenerator */ /** smart multi-trigger implementation */ @@ -152,7 +154,7 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ @@ -178,7 +180,7 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ) {} /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t, possibly add instantiations */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index aba311500..b12fed619 100755..100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_strategy_cbqi.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -46,11 +46,12 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort d_tableaux.clear(); d_ceTableaux.clear(); //search for instantiation rows in simplex tableaux - ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); - for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ - ArithVar x = (*it).first; + ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; if( d_th->d_partialModel.hasEitherBound( x ) ){ - Node n = (*it).second; + Node n = avnm.asNode(x); Node f; NodeBuilder<> t(kind::PLUS); if( n.getKind()==PLUS ){ @@ -167,10 +168,11 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder } void InstStrategySimplex::debugPrint( const char* c ){ - ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); - for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ - ArithVar x = (*it).first; - Node n = (*it).second; + const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; + Node n = avnm.asNode(x); //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ Debug(c) << x << " : " << n << ", bounds = "; if( d_th->d_partialModel.hasLowerBound( x ) ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 1c9565de6..de548ab14 100755..100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_strategy_cbqi.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index edf9d976c..3f5cc7666 100755..100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_strategy_e_matching.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -27,7 +27,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers; -#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER //#define MULTI_TRIGGER_FULL_EFFORT_HALF #define MULTI_MULTI_TRIGGERS @@ -65,18 +64,13 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ //Notice() << "Try user-provided patterns..." << std::endl; for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ bool processTrigger = true; - if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){ -//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF -// processTrigger = d_counter[f]%2==0; -//#endif - } if( processTrigger ){ //if( d_user_gen[f][i]->isMultiTrigger() ) - //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; + Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl; InstMatch baseMatch; int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); //if( d_user_gen[f][i]->isMultiTrigger() ) - //Notice() << " Done, numInst = " << numInst << "." << std::endl; + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; @@ -125,6 +119,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort itt->first->reset( Node::null() ); } } + d_processed_trigger.clear(); } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ @@ -134,6 +129,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( e<peffort ){ return STATUS_UNFINISHED; }else{ + int status = STATUS_UNKNOWN; bool gen = false; if( e==peffort ){ if( d_counter.find( f )==d_counter.end() ){ @@ -147,7 +143,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) gen = true; } if( gen ){ - generateTriggers( f ); + generateTriggers( f, effort, e, status ); } Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; //Notice() << "Try auto-generated triggers..." << std::endl; @@ -155,18 +151,14 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) Trigger* tr = itt->first; if( tr ){ bool processTrigger = itt->second; - if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){ -#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF - processTrigger = d_counter[f]%2==0; -#endif - } - if( processTrigger ){ + if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){ + d_processed_trigger[f][tr] = true; //if( tr->isMultiTrigger() ) - Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; + Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl; InstMatch baseMatch; int numInst = tr->addInstantiations( baseMatch ); //if( tr->isMultiTrigger() ) - Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; }else{ @@ -181,24 +173,24 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } Debug("quant-uf-strategy") << "done." << std::endl; //Notice() << "done" << std::endl; + return status; } - return STATUS_UNKNOWN; } -void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ - Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; +void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effort, int e, int & status ){ + Trace("auto-gen-trigger-debug") << "Generate trigger for " << f << std::endl; if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true ); - Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ - Debug("auto-gen-trigger") << patTermsF[i] << " "; + Trace("auto-gen-trigger") << patTermsF[i] << " "; } - Debug("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << std::endl; //extend to literal matching (if applicable) d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers @@ -214,23 +206,22 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } d_made_multi_trigger[f] = false; - Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ - Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " "; + Trace("auto-gen-trigger") << d_patTerms[0][f][i] << " "; } - Debug("auto-gen-trigger") << std::endl; - Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){ - Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " "; + Trace("auto-gen-trigger") << d_patTerms[1][f][i] << " "; } - Debug("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << std::endl; } //populate candidate pattern term vector for the current trigger std::vector< Node > patTerms; -#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER //try to add single triggers first for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){ @@ -241,13 +232,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( patTerms.empty() ){ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); } -#else - patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() ); - patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); -#endif if( !patTerms.empty() ){ - Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl; //sort terms based on relevance if( d_rlv_strategy==RELEVANCE_DEFAULT ){ sortQuantifiersForSymbol sqfs; @@ -273,6 +260,15 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ options::smartTriggers() ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ + //only generate multi trigger if effort level > 5, or if no single triggers exist + if( !d_patTerms[0][f].empty() ){ + if( e<=5 ){ + status = STATUS_UNFINISHED; + return; + }else{ + Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl; + } + } //if we are re-generating triggers, shuffle based on some method if( d_made_multi_trigger[f] ){ #ifndef MULTI_MULTI_TRIGGERS diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index b5ff90a62..13d443c6a 100755..100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_strategy_e_matching.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -80,12 +80,14 @@ private: std::map< Node, bool > d_is_single_trigger; std::map< Node, bool > d_single_trigger_gen; std::map< Node, bool > d_made_multi_trigger; + //processed trigger this round + std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger; private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); /** generate triggers */ - void generateTriggers( Node f ); + void generateTriggers( Node f, Theory::Effort effort, int e, int & status ); public: /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 53977ee4f..75cc10615 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -84,16 +84,18 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //add cbqi lemma //get the counterexample literal Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - //require any decision on cel to be phase=true - d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); - addedLemma = true; + if( !ceLit.isNull() ){ + //require any decision on cel to be phase=true + d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + NodeBuilder<> nb(kind::OR); + nb << f << ceLit; + Node lem = nb; + Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma( lem ); + addedLemma = true; + } } } if( addedLemma ){ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 5c7c9415e..bf67bdd25 100755..100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file macros.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -358,7 +358,7 @@ Node QuantifierMacros::simplify( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){ - //do subsitutition + //do substitution Node ret = d_macro_defs[op]; ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() ); return ret; diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index f4e58665d..140f02966 100755..100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -1,11 +1,11 @@ /********************* */ /*! \file macros.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 2f44140c2..d1c04ceab 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -526,7 +526,7 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ //if applicable, try to add exceptions here if( !tr_terms.empty() ){ //make a trigger for these terms, add instantiations - inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms ); + inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW, options::smartTriggers() ); //Notice() << "Trigger = " << (*tr) << std::endl; tr->resetInstantiationRound(); tr->reset( Node::null() ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index bf6ea11f0..39377d11c 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -73,9 +73,8 @@ void ModelEngine::check( Theory::Effort e ){ if( addedLemmas==0 ){ Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; //let the strong solver verify that the model is minimal - uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); //for debugging, this will if there are terms in the model that the strong solver was not notified of - uf_ss->debugModel( fm ); + ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ); Trace("model-engine-debug") << "Check model..." << std::endl; d_incomplete_check = false; //print debug @@ -164,7 +163,7 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine-debug") << " "; for( size_t i=0; i<it->second.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; - Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] ); + Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index bc45e6051..6b204eb60 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -45,8 +45,8 @@ option macrosQuant --macros-quant bool :default false option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers -option relevantTriggers /--relevant-triggers bool :default true - prefer triggers that are more relevant based on SInE style method +option relevantTriggers --relevant-triggers bool :default true + prefer triggers that are more relevant based on SInE style analysis # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false @@ -71,7 +71,7 @@ option userPatternsQuant /--ignore-user-patterns bool :default true option flipDecision --flip-decision/ bool :default false turns on flip decision heuristic -option internalReps --disable-quant-internal-reps/ bool :default true +option internalReps /--disable-quant-internal-reps bool :default true disables instantiating with representatives chosen by quantifiers engine option finiteModelFind --finite-model-find bool :default false diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index a78cd5612..9e4a2a14a 100755..100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file quant_util.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot, mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 1daaf3ea1..85602dbab 100755..100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -1,11 +1,11 @@ /********************* */ /*! \file quant_util.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters, bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 108c09c87..b00fe45f4 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_attributes.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index f5a8a749a..8e8ebe97a 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_attributes.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d60aa2ef4..65624686a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -206,6 +206,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ ModelBasisAttribute mba; mbt.setAttribute(mba,true); d_model_basis_term[tn] = mbt; + Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl; } return d_model_basis_term[tn]; } @@ -337,6 +338,14 @@ Node TermDb::getInstConstantBody( Node f ){ Node TermDb::getCounterexampleLiteral( Node f ){ if( d_ce_lit.find( f )==d_ce_lit.end() ){ Node ceBody = getInstConstantBody( f ); + //check if any variable are of bad types, and fail if so + for( size_t i=0; i<d_inst_constants[f].size(); i++ ){ + if( d_inst_constants[f][i].getType().isBoolean() ){ + d_ce_lit[ f ] = Node::null(); + return Node::null(); + } + } + //otherwise, ensure literal Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); d_ce_lit[ f ] = ceLit; setInstantiationConstantAttr( ceLit, f ); @@ -367,6 +376,10 @@ Node TermDb::getSkolemizedBody( Node f ){ Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" ); d_skolem_constants[ f ].push_back( skv ); vars.push_back( f[0][i] ); + //carry information for sort inference + if( options::sortInference() ){ + d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv ); + } } d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(), d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() ); @@ -515,6 +528,34 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){ return 0; } +bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ + if( n1==n2 ){ + return true; + }else if( n2.getKind()==INST_CONSTANT ){ + //if( !node_contains( n1, n2 ) ){ + // return false; + //} + if( subs.find( n2 )==subs.end() ){ + subs[n2] = n1; + }else if( subs[n2]!=n1 ){ + return false; + } + return true; + }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){ + if( n1.getOperator()!=n2.getOperator() ){ + return false; + } + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){ + return false; + } + } + return true; + }else{ + return false; + } +} + void TermDb::filterInstances( std::vector< Node >& nodes ){ std::vector< bool > active; active.resize( nodes.size(), true ); @@ -523,8 +564,10 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){ if( active[i] && active[j] ){ int result = isInstanceOf( nodes[i], nodes[j] ); if( result==1 ){ + Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl; active[j] = false; }else if( result==-1 ){ + Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl; active[i] = false; } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index a1f1de1dc..6bfea5c44 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -167,7 +167,7 @@ public: /** get counterexample literal (for cbqi) */ Node getCounterexampleLiteral( Node f ); /** returns node n with bound vars of f replaced by instantiation constants of f - node n : is the futur pattern + node n : is the future pattern node f : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. @@ -212,6 +212,8 @@ private: std::map< TNode, std::vector< TNode > > d_var_contains; /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; + /** helper for is intance of */ + bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); public: /** compute var contains */ void computeVarContains( Node n ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index bc577fda6..c4bc248d3 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -34,24 +34,26 @@ using namespace CVC4::theory::inst; Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); + Trace("trigger") << "Trigger for " << f << ": " << std::endl; + for( int i=0; i<(int)d_nodes.size(); i++ ){ + Trace("trigger") << " " << d_nodes[i] << std::endl; + } + Trace("trigger") << ", smart triggers = " << smartTriggers << std::endl; if( smartTriggers ){ if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ - d_mg = new InstMatchGenerator( d_nodes[0], qe, matchOption ); + d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); + d_mg->setActiveAdd(); } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); } }else{ - d_mg = new InstMatchGenerator( d_nodes, qe, matchOption ); - } - Trace("trigger") << "Trigger for " << f << ": " << std::endl; - for( int i=0; i<(int)d_nodes.size(); i++ ){ - Trace("trigger") << " " << d_nodes[i] << std::endl; + d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + d_mg->setActiveAdd(); } - Trace("trigger") << std::endl; if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ ++(qe->d_statistics.d_triggers); @@ -59,7 +61,7 @@ d_quantEngine( qe ), d_f( f ){ ++(qe->d_statistics.d_simple_triggers); } }else{ - Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; + Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl; //Notice() << "Multi-trigger for " << f << " : " << std::endl; //Notice() << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); @@ -80,14 +82,14 @@ void Trigger::reset( Node eqc ){ d_mg->reset( eqc, d_quantEngine ); } -bool Trigger::getNextMatch( InstMatch& m ){ - bool retVal = d_mg->getNextMatch( m, d_quantEngine ); +bool Trigger::getNextMatch( Node f, InstMatch& m ){ + bool retVal = d_mg->getNextMatch( f, m, d_quantEngine ); return retVal; } -bool Trigger::getMatch( Node t, InstMatch& m ){ +bool Trigger::getMatch( Node f, Node t, InstMatch& m ){ //FIXME: this assumes d_mg is an inst match generator - return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); + return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine ); } int Trigger::addTerm( Node t ){ @@ -115,6 +117,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& temp.insert( temp.begin(), nodes.begin(), nodes.end() ); std::map< Node, bool > vars; std::map< Node, std::vector< Node > > patterns; + size_t varCount = 0; for( int i=0; i<(int)temp.size(); i++ ){ bool foundVar = false; qe->getTermDatabase()->computeVarContains( temp[i] ); @@ -122,6 +125,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; if( v.getAttribute(InstConstantAttribute())==f ){ if( vars.find( v )==vars.end() ){ + varCount++; vars[ v ] = true; foundVar = true; } @@ -134,32 +138,40 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& patterns[ v ].push_back( temp[i] ); } } - } - //now, minimalize the trigger - for( int i=0; i<(int)trNodes.size(); i++ ){ - bool keepPattern = false; - Node n = trNodes[i]; - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - if( patterns[v].size()==1 ){ - keepPattern = true; - break; - } + if( varCount==f[0].getNumChildren() ){ + break; } - if( !keepPattern ){ - //remove from pattern vector + } + if( varCount<f[0].getNumChildren() ){ + //do not generate multi-trigger if it does not contain all variables + return NULL; + }else{ + //now, minimize the trigger + for( int i=0; i<(int)trNodes.size(); i++ ){ + bool keepPattern = false; + Node n = trNodes[i]; for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - for( int k=0; k<(int)patterns[v].size(); k++ ){ - if( patterns[v][k]==n ){ - patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); - break; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; + for( int k=0; k<(int)patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; + } } } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; } - //remove from trigger nodes - trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); - i--; } } }else{ @@ -322,16 +334,16 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ - Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; - Debug("trigger-filter-instance") << "Old: "; + Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; + Trace("trigger-filter-instance") << "Old: "; for( int i=0; i<(int)patTerms2.size(); i++ ){ - Debug("trigger-filter-instance") << patTerms2[i] << " "; + Trace("trigger-filter-instance") << patTerms2[i] << " "; } - Debug("trigger-filter-instance") << std::endl << "New: "; + Trace("trigger-filter-instance") << std::endl << "New: "; for( int i=0; i<(int)temp.size(); i++ ){ - Debug("trigger-filter-instance") << temp[i] << " "; + Trace("trigger-filter-instance") << temp[i] << " "; } - Debug("trigger-filter-instance") << std::endl; + Trace("trigger-filter-instance") << std::endl; } if( tstrt==TS_ALL ){ patTerms.insert( patTerms.begin(), temp.begin(), temp.end() ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 6fcd316f4..93731283b 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -56,12 +56,12 @@ public: /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */ void reset( Node eqc ); /** get next match. must call reset( eqc ) once before this function. */ - bool getNextMatch( InstMatch& m ); + bool getNextMatch( Node f, InstMatch& m ); /** get the match against ground term or formula t. the trigger and t should have the same shape. Currently the trigger should not be a multi-trigger. */ - bool getMatch( Node t, InstMatch& m); + bool getMatch( Node f, Node t, InstMatch& m); /** add ground term t, called when t is added to the TermDb */ int addTerm( Node t ); /** return whether this is a multi-trigger */ |