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: ";
using namespace CVC4::theory::quantifiers;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ){
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
}
}
}
-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);
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 );
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 );
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;
static std::vector<Node> 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] );
+ }
+ }
+}
class QuantifiersEngine;
+namespace inst{
+ class Trigger;
+}
+
namespace quantifiers {
class TermArgTrie {
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;
const std::vector<Node> & 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 */
#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;
//#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 ){
}
}
}
-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 );
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;
}
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] );
}
}
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;
}
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 );
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{
// 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
}
}
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 ){
}
/** 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 ){
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: ";
}
/** 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() ){
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 ){
}
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() );
//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;
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 );
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 );
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 );
projects / cvc5.git / commitdiff