summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/trigger.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r--src/theory/quantifiers/trigger.cpp145
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback