From 520c5903a4c399b7c5beaa2d353bbf9324009ee7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2015 19:47:32 +0200 Subject: [PATCH] Fixes related to cbqi + E-matching. --- .../quantifiers/inst_match_generator.cpp | 75 ++++++++++++------- src/theory/quantifiers/inst_match_generator.h | 7 +- src/theory/quantifiers/trigger.cpp | 6 +- src/theory/quantifiers/trigger.h | 2 +- 4 files changed, 54 insertions(+), 36 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index de8e45a84..941eaf89b 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -40,6 +40,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ d_match_pattern_type = pat.getType(); d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; + d_eq_class_rel = false; } InstMatchGenerator::InstMatchGenerator() { @@ -56,7 +57,7 @@ void InstMatchGenerator::setActiveAdd(bool val){ } } -void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){ +void InstMatchGenerator::initialize( Node q, 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 ){ @@ -103,16 +104,21 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //now, collect children of d_match_pattern //int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ - InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( d_match_pattern[i] ); + Node qa = quantifiers::TermDb::getInstConstAttr(d_match_pattern[i]); + if( !qa.isNull() ){ + InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, d_match_pattern[i] ); if( cimg ){ d_children.push_back( cimg ); d_children_index.push_back( i ); gens.push_back( cimg ); d_children_types.push_back( 1 ); }else{ - d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); - d_children_types.push_back( 0 ); + if( d_match_pattern[i].getKind()==INST_CONSTANT && qa==q ){ + d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); + d_children_types.push_back( 0 ); + }else{ + d_children_types.push_back( -1 ); + } } }else{ d_children_types.push_back( -1 ); @@ -157,6 +163,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } + d_eq_class_rel = true; Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op ); @@ -191,6 +198,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() ); Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); //first, check if ground arguments are not equal, or a match is in conflict + Trace("matching-debug2") << "Setting immediate matches..." << std::endl; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( d_children_types[i]==0 ){ Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl; @@ -213,6 +221,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } } + Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl; //for variable matching if( d_match_pattern.getKind()==INST_CONSTANT ){ bool addToPrev = m.get( d_var_num[0] ).isNull(); @@ -224,7 +233,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } //for relational matching - }else if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){ + }else if( d_eq_class_rel && d_eq_class.getKind()==INST_CONSTANT ){ int v = d_eq_class.getAttribute(InstVarNumAttribute()); //also must fit match to equivalence class bool pol = d_pattern.getKind()!=NOT; @@ -260,11 +269,13 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } if( success ){ + Trace("matching-debug2") << "Reset children..." << std::endl; //now, fit children into match //we will be requesting candidates for matching terms for each child for( int i=0; i<(int)d_children.size(); i++ ){ d_children[i]->reset( t[ d_children_index[i] ], qe ); } + Trace("matching-debug2") << "Continue next " << d_next << std::endl; success = continueNextMatch( f, m, qe ); } if( !success ){ @@ -312,14 +323,14 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ //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.getKind()==INST_CONSTANT ? Node::null() : d_eq_class ); + d_cg->reset( d_eq_class_rel ? Node::null() : d_eq_class ); d_needsReset = false; } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; - reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); + reset( d_eq_class_rel ? Node::null() : d_eq_class, qe ); } m.d_matched = Node::null(); Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; @@ -338,7 +349,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* if( !success ){ Trace("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); + reset( d_eq_class_rel ? Node::null() : d_eq_class, qe ); } return success; } @@ -382,13 +393,13 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ) { +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) { std::vector< Node > pats; pats.push_back( pat ); - return mkInstMatchGenerator( pats, qe ); + return mkInstMatchGenerator( q, pats, qe ); } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ) { +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) { size_t pCounter = 0; InstMatchGenerator* prev = NULL; InstMatchGenerator* oinit = NULL; @@ -406,7 +417,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node if( prev ){ prev->d_next = curr; } - curr->initialize(qe, gens); + curr->initialize(q, qe, gens); prev = curr; counter++; } @@ -488,7 +499,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( InstMatchGenerator::mkInstMatchGenerator( n, qe ) ); + d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(f, n, qe ) ); //compute unique/shared variables std::vector< int > unique_vars; std::map< int, bool > shared_vars; @@ -688,7 +699,11 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) { for( unsigned i=0; i::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - Node t = it->first; - Node prev = m.get( v ); - //using representatives, just check if equal - if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){ - m.setValue( v, t); - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - m.setValue( v, prev); + if( v!=-1 ){ + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ + Node t = it->first; + Node prev = m.get( v ); + //using representatives, just check if equal + if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){ + m.setValue( v, t); + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + m.setValue( v, prev); + } } + return; } - }else{ - Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); - if( it!=tat->d_data.end() ){ - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - } + } + Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); + std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + if( it!=tat->d_data.end() ){ + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); } } } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index f9853ef54..aae6d4e73 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -64,10 +64,11 @@ protected: InstMatchGenerator* d_next; /** eq class */ Node d_eq_class; + bool d_eq_class_rel; /** variable numbers */ std::map< int, int > d_var_num; /** initialize pattern */ - void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ); + void initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ); /** children types 0 : variable, 1 : child term, -1 : ground term */ std::vector< int > d_children_types; /** continue */ @@ -116,8 +117,8 @@ public: bool d_active_add; void setActiveAdd( bool val ); - static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ); - static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ); + static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ); + static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); };/* class InstMatchGenerator */ //match generator for boolean term ITEs diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index e9ce29468..c55ed27ea 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -43,7 +43,7 @@ d_quantEngine( qe ), d_f( f ){ if( isSimpleTrigger( d_nodes[0] ) ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe ); d_mg->setActiveAdd(true); } }else{ @@ -52,7 +52,7 @@ d_quantEngine( qe ), d_f( f ){ //d_mg->setActiveAdd(); } }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe ); d_mg->setActiveAdd(true); } if( d_nodes.size()==1 ){ @@ -553,7 +553,7 @@ Node Trigger::getInversion( Node n, Node x ) { return Node::null(); } -InstMatchGenerator* Trigger::getInstMatchGenerator( Node n ) { +InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { if( n.getKind()==INST_CONSTANT ){ return NULL; }else{ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 28da9f959..60e268a4f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -113,7 +113,7 @@ public: static bool isPureTheoryTrigger( Node n ); static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ - static InstMatchGenerator* getInstMatchGenerator( Node n ); + static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); static Node getInversionVariable( Node n ); static Node getInversion( Node n, Node x ); -- 2.30.2