diff options
Diffstat (limited to 'src/theory/rr_trigger.cpp')
| -rw-r--r-- | src/theory/rr_trigger.cpp | 444 |
1 files changed, 222 insertions, 222 deletions
diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp index 52e7efcc2..ece68d137 100644 --- a/src/theory/rr_trigger.cpp +++ b/src/theory/rr_trigger.cpp @@ -75,156 +75,156 @@ d_quantEngine( qe ), d_f( f ){ }else{ ++(qe->d_statistics.d_simple_triggers); } - }else{
+ }else{ Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; //std::cout << "Multi-trigger for " << f << " : " << std::endl; //std::cout << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); } -}
-void Trigger::computeVarContains( Node n ) {
- if( d_var_contains.find( n )==d_var_contains.end() ){
- d_var_contains[n].clear();
- computeVarContains2( n, n );
- }
-}
-
-void Trigger::computeVarContains2( Node n, Node parent ){
- if( n.getKind()==INST_CONSTANT ){
- if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
- d_var_contains[parent].push_back( n );
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- computeVarContains2( n[i], parent );
- }
- }
} -
-void Trigger::resetInstantiationRound(){
- d_mg->resetInstantiationRound( d_quantEngine );
-}
-
+void Trigger::computeVarContains( Node n ) { + if( d_var_contains.find( n )==d_var_contains.end() ){ + d_var_contains[n].clear(); + computeVarContains2( n, n ); + } +} + +void Trigger::computeVarContains2( Node n, Node parent ){ + if( n.getKind()==INST_CONSTANT ){ + if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ + d_var_contains[parent].push_back( n ); + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + computeVarContains2( n[i], parent ); + } + } +} + +void Trigger::resetInstantiationRound(){ + d_mg->resetInstantiationRound( d_quantEngine ); +} -bool Trigger::getNextMatch(){
- bool retVal = d_mg->getNextMatch( d_quantEngine );
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- return retVal;
-}
+ +bool Trigger::getNextMatch(){ + bool retVal = d_mg->getNextMatch( d_quantEngine ); + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + return retVal; +} // bool Trigger::getMatch( Node t, InstMatch& m ){ // //FIXME: this assumes d_mg is an inst match generator // return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); // } -
-int Trigger::addInstantiations( InstMatch& baseMatch ){
+ +int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( baseMatch, d_nodes[0].getAttribute(InstConstantAttribute()), - d_quantEngine);
- if( addedLemmas>0 ){
+ d_quantEngine); + if( addedLemmas>0 ){ Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; for( int i=0; i<(int)d_nodes.size(); i++ ){ Debug("inst-trigger") << d_nodes[i] << " "; } - Debug("inst-trigger") << std::endl;
- }
- return addedLemmas;
-}
-
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
- bool smartTriggers ){
- std::vector< Node > trNodes;
- if( !keepAll ){
- //only take nodes that contribute variables to the trigger when added
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::map< Node, bool > vars;
- std::map< Node, std::vector< Node > > patterns;
- for( int i=0; i<(int)temp.size(); i++ ){
- bool foundVar = false;
- computeVarContains( temp[i] );
- for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
- Node v = d_var_contains[ temp[i] ][j];
- if( v.getAttribute(InstConstantAttribute())==f ){
- if( vars.find( v )==vars.end() ){
- vars[ v ] = true;
- foundVar = true;
- }
- }
- }
- if( foundVar ){
- trNodes.push_back( temp[i] );
- for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
- Node v = d_var_contains[ temp[i] ][j];
- patterns[ v ].push_back( temp[i] );
- }
- }
- }
- //now, minimalize the trigger
- for( int i=0; i<(int)trNodes.size(); i++ ){
- bool keepPattern = false;
- Node n = trNodes[i];
- for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
- Node v = d_var_contains[ n ][j];
- if( patterns[v].size()==1 ){
- keepPattern = true;
- break;
- }
- }
- if( !keepPattern ){
- //remove from pattern vector
- for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
- Node v = d_var_contains[ n ][j];
- for( int k=0; k<(int)patterns[v].size(); k++ ){
- if( patterns[v][k]==n ){
- patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
- break;
- }
- }
- }
- //remove from trigger nodes
- trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
- i--;
- }
- }
- }else{
- trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
- }
-
- //check for duplicate?
- if( trOption==TR_MAKE_NEW ){
- //static int trNew = 0;
- //static int trOld = 0;
- //Trigger* t = d_tr_trie.getTrigger( trNodes );
- //if( t ){
- // trOld++;
- //}else{
- // trNew++;
- //}
- //if( (trNew+trOld)%100==0 ){
- // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
- //}
- }else{
- Trigger* t = d_tr_trie.getTrigger( trNodes );
- if( t ){
- if( trOption==TR_GET_OLD ){
- //just return old trigger
- return t;
- }else{
- return NULL;
- }
- }
- }
- Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
- d_tr_trie.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 );
-}
+ Debug("inst-trigger") << std::endl; + } + return addedLemmas; +} + +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, + bool smartTriggers ){ + std::vector< Node > trNodes; + if( !keepAll ){ + //only take nodes that contribute variables to the trigger when added + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::map< Node, bool > vars; + std::map< Node, std::vector< Node > > patterns; + for( int i=0; i<(int)temp.size(); i++ ){ + bool foundVar = false; + computeVarContains( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + if( v.getAttribute(InstConstantAttribute())==f ){ + if( vars.find( v )==vars.end() ){ + vars[ v ] = true; + foundVar = true; + } + } + } + if( foundVar ){ + trNodes.push_back( temp[i] ); + for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ + Node v = d_var_contains[ temp[i] ][j]; + patterns[ v ].push_back( temp[i] ); + } + } + } + //now, minimalize the trigger + for( int i=0; i<(int)trNodes.size(); i++ ){ + bool keepPattern = false; + Node n = trNodes[i]; + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector + for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ + Node v = d_var_contains[ n ][j]; + for( int k=0; k<(int)patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; + } + } + } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; + } + } + }else{ + trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); + } + + //check for duplicate? + if( trOption==TR_MAKE_NEW ){ + //static int trNew = 0; + //static int trOld = 0; + //Trigger* t = d_tr_trie.getTrigger( trNodes ); + //if( t ){ + // trOld++; + //}else{ + // trNew++; + //} + //if( (trNew+trOld)%100==0 ){ + // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; + //} + }else{ + Trigger* t = d_tr_trie.getTrigger( trNodes ); + if( t ){ + if( trOption==TR_GET_OLD ){ + //just return old trigger + return t; + }else{ + return NULL; + } + } + } + Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); + d_tr_trie.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++ ){ @@ -233,25 +233,25 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } } return true; -}
-
-bool Trigger::isUsable( Node n, Node f ){
- if( n.getAttribute(InstConstantAttribute())==f ){
- if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
- std::map< Node, Node > coeffs;
- return getPatternArithmetic( f, n, coeffs );
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !isUsable( n[i], f ) ){
- return false;
- }
- }
- return true;
- }
- }else{
- return true;
- }
-}
+} + +bool Trigger::isUsable( Node n, Node f ){ + if( n.getAttribute(InstConstantAttribute())==f ){ + if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ + std::map< Node, Node > coeffs; + return getPatternArithmetic( f, n, coeffs ); + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( !isUsable( n[i], f ) ){ + return false; + } + } + return true; + } + }else{ + return true; + } +} bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ @@ -293,67 +293,67 @@ void Trigger::filterInstances( std::vector< Node >& nodes ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
- if( patMap.find( n )==patMap.end() ){
- patMap[ n ] = false;
- 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 ) ){
- retVal = true;
- }
- }
- if( retVal ){
- return true;
- }else if( isUsableTrigger( n, f ) ){
- patMap[ n ] = true;
- return true;
- }else{
- return false;
- }
- }
- }else{
- bool retVal = false;
- if( isUsableTrigger( n, f ) ){
- patMap[ n ] = 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{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
- retVal = true;
- }
- }
- }
- return retVal;
- }
- }else{
- return patMap[ n ];
- }
+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ + if( patMap.find( n )==patMap.end() ){ + patMap[ n ] = false; + 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 ) ){ + retVal = true; + } + } + if( retVal ){ + return true; + }else if( isUsableTrigger( n, f ) ){ + patMap[ n ] = true; + return true; + }else{ + return false; + } + } + }else{ + bool retVal = false; + if( isUsableTrigger( n, f ) ){ + patMap[ n ] = 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{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + retVal = true; + } + } + } + return retVal; + } + }else{ + return patMap[ n ]; + } } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, 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 @@ -387,10 +387,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } collectPatTerms2( qe, f, n, patMap, tstrt ); - for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
- if( it->second ){
- patTerms.push_back( it->first );
- }
+ for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ + if( it->second ){ + patTerms.push_back( it->first ); + } } } @@ -469,15 +469,15 @@ void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, } } } -
-void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
- computeVarContains( n );
- for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
- if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
- varContains.push_back( d_var_contains[n][j] );
- }
- }
-}
+ +void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){ + computeVarContains( n ); + for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ + varContains.push_back( d_var_contains[n][j] ); + } + } +} bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ |