From ce6c89be30b18a331fd08f843b9d4ee8d6bb1ced Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 25 Aug 2014 12:50:55 +0200 Subject: [PATCH] New option --purify-triggers. Refactoring of InstMatchGenerator. --- .../quantifiers/inst_match_generator.cpp | 135 ++++++++++++------ src/theory/quantifiers/inst_match_generator.h | 47 +++++- src/theory/quantifiers/options | 2 + src/theory/quantifiers/trigger.cpp | 89 +++++++++++- src/theory/quantifiers/trigger.h | 5 + src/theory/quantifiers_engine.cpp | 1 + 6 files changed, 230 insertions(+), 49 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 6faa5ffca..6dbe1ec42 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -30,14 +30,21 @@ namespace CVC4 { namespace theory { namespace inst { - -InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){ +InstMatchGenerator::InstMatchGenerator( Node pat ){ d_needsReset = true; d_active_add = false; Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); d_pattern = pat; d_match_pattern = pat; d_next = NULL; + d_matchPolicy = MATCH_GEN_DEFAULT; +} + +InstMatchGenerator::InstMatchGenerator() { + d_needsReset = true; + d_active_add = false; + d_next = NULL; + d_matchPolicy = MATCH_GEN_DEFAULT; } void InstMatchGenerator::setActiveAdd(bool val){ @@ -89,24 +96,28 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern ); //now, collect children of d_match_pattern - int childMatchPolicy = MATCH_GEN_DEFAULT; + //int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ - if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy ); + InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( 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 ); } + }else{ + d_children_types.push_back( -1 ); } } //create candidate generator if( d_match_pattern.getKind()==INST_CONSTANT ){ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); - } - else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ - Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); + }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ //candidates will be all equalities @@ -139,15 +150,6 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } - for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - Node vv = d_match_pattern[i]; - if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - vv = d_match_pattern[i][0]; - } - d_var_num[i] = vv.getAttribute(InstVarNumAttribute()); - } - } } } @@ -157,6 +159,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ + Trace("matching-fail") << "Internal error for match generator." << std::endl; return false; }else{ EqualityQuery* q = qe->getEqualityQuery(); @@ -171,23 +174,19 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi 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 for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - Node tt = t[i]; - if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] )); - } - bool addToPrev = m.get( d_var_num[i] ).isNull(); - if( !m.set( qe, d_var_num[i], tt ) ){ - //match is in conflict - Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << tt << std::endl; - success = false; - break; - }else if( addToPrev ){ - prev.push_back( d_var_num[i] ); - } + if( d_children_types[i]==0 ){ + Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl; + bool addToPrev = m.get( d_var_num[i] ).isNull(); + if( !m.set( qe, d_var_num[i], t[i] ) ){ + //match is in conflict + Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl; + success = false; + break; + }else if( addToPrev ){ + Trace("matching-debug2") << "Success." << std::endl; + prev.push_back( d_var_num[i] ); } - }else{ + }else if( d_children_types[i]==-1 ){ if( !q->areEqual( d_match_pattern[i], t[i] ) ){ Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; //ground arguments are not equal @@ -239,15 +238,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Node rep = q->getRepresentative( t[ d_children_index[i] ] ); d_children[i]->reset( rep, qe ); } - 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, false ); - Trace("active-add") << "Success = " << success << std::endl; - } - } + success = continueNextMatch( f, m, qe ); } if( !success ){ //m = InstMatch( &prev ); @@ -259,6 +250,18 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } +bool InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ + if( d_next!=NULL ){ + return d_next->getNextMatch( f, m, qe ); + }else{ + if( d_active_add ){ + return qe->addInstantiation( f, m, false ); + }else{ + return true; + } + } +} + /** reset instantiation round */ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ if( !d_match_pattern.isNull() ){ @@ -384,6 +387,54 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node return oinit; } +VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) : + InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) { + d_var_num[0] = var.getAttribute(InstVarNumAttribute()); +} + +bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { + if( !d_eq_class.isNull() ){ + Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); + d_eq_class = Node::null(); + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; + }else{ + return continueNextMatch( f, m, qe ); + } + }else{ + if( d_rm_prev ){ + m.d_vals[d_var_num[0]] = Node::null(); + } + return false; + } +} + +VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : + InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ + d_var_num[0] = d_var.getAttribute(InstVarNumAttribute()); +} + +bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { + if( !d_eq_class.isNull() ){ + Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; + Node s = d_subs.substitute( d_var, d_eq_class ); + Trace("var-trigger-matching") << "...got " << s << std::endl; + d_eq_class = Node::null(); + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; + }else{ + return continueNextMatch( f, m, qe ); + } + }else{ + if( d_rm_prev ){ + m.d_vals[d_var_num[0]] = Node::null(); + } + return false; + } +} + /** constructors */ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) : d_f( f ){ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 56eaf2c17..aa5d37713 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -42,7 +42,7 @@ public: /** 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; + virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; } /** set active add */ virtual void setActiveAdd( bool val ) {} };/* class IMGenerator */ @@ -50,7 +50,7 @@ public: class CandidateGenerator; class InstMatchGenerator : public IMGenerator { -private: +protected: bool d_needsReset; /** candidate generator */ CandidateGenerator* d_cg; @@ -63,17 +63,18 @@ private: InstMatchGenerator* d_next; /** eq class */ Node d_eq_class; - /** for arithmetic matching */ - std::map< Node, Node > d_arith_coeffs; /** variable numbers */ std::map< int, int > d_var_num; /** initialize pattern */ void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ); + /** children types 0 : variable, 1 : child term, -1 : ground term */ + std::vector< int > d_children_types; + /** continue */ + bool continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); public: enum { //options for producing matches MATCH_GEN_DEFAULT = 0, - MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers //others (internally used) MATCH_GEN_INTERNAL_ERROR, }; @@ -85,7 +86,8 @@ public: bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ); /** constructors */ - InstMatchGenerator( Node pat, int matchOption = 0 ); + InstMatchGenerator( Node pat ); + InstMatchGenerator(); /** destructor */ ~InstMatchGenerator(){} /** The pattern we are producing matches for. @@ -115,6 +117,39 @@ public: static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ); };/* class InstMatchGenerator */ +//match generator for boolean term ITEs +class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { +public: + VarMatchGeneratorBooleanTerm( Node var, Node comp ); + Node d_comp; + bool d_rm_prev; + /** reset instantiation round (call this at beginning of instantiation round) */ + void resetInstantiationRound( QuantifiersEngine* qe ){} + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; } + /** get the next match. must call reset( eqc ) before this function. */ + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + /** add instantiations directly */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; } +}; + +//match generator for purified terms (matched term is substituted into d_subs) +class VarMatchGeneratorTermSubs : public InstMatchGenerator { +public: + VarMatchGeneratorTermSubs( Node var, Node subs ); + TNode d_var; + Node d_subs; + bool d_rm_prev; + /** reset instantiation round (call this at beginning of instantiation round) */ + void resetInstantiationRound( QuantifiersEngine* qe ){} + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; } + /** get the next match. must call reset( eqc ) before this function. */ + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + /** add instantiations directly */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; } +}; + /** smart multi-trigger implementation */ class InstMatchGeneratorMulti : public IMGenerator { private: diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index bdd852adb..f33f1ce83 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -63,6 +63,8 @@ option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false choose relational triggers such as x = f(y), x >= f(y) +option purifyTriggers --purify-triggers bool :default false + purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h" selection mode for triggers diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c6ee48057..856ac782c 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ Kind k = n.getKind(); - return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || + return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || ( k!=APPLY_UF && isAtomicTriggerKind( k ) ); } bool Trigger::isAtomicTriggerKind( Kind k ) { @@ -503,6 +503,93 @@ bool Trigger::isBooleanTermTrigger( Node n ) { return false; } +Node Trigger::getInversionVariable( Node n ) { + if( n.getKind()==INST_CONSTANT ){ + return n; + }else if( n.getKind()==PLUS || n.getKind()==MULT ){ + Node ret; + for( unsigned i=0; i(); + if( r!=Rational(-1) && r!=Rational(1) ){ + Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl; + return Node::null(); + } + } + } + } + return ret; + }else{ + Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl; + } + return Node::null(); +} + +Node Trigger::getInversion( Node n, Node x ) { + if( n.getKind()==INST_CONSTANT ){ + return x; + }else if( n.getKind()==PLUS || n.getKind()==MULT ){ + int cindex = -1; + for( unsigned i=0; imkNode( MINUS, x, n[i] ); + }else if( n.getKind()==MULT ){ + Assert( n[i].isConst() ); + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst() ); + x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + } + }else{ + Assert( cindex==-1 ); + cindex = i; + } + } + Assert( cindex!=-1 ); + return getInversion( n[cindex], x ); + } + return Node::null(); +} + +InstMatchGenerator* Trigger::getInstMatchGenerator( Node n ) { + if( n.getKind()==INST_CONSTANT ){ + return NULL; + }else{ + Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl; + if( isBooleanTermTrigger( n ) ){ + VarMatchGeneratorBooleanTerm* vmg = new VarMatchGeneratorBooleanTerm( n[0], n[1] ); + Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] << std::endl; + return vmg; + }else{ + Node x; + if( options::purifyTriggers() ){ + x = getInversionVariable( n ); + } + if( !x.isNull() ){ + Node s = getInversion( n, x ); + VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs( x, s ); + Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl; + return vmg; + }else{ + return new InstMatchGenerator( n ); + } + } + } +} + Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ if( nodes.empty() ){ return d_tr; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 17da6f0d5..42b7598ea 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -30,6 +30,7 @@ class QuantifiersEngine; namespace inst { class IMGenerator; +class InstMatchGenerator; //a collect of nodes representing a trigger class Trigger { @@ -112,6 +113,10 @@ public: /** get pattern arithmetic */ static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ); static bool isBooleanTermTrigger( Node n ); + /** return data structure for producing matches for this trigger. */ + static InstMatchGenerator* getInstMatchGenerator( Node n ); + static Node getInversionVariable( Node n ); + static Node getInversion( Node n, Node x ); inline void toStream(std::ostream& out) const { /* diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e54dfe42f..03143ab9c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -664,6 +664,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //add the instantiation + Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); //report the result if( addedInst ){ -- 2.30.2