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.cpp228
1 files changed, 148 insertions, 80 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c6ee48057..511103019 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -188,19 +188,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
}
//check for duplicate?
- if( trOption==TR_MAKE_NEW ){
- //static int trNew = 0;
- //static int trOld = 0;
- //Trigger* t = qe->getTermDatabase()->getTrigger( trNodes );
- //if( t ){
- // trOld++;
- //}else{
- // trNew++;
- //}
- //if( (trNew+trOld)%100==0 ){
- // Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl;
- //}
- }else{
+ if( trOption!=TR_MAKE_NEW ){
Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
if( t ){
if( trOption==TR_GET_OLD ){
@@ -215,21 +203,13 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
qe->getTriggerDatabase()->addTrigger( trNodes, t );
return t;
}
+
Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
std::vector< Node > nodes;
nodes.push_back( n );
return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
}
-bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
- for( int i=0; i<(int)nodes.size(); i++ ){
- if( !isUsableTrigger( nodes[i], f ) ){
- return false;
- }
- }
- return true;
-}
-
bool Trigger::isUsable( Node n, Node f ){
if( quantifiers::TermDb::getInstConstAttr(n)==f ){
if( isAtomicTrigger( n ) ){
@@ -243,9 +223,7 @@ bool Trigger::isUsable( Node n, Node f ){
return true;
}else{
std::map< Node, Node > coeffs;
- if( isArithmeticTrigger( f, n, coeffs ) ){
- return true;
- }else if( isBooleanTermTrigger( n ) ){
+ if( isBooleanTermTrigger( n ) ){
return true;
}
}
@@ -324,7 +302,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 ) {
@@ -347,7 +325,7 @@ bool Trigger::isSimpleTrigger( Node n ){
}
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){
+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
if( patMap.find( n )==patMap.end() ){
patMap[ n ] = false;
bool newHasPol = n.getKind()==IFF ? false : hasPol;
@@ -359,14 +337,17 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
bool retVal = false;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
retVal = true;
}
}
if( retVal ){
return true;
}else{
- Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+ Node nu;
+ if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+ nu = getIsUsableTrigger( n, f, pol, hasPol );
+ }
if( !nu.isNull() ){
patMap[ nu ] = true;
return true;
@@ -377,7 +358,10 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
}
}else{
bool retVal = false;
- Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+ Node nu;
+ if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+ nu = getIsUsableTrigger( n, f, pol, hasPol );
+ }
if( !nu.isNull() ){
patMap[ nu ] = true;
if( tstrt==TS_MAX_TRIGGER ){
@@ -389,7 +373,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
if( n.getKind()!=FORALL ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
retVal = true;
}
}
@@ -401,12 +385,70 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
}
}
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
+bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) {
+ if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+ bool hasVar = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==APPLY_UF ){
+ return false;
+ }else if( n[i].getKind()==INST_CONSTANT ){
+ hasVar = true;
+ //if( std::find( var_found.begin(), var_found.end(), n[i]
+ }
+ }
+ if( hasVar ){
+ patTerms.push_back( n );
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+bool Trigger::isBooleanTermTrigger( Node n ) {
+ if( n.getKind()==ITE ){
+ //check for boolean term converted to ITE
+ if( n[0].getKind()==INST_CONSTANT &&
+ n[1].getKind()==CONST_BITVECTOR &&
+ n[2].getKind()==CONST_BITVECTOR ){
+ if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
+ n[1].getConst<BitVector>().toInteger()==1 &&
+ n[2].getConst<BitVector>().toInteger()==0 ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool Trigger::isPureTheoryTrigger( Node n ) {
+ if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermDb::hasInstConstAttr( n ) ){
+ return false;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isPureTheoryTrigger( n[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }
+}
+
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& patTerms ) {
+ std::vector< Node > var_found;
+ return isLocalTheoryExt2( n, var_found, patTerms );
+}
+
+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
std::map< Node, bool > patMap;
if( filterInst ){
//immediately do not consider any term t for which another term is an instance of t
std::vector< Node > patTerms2;
- collectPatTerms( qe, f, n, patTerms2, TS_ALL, false );
+ collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false );
std::vector< Node > temp;
temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
qe->getTermDatabase()->filterInstances( temp );
@@ -434,7 +476,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
}
}
}
- collectPatTerms2( qe, f, n, patMap, tstrt, true, true );
+ collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true );
for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
if( it->second ){
patTerms.push_back( it->first );
@@ -442,65 +484,91 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
}
}
-bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){
- if( n.getKind()==PLUS ){
- Assert( coeffs.empty() );
- NodeBuilder<> t(kind::PLUS);
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+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<n.getNumChildren(); i++ ){
if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
- if( n[i].getKind()==INST_CONSTANT ){
- if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
- coeffs[ n[i] ] = Node::null();
- }else{
- coeffs.clear();
- return false;
+ if( ret.isNull() ){
+ ret = getInversionVariable( n[i] );
+ if( ret.isNull() ){
+ Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
+ return Node::null();
+ }
+ }else{
+ return Node::null();
+ }
+ }else if( n.getKind()==MULT ){
+ if( !n[i].isConst() ){
+ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
+ return Node::null();
+ }else if( n.getType().isInteger() ){
+ Rational r = n[i].getConst<Rational>();
+ if( r!=Rational(-1) && r!=Rational(1) ){
+ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
+ return Node::null();
}
- }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){
- coeffs.clear();
- return false;
}
- }else{
- t << n[i];
}
}
- if( t.getNumChildren()==0 ){
- coeffs[ Node::null() ] = NodeManager::currentNM()->mkConst( Rational(0) );
- }else if( t.getNumChildren()==1 ){
- coeffs[ Node::null() ] = t.getChild( 0 );
- }else{
- coeffs[ Node::null() ] = t;
- }
- return true;
- }else if( n.getKind()==MULT ){
- 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 && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
- if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
- coeffs[ n[1] ] = n[0];
- return true;
+ 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; i<n.getNumChildren(); i++ ){
+ if( !quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ if( n.getKind()==PLUS ){
+ x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
+ }else if( n.getKind()==MULT ){
+ Assert( n[i].isConst() );
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
+ x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+ }
+ }else{
+ Assert( cindex==-1 );
+ cindex = i;
}
}
+ Assert( cindex!=-1 );
+ return getInversion( n[cindex], x );
}
- return false;
+ return Node::null();
}
-bool Trigger::isBooleanTermTrigger( Node n ) {
- if( n.getKind()==ITE ){
- //check for boolean term converted to ITE
- if( n[0].getKind()==INST_CONSTANT &&
- n[1].getKind()==CONST_BITVECTOR &&
- n[2].getKind()==CONST_BITVECTOR ){
- if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
- n[1].getConst<BitVector>().toInteger()==1 &&
- n[2].getConst<BitVector>().toInteger()==0 ){
- return true;
+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 );
}
}
}
- return false;
}
Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback