diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 122 |
1 files changed, 104 insertions, 18 deletions
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<Node> & TermDb::getParents(TNode n, TNode f, int arg){ 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] ); + } + } +} |