From 318e836ed5f6bd76d378dfce1c707b9908a1c5e1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Oct 2012 19:24:37 +0000 Subject: [PATCH] cleanup up some static data members in the quantifiers code --- src/theory/quantifiers/inst_match.cpp | 2 +- .../quantifiers/instantiation_engine.cpp | 10 +- src/theory/quantifiers/instantiation_engine.h | 2 + src/theory/quantifiers/term_database.cpp | 122 +++++++++++++--- src/theory/quantifiers/term_database.h | 52 +++++++ src/theory/quantifiers/trigger.cpp | 132 ++++-------------- src/theory/quantifiers/trigger.h | 39 +----- src/theory/uf/inst_strategy.cpp | 2 +- 8 files changed, 190 insertions(+), 171 deletions(-) diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index d2083ef3d..5f24a3dfa 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -610,7 +610,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& p d_f( f ){ Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl; std::map< Node, std::vector< Node > > var_contains; - Trigger::getVarContains( f, pats, var_contains ); + qe->getTermDatabase()->getVarContains( f, pats, var_contains ); //convert to indicies for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: "; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 727f568c5..fb3098e24 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -30,7 +30,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_setIncomplete( setIncomplete ){ +QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ } @@ -144,25 +144,23 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } -static int ierCounter = 0; - void InstantiationEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_FULL ){ - ierCounter++; + d_ierCounter++; } //determine if we should perform check, based on instWhenMode bool performCheck = false; if( options::instWhenMode()==INST_WHEN_FULL ){ performCheck = ( e >= Theory::EFFORT_FULL ); }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ performCheck = true; } if( performCheck ){ - Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl; + Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 19dac736c..7721552c5 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -36,6 +36,8 @@ private: std::map< Node, Node > d_ce_lit; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; + /** inst round counter */ + int d_ierCounter; private: bool hasAddedCbqiLemma( Node f ); void addCbqiLemma( Node f ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7b5d9e6e2..b41770b7e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -28,26 +28,54 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; - bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ - if( argIndex<(int)n.getNumChildren() ){ - Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); - std::map< Node, TermArgTrie >::iterator it = d_data.find( r ); - if( it==d_data.end() ){ - d_data[r].addTerm2( qe, n, argIndex+1 ); - return true; - }else{ - return it->second.addTerm2( qe, n, argIndex+1 ); - } - }else{ - //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) - d_data[n].d_data.clear(); - return false; - } - } + +bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ + if( argIndex<(int)n.getNumChildren() ){ + Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); + std::map< Node, TermArgTrie >::iterator it = d_data.find( r ); + if( it==d_data.end() ){ + d_data[r].addTerm2( qe, n, argIndex+1 ); + return true; + }else{ + return it->second.addTerm2( qe, n, argIndex+1 ); + } + }else{ + //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) + d_data[n].d_data.clear(); + return false; + } +} + +Trigger* TrTrie::getTrigger2( std::vector< Node >& nodes ){ + if( nodes.empty() ){ + return d_tr; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )!=d_children.end() ){ + return d_children[n]->getTrigger2( nodes ); + }else{ + return NULL; + } + } +} + +void TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ + if( nodes.empty() ){ + d_tr = t; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )==d_children.end() ){ + d_children[n] = new TrTrie; + } + d_children[n]->addTrigger2( nodes, t ); + } +} void TermDb::addTermEfficient( Node n, std::set< Node >& added){ static AvailableInTermDb aitdi; - if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ + if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ //Already processed but new in this branch n.setAttribute(aitdi,true); added.insert( n ); @@ -71,7 +99,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ n.setAttribute(AvailableInTermDb(),true); //if this is an atomic trigger, consider adding it //Call the children? - if( Trigger::isAtomicTrigger( n ) ){ + if( inst::Trigger::isAtomicTrigger( n ) ){ if( !n.hasAttribute(InstConstantAttribute()) ){ Debug("term-db") << "register trigger term " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; @@ -370,3 +398,61 @@ const std::vector & TermDb::getParents(TNode n, TNode f, int arg){ static std::vector empty; return empty; } + +void TermDb::computeVarContains( Node n ) { + if( d_var_contains.find( n )==d_var_contains.end() ){ + d_var_contains[n].clear(); + computeVarContains2( n, n ); + } +} + +void TermDb::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 ); + } + } +} + +bool TermDb::isVariableSubsume( Node n1, Node n2 ){ + if( n1==n2 ){ + return true; + }else{ + //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl; + computeVarContains( n1 ); + computeVarContains( n2 ); + for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){ + if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){ + //Notice() << "no" << std::endl; + return false; + } + } + //Notice() << "yes" << std::endl; + return true; + } +} + +void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){ + for( int i=0; i<(int)pats.size(); i++ ){ + computeVarContains( pats[i] ); + varContains[ pats[i] ].clear(); + for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){ + if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){ + varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] ); + } + } + } +} + +void TermDb::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] ); + } + } +} diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 8106b5715..8e3b5b085 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -28,6 +28,10 @@ namespace theory { class QuantifiersEngine; +namespace inst{ + class Trigger; +} + namespace quantifiers { class TermArgTrie { @@ -40,8 +44,34 @@ public: bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } };/* class TermArgTrie */ + +/** a trie of triggers */ +class TrTrie { +private: + inst::Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); +public: + TrTrie() : d_tr( NULL ){} + inst::Trigger* d_tr; + std::map< TNode, TrTrie* > d_children; + inst::Trigger* getTrigger( std::vector< Node >& nodes ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return getTrigger2( temp ); + } + void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return addTrigger2( temp, t ); + } +};/* class inst::Trigger::TrTrie */ + + class TermDb { friend class ::CVC4::theory::QuantifiersEngine; + friend class ::CVC4::theory::inst::Trigger; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -147,6 +177,28 @@ public: const std::vector & nvars); /** get free variable for instantiation constant */ Node getFreeVariableForInstConstant( Node n ); + +//for triggers +private: + /** helper function for compute var contains */ + void computeVarContains2( Node n, Node parent ); + /** all triggers will be stored in this trie */ + TrTrie d_tr_trie; + /** var contains */ + std::map< TNode, std::vector< TNode > > d_var_contains; +public: + /** compute var contains */ + void computeVarContains( Node n ); + /** variables subsume, return true if n1 contains all free variables in n2 */ + bool isVariableSubsume( Node n1, Node n2 ); + /** get var contains for each of the patterns in pats */ + void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); + /** get var contains for node n */ + void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** get trigger */ + inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); } + /** add trigger */ + void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ d_tr_trie.addTrigger( nodes, t ); } };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 49a1f8332..f197c0885 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -31,36 +32,6 @@ using namespace CVC4::theory::inst; //#define NESTED_PATTERN_SELECTION -Trigger* Trigger::TrTrie::getTrigger2( std::vector< Node >& nodes ){ - if( nodes.empty() ){ - return d_tr; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )!=d_children.end() ){ - return d_children[n]->getTrigger2( nodes ); - }else{ - return NULL; - } - } -} -void Trigger::TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ - if( nodes.empty() ){ - d_tr = t; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )==d_children.end() ){ - d_children[n] = new TrTrie; - } - d_children[n]->addTrigger2( nodes, t ); - } -} - -/** trigger static members */ -std::map< TNode, std::vector< TNode > > Trigger::d_var_contains; -Trigger::TrTrie Trigger::d_tr_trie; - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ @@ -104,24 +75,6 @@ d_quantEngine( qe ), d_f( f ){ } } } -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 ); @@ -169,9 +122,9 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& 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]; + 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( vars.find( v )==vars.end() ){ vars[ v ] = true; @@ -181,8 +134,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } 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]; + 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]; patterns[ v ].push_back( temp[i] ); } } @@ -191,8 +144,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& 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]; + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; if( patterns[v].size()==1 ){ keepPattern = true; break; @@ -200,8 +153,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } 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 j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->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 ); @@ -222,7 +175,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& if( trOption==TR_MAKE_NEW ){ //static int trNew = 0; //static int trOld = 0; - //Trigger* t = d_tr_trie.getTrigger( trNodes ); + //Trigger* t = qe->getTermDatabase()->getTrigger( trNodes ); //if( t ){ // trOld++; //}else{ @@ -232,7 +185,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& // Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl; //} }else{ - Trigger* t = d_tr_trie.getTrigger( trNodes ); + Trigger* t = qe->getTermDatabase()->getTrigger( trNodes ); if( t ){ if( trOption==TR_GET_OLD ){ //just return old trigger @@ -243,7 +196,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - d_tr_trie.addTrigger( trNodes, t ); + qe->getTermDatabase()->addTrigger( trNodes, t ); return t; } Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ @@ -302,13 +255,13 @@ bool Trigger::isSimpleTrigger( Node n ){ } /** filter all nodes that have instances */ -void Trigger::filterInstances( std::vector< Node >& nodes ){ +void Trigger::filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ){ std::vector< bool > active; active.resize( nodes.size(), true ); for( int i=0; i<(int)nodes.size(); i++ ){ for( int j=i+1; j<(int)nodes.size(); j++ ){ if( active[i] && active[j] ){ - int result = isInstanceOf( nodes[i], nodes[j] ); + int result = isInstanceOf( qe, nodes[i], nodes[j] ); if( result==1 ){ active[j] = false; }else if( result==-1 ){ @@ -396,7 +349,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - filterInstances( temp ); + filterInstances( qe, temp ); if( temp.size()!=patTerms2.size() ){ Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; Debug("trigger-filter-instance") << "Old: "; @@ -430,7 +383,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } /** is n1 an instance of n2 or vice versa? */ -int Trigger::isInstanceOf( Node n1, Node n2 ){ +int Trigger::isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ){ if( n1==n2 ){ return 1; }else if( n1.getKind()==n2.getKind() ){ @@ -439,7 +392,7 @@ int Trigger::isInstanceOf( Node n1, Node n2 ){ int result = 0; for( int i=0; i<(int)n1.getNumChildren(); i++ ){ if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf( n1[i], n2[i] ); + int cResult = isInstanceOf( qe, n1[i], n2[i] ); if( cResult==0 ){ return 0; }else if( cResult!=result ){ @@ -456,64 +409,27 @@ int Trigger::isInstanceOf( Node n1, Node n2 ){ } return 0; }else if( n2.getKind()==INST_CONSTANT ){ - computeVarContains( n1 ); + qe->getTermDatabase()->computeVarContains( n1 ); //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ // return 1; //} - if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){ + if( qe->getTermDatabase()->d_var_contains[ n1 ].size()==1 && + qe->getTermDatabase()->d_var_contains[ n1 ][ 0 ]==n2 ){ return 1; } }else if( n1.getKind()==INST_CONSTANT ){ - computeVarContains( n2 ); + qe->getTermDatabase()->computeVarContains( n2 ); //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ // return -1; //} - if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){ + if( qe->getTermDatabase()->d_var_contains[ n2 ].size()==1 && + qe->getTermDatabase()->d_var_contains[ n2 ][ 0 ]==n1 ){ return 1; } } return 0; } -bool Trigger::isVariableSubsume( Node n1, Node n2 ){ - if( n1==n2 ){ - return true; - }else{ - //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl; - computeVarContains( n1 ); - computeVarContains( n2 ); - for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){ - if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){ - //Notice() << "no" << std::endl; - return false; - } - } - //Notice() << "yes" << std::endl; - return true; - } -} - -void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){ - for( int i=0; i<(int)pats.size(); i++ ){ - computeVarContains( pats[i] ); - varContains[ pats[i] ].clear(); - for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){ - if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){ - varContains[ pats[i] ].push_back( d_var_contains[pats[i]][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 ){ Assert( coeffs.empty() ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 207cef5d9..686fda241 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -27,11 +27,6 @@ namespace inst { //a collect of nodes representing a trigger class Trigger { -private: - /** computation of variable contains */ - static std::map< TNode, std::vector< TNode > > d_var_contains; - static void computeVarContains( Node n ); - static void computeVarContains2( Node n, Node parent ); private: /** the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -39,31 +34,6 @@ private: Node d_f; /** match generators */ IMGenerator* d_mg; -private: - /** a trie of triggers */ - class TrTrie { - private: - Trigger* getTrigger2( std::vector< Node >& nodes ); - void addTrigger2( std::vector< Node >& nodes, Trigger* t ); - public: - TrTrie() : d_tr( NULL ){} - Trigger* d_tr; - std::map< TNode, TrTrie* > d_children; - Trigger* getTrigger( std::vector< Node >& nodes ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return getTrigger2( temp ); - } - void addTrigger( std::vector< Node >& nodes, Trigger* t ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return addTrigger2( temp, t ); - } - };/* class Trigger::TrTrie */ - /** all triggers will be stored in this trie */ - static TrTrie d_tr_trie; private: /** trigger constructor */ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false ); @@ -138,14 +108,9 @@ public: static bool isAtomicTrigger( Node n ); static bool isSimpleTrigger( Node n ); /** filter all nodes that have instances */ - static void filterInstances( std::vector< Node >& nodes ); + static void filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ); /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf( Node n1, Node n2 ); - /** variables subsume, return true if n1 contains all free variables in n2 */ - static bool isVariableSubsume( Node n1, Node n2 ); - /** get var contains */ - static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); - static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + static int isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ); /** get pattern arithmetic */ static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 9d644ae8d..5ce88177a 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -236,7 +236,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers std::map< Node, std::vector< Node > > varContains; - Trigger::getVarContains( f, patTermsF, varContains ); + d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains ); for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ if( it->second.size()==f[0].getNumChildren() ){ d_patTerms[0][f].push_back( it->first ); -- 2.30.2