From: Andrew Reynolds Date: Tue, 5 Feb 2013 07:35:21 +0000 (-0600) Subject: More improvements for E-matching X-Git-Tag: cvc5-1.0.0~7426 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58d58ad5da9bbfbe1df338083fbb2a2e7c8d19e9;p=cvc5.git More improvements for E-matching --- diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index e5922e77f..386834385 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -30,116 +30,103 @@ 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::setActiveAdd(){ d_active_add = true; - if( !d_children.empty() ){ - d_children[d_children.size()-1]->setActiveAdd(); - } -} - -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 ) ); + 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 ){ - d_active_add = false; - 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; } } } @@ -157,9 +144,8 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi 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()) ); @@ -169,13 +155,13 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi 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; } } @@ -193,55 +179,25 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi 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( f, 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 ){ - if( d_children.empty() && d_active_add ){ - Trace("active-add") << "Active Adding instantiation " << partial.back() << std::endl; - bool succ = qe->addInstantiation( f, partial.back() ); - Trace("active-add") << "Success = " << succ << std::endl; - return succ; - }else{ - m = partial.back(); - return true; - } - }else{ - return false; + if( !success ){ + m = InstMatch( &prev ); } + return success; } } -bool InstMatchGenerator::getNextMatch2( Node f, 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( f, 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() ){ @@ -314,68 +270,44 @@ 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( 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( f, 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( f, 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( f, m, qe ) ){ - //if( d_active_add ){ - // std::cout << "should not add at top level." << std::endl; - //} if( !d_active_add ){ //m.makeInternal( d_quantEngine->getEqualityQuery() ); m.add( baseMatch ); @@ -386,6 +318,8 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif } } m.clear(); + }else{ + addedLemmas++; } } //return number of lemmas added @@ -409,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 gens; + InstMatchGenerator* init = new InstMatchGenerator(pats[pCounter]); + if(pCounter==0){ + oinit = init; + } + gens.push_back(init); + //chain the resulting match generators together + while (counterd_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 ){ @@ -429,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; diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 602e71ca7..b201fa60f 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -58,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 @@ -77,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( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); /** for arithmetic */ bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: @@ -91,8 +86,7 @@ public: 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. @@ -115,6 +109,9 @@ public: 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 */ 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/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 4b181a807..c4bc248d3 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -34,25 +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);