diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 145 |
1 files changed, 103 insertions, 42 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cab94fb5c..39063942d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -28,8 +28,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -//#define NESTED_PATTERN_SELECTION - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ @@ -46,7 +44,7 @@ d_quantEngine( qe ), d_f( f ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); @@ -55,7 +53,7 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -75,6 +73,7 @@ d_quantEngine( qe ), d_f( f ){ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } + Trace("trigger-debug") << "Finished making trigger." << std::endl; } void Trigger::resetInstantiationRound(){ @@ -126,7 +125,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& qe->getTermDatabase()->computeVarContains( temp[i] ); for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( v.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(v)==f ){ if( vars.find( v )==vars.end() ){ varCount++; vars[ v ] = true; @@ -146,6 +145,12 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } if( varCount<f[0].getNumChildren() ){ + Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; + for( unsigned i=0; i<nodes.size(); i++) { + Trace("trigger-debug") << nodes[i] << " "; + } + Trace("trigger-debug") << std::endl; + //do not generate multi-trigger if it does not contain all variables return NULL; }else{ @@ -225,7 +230,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } bool Trigger::isUsable( Node n, Node f ){ - if( n.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( !isUsable( n[i], f ) ){ @@ -249,11 +254,71 @@ bool Trigger::isUsable( Node n, Node f ){ } } +bool nodeContainsVar( Node n, Node v ){ + if( n==v) { + return true; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++) { + if( nodeContainsVar(n[i], v) ){ + return true; + } + } + return false; + } +} + +Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + Node rtr; + for( unsigned i=0; i<2; i++) { + unsigned j = (i==0) ? 1 : 0; + if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) { + rtr = n; + break; + } + } + if( n[0].getType().isInteger() ){ + //try to rearrange? + std::map< Node, Node > m; + if (QuantArith::getMonomialSumLit(n, m) ){ + for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ + if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ + Node veq; + if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){ + int vti = veq[0]==it->first ? 1 : 0; + if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ + rtr = veq; + } + } + } + } + } + } + if( !rtr.isNull() ){ + Trace("relational-trigger") << "Relational trigger : " << std::endl; + Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; + Trace("relational-trigger") << " in quantifier " << f << std::endl; + if( hasPol ){ + Trace("relational-trigger") << " polarity : " << pol << std::endl; + } + Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; + return rtr2; + } + } + } + bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); + Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; + if( usable ){ + return n; + }else{ + return Node::null(); + } +} + bool Trigger::isUsableTrigger( Node n, Node f ){ - //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; - bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << usable << std::endl; - return usable; + Node nu = getIsUsableTrigger(n,f); + return !nu.isNull(); } bool Trigger::isAtomicTrigger( Node n ){ @@ -263,7 +328,7 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ return false; } } @@ -274,55 +339,51 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; + bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else return false; -#endif }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; }else{ - return false; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; + return true; + }else{ + return false; + } } } }else{ bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ return true; }else{ retVal = true; } } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ + if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } @@ -367,7 +428,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt ); + collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); @@ -380,9 +441,9 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff Assert( coeffs.empty() ); NodeBuilder<> t(kind::PLUS); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ if( n[i].getKind()==INST_CONSTANT ){ - if( n[i].getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ coeffs[ n[i] ] = Node::null(); }else{ coeffs.clear(); @@ -405,13 +466,13 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff } return true; }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){ - if( !n[1].hasAttribute(InstConstantAttribute()) ){ + if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){ coeffs[ n[0] ] = n[1]; return true; } - }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){ - if( !n[0].hasAttribute(InstConstantAttribute()) ){ + }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ coeffs[ n[1] ] = n[0]; return true; } |