diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
| commit | 5ebe47d38892131b96521a729c915365a3369110 (patch) | |
| tree | 59e8f2f3b9de3a9f81e178de7d18124ddc4f3c32 /src/theory/rewriterules | |
| parent | 304404e3709ff7e95156c87f65a3e2647d9f3441 (diff) | |
efficient e-matching now specific to rewrite rules
Diffstat (limited to 'src/theory/rewriterules')
| -rw-r--r-- | src/theory/rewriterules/Makefile.am | 4 | ||||
| -rwxr-xr-x | src/theory/rewriterules/efficient_e_matching.cpp | 679 | ||||
| -rwxr-xr-x | src/theory/rewriterules/efficient_e_matching.h | 447 | ||||
| -rw-r--r-- | src/theory/rewriterules/rr_inst_match.cpp | 10 |
4 files changed, 1134 insertions, 6 deletions
diff --git a/src/theory/rewriterules/Makefile.am b/src/theory/rewriterules/Makefile.am index a9eddb812..1b137e7f0 100644 --- a/src/theory/rewriterules/Makefile.am +++ b/src/theory/rewriterules/Makefile.am @@ -20,7 +20,9 @@ librewriterules_la_SOURCES = \ rr_trigger.h \ rr_trigger.cpp \ rr_candidate_generator.h \ - rr_candidate_generator.cpp + rr_candidate_generator.cpp \ + efficient_e_matching.h \ + efficient_e_matching.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp new file mode 100755 index 000000000..b9d19d391 --- /dev/null +++ b/src/theory/rewriterules/efficient_e_matching.cpp @@ -0,0 +1,679 @@ +/********************* */
+/*! \file efficient_e_matching.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of theory uf instantiator class
+ **/
+
+#include "theory/rewriterules/efficient_e_matching.h"
+#include "theory/rewriterules/rr_candidate_generator.h"
+#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/options.h"
+#include "theory/rewriterules/options.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+
+inline std::ostream& operator<<(std::ostream& out, const EfficientEMatcher::Ips& ips) {
+ return out;
+};
+
+EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){
+
+}
+
+//set member
+void EqClassInfo::setMember( Node n, quantifiers::TermDb* db ){
+ if( n.hasOperator() ){
+ d_funs.insertAtContextLevelZero(n.getOperator(),true);
+ }
+ //add parent functions
+ for( std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction >::iterator it = db->d_parents[n].begin();
+ it != db->d_parents[n].end(); ++it ){
+ //TODO Is it true to do it at level 0? That depend when SetMember is called
+ // At worst it is a good overapproximation
+ d_pfuns.insertAtContextLevelZero( it->first, true);
+ }
+}
+
+//get has function
+bool EqClassInfo::hasFunction( Node op ){
+ return d_funs.find( op )!=d_funs.end();
+}
+
+bool EqClassInfo::hasParent( Node op ){
+ return d_pfuns.find( op )!=d_pfuns.end();
+}
+
+//merge with another eq class info
+void EqClassInfo::merge( EqClassInfo* eci ){
+ for( BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
+ d_funs[ (*it).first ] = true;
+ }
+ for( BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
+ d_pfuns[ (*it).first ] = true;
+ }
+}
+
+inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){
+ Debug(c) << " funs:";
+ for( EqClassInfo::BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
+ Debug(c) << (*it).first << ",";
+ }
+ Debug(c) << std::endl << "pfuns:";
+ for( EqClassInfo::BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
+ Debug(c) << (*it).first << ",";
+ }
+ Debug(c) << std::endl;
+}
+
+
+
+EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_quantEngine( qe )
+{
+
+}
+
+/** new node */
+void EfficientEMatcher::newEqClass( TNode n ){
+
+}
+
+void EfficientEMatcher::newTerms(SetNode& s){
+ static NoMatchAttribute rewrittenNodeAttribute;
+ /* op -> nodes (if the set is empty, the op is not interesting) */
+ std::hash_map< TNode, SetNode, TNodeHashFunction > h;
+ /* types -> nodes (if the set is empty, the type is not interesting) */
+ std::hash_map< TypeNode, SetNode, TypeNodeHashFunction > tyh;
+ for(SetNode::iterator i=s.begin(), end=s.end(); i != end; ++i){
+ if (i->getAttribute(rewrittenNodeAttribute)) continue; /* skip it */
+ if( !d_cand_gens.empty() ){
+ // op
+ TNode op = i->getOperator();
+ std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator
+ is = h.find(op);
+ if(is == h.end()){
+ std::pair<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool>
+ p = h.insert(make_pair(op,SetNode()));
+ is = p.first;
+ if(d_cand_gens.find(op) != d_cand_gens.end()){
+ is->second.insert(*i);
+ } /* else we have inserted an empty set */
+ }else if(!is->second.empty()){
+ is->second.insert(*i);
+ }
+ }
+ if( !d_cand_gen_types.empty() ){
+ //type
+ TypeNode ty = i->getType();
+ std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator
+ is = tyh.find(ty);
+ if(is == tyh.end()){
+ std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool>
+ p = tyh.insert(make_pair(ty,SetNode()));
+ is = p.first;
+ if(d_cand_gen_types.find(ty) != d_cand_gen_types.end()){
+ is->second.insert(*i);
+ } /* else we have inserted an empty set */
+ }else if(!is->second.empty()){
+ is->second.insert(*i);
+ }
+ }
+ }
+ //op
+ for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end();
+ i != end; ++i){
+ //new term, add n to candidate generators
+ if(i->second.empty()) continue;
+ std::map< Node, NodeNewTermDispatcher >::iterator
+ inpc = d_cand_gens.find(i->first);
+ //we know that this op exists
+ Assert(inpc != d_cand_gens.end());
+ inpc->second.send(i->second);
+ }
+ //type
+ for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end();
+ i != end; ++i){
+ //new term, add n to candidate generators
+ if(i->second.empty()) continue;
+ std::map< TypeNode, NodeNewTermDispatcher >::iterator
+ inpc = d_cand_gen_types.find(i->first);
+ //we know that this op exists
+ Assert(inpc != d_cand_gen_types.end());
+ inpc->second.send(i->second);
+ }
+
+}
+
+
+/** merge */
+void EfficientEMatcher::merge( TNode a, TNode b ){
+ if( options::efficientEMatching() ){
+ //merge eqc_ops of b into a
+ EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
+ EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
+
+ if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){
+ Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl;
+
+ //determine new candidates for instantiation
+ computeCandidatesPcPairs( a, eci_a, b, eci_b );
+ computeCandidatesPcPairs( b, eci_b, a, eci_a );
+ computeCandidatesPpPairs( a, eci_a, b, eci_b );
+ computeCandidatesPpPairs( b, eci_b, a, eci_a );
+ }
+ computeCandidatesConstants( a, eci_a, b, eci_b);
+ computeCandidatesConstants( b, eci_b, a, eci_a);
+
+ eci_a->merge( eci_b );
+ }
+}
+
+/** assert terms are disequal */
+void EfficientEMatcher::assertDisequal( TNode a, TNode b, TNode reason ){
+
+}
+
+EqClassInfo* EfficientEMatcher::getEquivalenceClassInfo( Node n ) {
+ return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
+}
+EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){
+ Assert( n==d_quantEngine->getEqualityQuery()->getRepresentative( n ) );
+ if( d_eqc_ops.find( n )==d_eqc_ops.end() ){
+ EqClassInfo* eci = new EqClassInfo( d_quantEngine->getSatContext() );
+ eci->setMember( n, d_quantEngine->getTermDatabase() );
+ d_eqc_ops[n] = eci;
+ }
+ return d_eqc_ops[n];
+}
+
+void EfficientEMatcher::computeCandidatesPcPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
+ Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl;
+ Debug("efficient-e-match") << " Eq class = [";
+ outputEqClass( "efficient-e-match", a);
+ Debug("efficient-e-match") << "]" << std::endl;
+ outputEqClassInfo("efficient-e-match",eci_a);
+ for( EqClassInfo::BoolMap::iterator it = eci_a->d_funs.begin(); it != eci_a->d_funs.end(); it++ ) {
+ //the child function: a member of eq_class( a ) has top symbol g, in other words g is in funs( a )
+ Node g = (*it).first;
+ Debug("efficient-e-match") << " Checking application " << g << std::endl;
+ //look at all parent/child pairs
+ for( std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > >::iterator itf = d_pc_pairs[g].begin();
+ itf != d_pc_pairs[g].end(); ++itf ){
+ //f/g is a parent/child pair
+ Node f = itf->first;
+ if( eci_b->hasParent( f ) ){
+ //DO_THIS: determine if f in pfuns( b ), only do the follow if so
+ Debug("efficient-e-match") << " Checking parent application " << f << std::endl;
+ //scan through the list of inverted path strings/candidate generators
+ for( std::vector< std::pair< NodePcDispatcher*, Ips > >::iterator cit = itf->second.begin();
+ cit != itf->second.end(); ++cit ){
+#ifdef CVC4_DEBUG
+ Debug("efficient-e-match") << " Checking pattern " << cit->first->pat << std::endl;
+#endif
+ Debug("efficient-e-match") << " Check inverted path string for pattern ";
+ outputIps( "efficient-e-match", cit->second );
+ Debug("efficient-e-match") << std::endl;
+
+ //collect all new relevant terms
+ SetNode terms;
+ terms.insert( b );
+ collectTermsIps( cit->second, terms );
+ if( terms.empty() ) continue;
+ Debug("efficient-e-match") << " -> Added terms (" << terms.size() << "): ";
+ for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+ t!=end; ++t ){
+ Debug("efficient-e-match") << (*t) << " ";
+ }
+ Debug("efficient-e-match") << std::endl;
+ //add them as candidates to the candidate generator
+ cit->first->send(terms);
+ }
+ }
+ }
+ }
+}
+
+void EfficientEMatcher::computeCandidatesPpPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
+ Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl;
+ for( std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > >::iterator it = d_pp_pairs.begin();
+ it != d_pp_pairs.end(); ++it ){
+ Node f = it->first;
+ if( eci_a->hasParent( f ) ){
+ Debug("efficient-e-match") << " Checking parent application " << f << std::endl;
+ for( std::map< Node, std::vector< triple<NodePpDispatcher*, Ips, Ips> > >::iterator it2 = it->second.begin();
+ it2 != it->second.end(); ++it2 ){
+ Node g = it2->first;
+ if( eci_b->hasParent( g ) ){
+ Debug("efficient-e-match") << " Checking parent application " << g << std::endl;
+ //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
+ for( std::vector< triple<NodePpDispatcher*, Ips, Ips> > ::iterator cit = it2->second.begin();
+ cit != it2->second.end(); ++cit ){
+#ifdef CVC4_DEBUG
+ Debug("efficient-e-match") << " Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl;
+#endif
+ Debug("efficient-e-match") << " Check inverted path string ";
+ outputIps( "efficient-e-match", cit->second );
+ SetNode a_terms;
+ a_terms.insert( a );
+ collectTermsIps( cit->second, a_terms );
+ if( a_terms.empty() ) continue;
+ Debug("efficient-e-match") << " And check inverted path string ";
+ outputIps( "efficient-e-match", cit->third );
+ SetNode b_terms;
+ b_terms.insert( b );
+ collectTermsIps( cit->third, b_terms );
+ if( b_terms.empty() ) continue;
+ //Start debug
+ Debug("efficient-e-match") << " -> Possibly Added termsA (" << a_terms.size() << "): ";
+ for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end();
+ t!=end; ++t ){
+ Debug("efficient-e-match") << (*t) << " ";
+ }
+ Debug("efficient-e-match") << std::endl;
+ Debug("efficient-e-match") << " -> Possibly Added termsB (" << b_terms.size() << "): ";
+ for( SetNode::const_iterator t=b_terms.begin(), end=b_terms.end();
+ t!=end; ++t ){
+ Debug("efficient-e-match") << (*t) << " ";
+ }
+ Debug("efficient-e-match") << std::endl;
+ //End debug
+
+ cit->first->send(a_terms,b_terms);
+ }
+ }
+ }
+ }
+ }
+}
+
+
+void EfficientEMatcher::computeCandidatesConstants( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
+ Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl;
+ Debug("efficient-e-match") << " Eq class = [";
+ outputEqClass( "efficient-e-match", a);
+ Debug("efficient-e-match") << "]" << std::endl;
+ outputEqClassInfo("efficient-e-match",eci_a);
+ for( std::map< Node, std::map< Node, NodePcDispatcher* > >::iterator
+ it = d_cc_pairs.begin(), end = d_cc_pairs.end();
+ it != end; ++it ) {
+ Debug("efficient-e-match") << " Checking application " << it->first << std::endl;
+ if( !eci_b->hasFunction(it->first) ) continue;
+ for( std::map< Node, NodePcDispatcher* >::iterator
+ itc = it->second.begin(), end = it->second.end();
+ itc != end; ++itc ) {
+ //The constant
+ Debug("efficient-e-match") << " Checking constant " << a << std::endl;
+ if(d_quantEngine->getEqualityQuery()->getRepresentative(itc->first) != a) continue;
+ SetNode s;
+ eq::EqClassIterator eqc_iter( b, d_quantEngine->getEqualityQuery()->getEngine() );
+ while( !eqc_iter.isFinished() ){
+ Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+ << std::endl;
+ if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == it->first ) s.insert(*eqc_iter);
+ eqc_iter++;
+ }
+
+ if( s.empty() ) continue;
+ Debug("efficient-e-match") << " -> Added terms (" << s.size() << "): ";
+ for( SetNode::const_iterator t=s.begin(), end=s.end();
+ t!=end; ++t ){
+ Debug("efficient-e-match") << (*t) << " ";
+ }
+ Debug("efficient-e-match") << std::endl;
+ itc->second->send(s);
+ }
+ }
+}
+
+void EfficientEMatcher::collectTermsIps( Ips& ips, SetNode & terms ){
+ Assert( ips.size() > 0);
+ return collectTermsIps( ips, terms, ips.size() - 1);
+}
+
+void EfficientEMatcher::collectTermsIps( Ips& ips, SetNode& terms, int index ){
+ if( !terms.empty() ){
+ Debug("efficient-e-match-debug") << "> Process " << index << std::endl;
+ Node f = ips[index].first;
+ int arg = ips[index].second;
+
+ //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg"
+ bool addRep = ( index!=0 ); // We want to keep the top symbol for the last
+ SetNode newTerms;
+ for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+ t!=end; ++t ){
+ collectParentsTermsIps( *t, f, arg, newTerms, addRep );
+ }
+ terms.swap(newTerms);
+
+ Debug("efficient-e-match-debug") << "> Terms are now: ";
+ for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+ t!=end; ++t ){
+ Debug("efficient-e-match-debug") << *t << " ";
+ }
+ Debug("efficient-e-match-debug") << std::endl;
+
+ if(index!=0) collectTermsIps( ips, terms, index-1 );
+ }
+}
+
+bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
+ bool addedTerm = false;
+
+ if( modEq && d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n )){
+ Assert( d_quantEngine->getEqualityQuery()->getRepresentative( n )==n );
+ //collect modulo equality
+ //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it
+ eq::EqClassIterator eqc_iter( n, d_quantEngine->getEqualityQuery()->getEngine() );
+ while( !eqc_iter.isFinished() ){
+ Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+ << std::endl;
+ if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){
+ //if only one argument, we know we can stop (since all others added will be congruent)
+ if( f.getType().getNumChildren()==2 ){
+ return true;
+ }
+ addedTerm = true;
+ }
+ eqc_iter++;
+ }
+ }else{
+ quantifiers::TermDb* db = d_quantEngine->getTermDatabase();
+ //see if parent f exists from argument arg
+ const std::vector<Node> & parents = db->getParents(n,f,arg);
+ for( size_t i=0; i<parents.size(); ++i ){
+ TNode t = parents[i];
+ if(!CandidateGenerator::isLegalCandidate(t)) continue;
+ if( addRep ) t = d_quantEngine->getEqualityQuery()->getRepresentative( t );
+ terms.insert(t);
+ addedTerm = true;
+ }
+ }
+ return addedTerm;
+}
+
+void EfficientEMatcher::registerPatternElementPairs2( Node pat, Ips& ips, PpIpsMap & pp_ips_map, NodePcDispatcher* npc ){
+ Assert( pat.hasOperator() );
+ //add information for possible pp-pair
+ ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); //0 is just a dumb value
+
+ for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+ if( pat[i].getKind()==INST_CONSTANT ){
+ ips.back().second = i;
+ pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), Ips( ips ) ) );
+ }
+ }
+
+ for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+ if( pat[i].getKind()==APPLY_UF ){
+ ips.back().second = i;
+ registerPatternElementPairs2( pat[i], ips, pp_ips_map, npc );
+ Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl;
+ Debug("pattern-element-opt") << " Path = ";
+ outputIps( "pattern-element-opt", ips );
+ Debug("pattern-element-opt") << std::endl;
+ //pat.getOperator() and pat[i].getOperator() are a pc-pair
+ d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ]
+ .push_back( make_pair(npc,Ips(ips)) );
+ }
+ }
+ ips.pop_back();
+}
+
+void EfficientEMatcher::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
+ NodePcDispatcher* npc,
+ NodePpDispatcher* npp){
+ Ips ips;
+ registerPatternElementPairs2( pat, ips, pp_ips_map, npc );
+ for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+ // for each variable construct all the pp-pair
+ for( size_t j=0; j<it->second.size(); j++ ){
+ for( size_t k=j+1; k<it->second.size(); k++ ){
+ //found a pp-pair
+ Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl;
+ Debug("pattern-element-opt") << " Paths = ";
+ outputIps( "pattern-element-opt", it->second[j].second );
+ Debug("pattern-element-opt") << " and ";
+ outputIps( "pattern-element-opt", it->second[k].second );
+ Debug("pattern-element-opt") << std::endl;
+ d_pp_pairs[ it->second[j].first ][ it->second[k].first ]
+ .push_back( make_triple( npp, it->second[j].second, it->second[k].second ));
+ }
+ }
+ }
+};
+
+void findPpSite(Node pat, EfficientEMatcher::Ips& ips, EfficientEMatcher::PpIpsMap & pp_ips_map){
+ Assert( pat.getKind()==APPLY_UF );
+ //add information for possible pp-pair
+
+ ips.push_back( make_pair( pat.getOperator(), 0) );
+ for( size_t i=0; i<pat.getNumChildren(); i++ ){
+ if( pat[i].getKind()==INST_CONSTANT ){
+ ips.back().second = i;
+ pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), EfficientEMatcher::Ips( ips ) ) );
+ }
+ }
+
+ for( size_t i=0; i<pat.getNumChildren(); i++ ){
+ if( pat[i].getKind()==APPLY_UF ){
+ ips.back().second = i;
+ findPpSite( pat[i], ips, pp_ips_map );
+ }
+ }
+ ips.pop_back();
+}
+
+void EfficientEMatcher::combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
+ EfficientHandler& eh, size_t index2,const std::vector<Node> & pats){
+ hash_map<size_t,NodePpDispatcher*> npps;
+ for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+ MultiPpIpsMap::iterator mit = multi_pp_ips_map.find(it->first);
+ if(mit == multi_pp_ips_map.end()) continue;
+ // for each variable construct all the pp-pair
+ // j the last pattern treated
+ for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
+ j != jend; ++j){
+ // k one of the previous one
+ for( std::vector< triple< size_t, Node, Ips > >::iterator k=mit->second.begin(), kend = mit->second.end() ;
+ k != kend; ++k){
+ //found a pp-pair
+ Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j->first
+ << ", " << k->second << " in "<< k->first
+ << " )" << std::endl;
+ Debug("pattern-element-opt") << " Paths = ";
+ outputIps( "pattern-element-opt", j->second );
+ Debug("pattern-element-opt") << " and ";
+ outputIps( "pattern-element-opt", k->third );
+ Debug("pattern-element-opt") << std::endl;
+ NodePpDispatcher* dispatcher;
+ hash_map<size_t,NodePpDispatcher*>::iterator inpp = npps.find(k->first);
+ if( inpp != npps.end() ) dispatcher = inpp->second;
+ else{
+ dispatcher = new NodePpDispatcher();
+#ifdef CVC4_DEBUG
+ dispatcher->pat1 = pats[index2];
+ dispatcher->pat2 = pats[k->first];
+#endif
+ dispatcher->addPpDispatcher(&eh,index2,k->first);
+ };
+ d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third ));
+ }
+ }
+ }
+
+ /** Put pp_ips_map to multi_pp_ips_map */
+ for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+ for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
+ j != jend; ++j){
+ multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second));
+ }
+ }
+
+}
+
+
+void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler,
+ const std::vector< Node > & pats ){
+ Assert(pats.size() > 0);
+
+ MultiPpIpsMap multi_pp_ips_map;
+ PpIpsMap pp_ips_map;
+ //In a multi-pattern Pattern that is only a variable are specials,
+ //if the variable appears in another pattern, it can be discarded.
+ //Otherwise new term of this term can be candidate. So we stock them
+ //here before adding them.
+ std::vector< size_t > patVars;
+
+ Debug("pattern-element-opt") << "Register patterns" << pats << std::endl;
+ for(size_t i = 0; i < pats.size(); ++i){
+ if( pats[i].getKind() == kind::INST_CONSTANT){
+ patVars.push_back(i);
+ continue;
+ }
+ //to complete
+ if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
+ Node cst = NodeManager::currentNM()->mkConst<bool>(false);
+ TNode op = pats[i][0].getOperator();
+ if(d_cc_pairs[op][cst] == NULL){
+ d_cc_pairs[op][cst] = new NodePcDispatcher();
+ }
+ d_cc_pairs[op][cst]->addPcDispatcher(&handler,i);
+ continue;
+ }
+ //end to complete
+ Debug("pattern-element-opt") << " Register candidate generator..." << pats[i] << std::endl;
+ /* Has the pattern already been seen */
+ if( d_pat_cand_gens.find( pats[i] )==d_pat_cand_gens.end() ){
+ NodePcDispatcher* npc = new NodePcDispatcher();
+ NodePpDispatcher* npp = new NodePpDispatcher();
+#ifdef CVC4_DEBUG
+ npc->pat = pats[i];
+ npp->pat1 = pats[i];
+ npp->pat2 = pats[i];
+#endif
+ d_pat_cand_gens[pats[i]] = make_pair(npc,npp);
+ registerPatternElementPairs( pats[i], pp_ips_map, npc, npp );
+ }else{
+ Ips ips;
+ findPpSite(pats[i],ips,pp_ips_map);
+ }
+ //Has the top operator already been seen */
+ TNode op = pats[i].getOperator();
+ d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
+ d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
+ d_cand_gens[op].addNewTermDispatcher(&handler,i);
+
+ combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
+
+ pp_ips_map.clear();
+ }
+
+ for(size_t i = 0; i < patVars.size(); ++i){
+ TNode var = pats[patVars[i]];
+ Assert( var.getKind() == kind::INST_CONSTANT );
+ if( multi_pp_ips_map.find(var) != multi_pp_ips_map.end() ){
+ //The variable appear in another pattern, skip it
+ continue;
+ };
+ d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]);
+ }
+
+ //take all terms from the uf term db and add to candidate generator
+ if( pats[0].getKind() == kind::INST_CONSTANT ){
+ TypeNode ty = pats[0].getType();
+ rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine);
+ cg->reset(Node::null());
+ TNode c;
+ SetNode ele;
+ while( !(c = cg->getNextCandidate()).isNull() ){
+ if( c.getType() == ty ) ele.insert(c);
+ }
+ if( !ele.empty() ){
+ // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
+ // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
+ // }
+ if(Debug.isOn("efficient-e-match-stats")){
+ Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+ }
+ handler.addMonoCandidate(ele, 0);
+ }
+
+ } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){
+ Node cst = NodeManager::currentNM()->mkConst<bool>(false);
+ TNode op = pats[0][0].getOperator();
+ cst = d_quantEngine->getEqualityQuery()->getRepresentative(cst);
+ SetNode ele;
+ eq::EqClassIterator eqc_iter( cst, d_quantEngine->getEqualityQuery()->getEngine() );
+ while( !eqc_iter.isFinished() ){
+ Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+ << std::endl;
+ if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == op ) ele.insert(*eqc_iter);
+ eqc_iter++;
+ }
+ if( !ele.empty() ){
+ if(Debug.isOn("efficient-e-match-stats")){
+ Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+ }
+ handler.addMonoCandidate(ele, 0);
+ }
+
+ } else {
+ Node op = pats[0].getOperator();
+ TermDb* db = d_quantEngine->getTermDatabase();
+ if(db->d_op_map[op].begin() != db->d_op_map[op].end()){
+ SetNode ele;
+ // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
+ // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
+ // }
+ ele.insert(db->d_op_map[op].begin(), db->d_op_map[op].end());
+ if(Debug.isOn("efficient-e-match-stats")){
+ Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+ }
+ handler.addMonoCandidate(ele, 0);
+ }
+ }
+ Debug("efficient-e-match") << "Done." << std::endl;
+}
+
+void EfficientEMatcher::outputEqClass( const char* c, Node n ){
+ if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+ eq::EqClassIterator eqc_iter( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
+ d_quantEngine->getEqualityQuery()->getEngine() );
+ bool firstTime = true;
+ while( !eqc_iter.isFinished() ){
+ if( !firstTime ){ Debug(c) << ", "; }
+ Debug(c) << (*eqc_iter);
+ firstTime = false;
+ eqc_iter++;
+ }
+ }else{
+ Debug(c) << n;
+ }
+}
+
+void EfficientEMatcher::outputIps( const char* c, Ips& ips ){
+ for( int i=0; i<(int)ips.size(); i++ ){
+ if( i>0 ){ Debug( c ) << "."; }
+ Debug( c ) << ips[i].first << "." << ips[i].second;
+ }
+}
+
+
+} /* namespace theory */
+} /* namespace cvc4 */
diff --git a/src/theory/rewriterules/efficient_e_matching.h b/src/theory/rewriterules/efficient_e_matching.h new file mode 100755 index 000000000..ea06ad06e --- /dev/null +++ b/src/theory/rewriterules/efficient_e_matching.h @@ -0,0 +1,447 @@ +/********************* */
+/*! \file efficient_e_matching.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief efficient e-matching
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EFFICIENT_E_MATCHING_H
+#define __CVC4__EFFICIENT_E_MATCHING_H
+
+#include "expr/node.h"
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
+#include "util/statistics_registry.h"
+#include "util/ntuple.h"
+#include "context/cdqueue.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers{
+ class TermDb;
+}
+
+class EfficientEMatcher;
+class HandlerPcDispatcher;
+class HandlerPpDispatcher;
+
+typedef std::set<Node> SetNode;
+
+template<class T>
+class CleanUpPointer{
+public:
+ inline void operator()(T** e){
+ delete(*e);
+ };
+};
+
+class EfficientHandler{
+public:
+ typedef std::pair< Node, size_t > MonoCandidate;
+ typedef std::pair< MonoCandidate, MonoCandidate > MultiCandidate;
+ typedef std::pair< SetNode, size_t > MonoCandidates;
+ typedef std::pair< MonoCandidates, MonoCandidates > MultiCandidates;
+private:
+ /* Queue of candidates */
+ typedef context::CDQueue< MonoCandidates *, CleanUpPointer<MonoCandidates> > MonoCandidatesQueue;
+ typedef context::CDQueue< MultiCandidates *, CleanUpPointer<MultiCandidates> > MultiCandidatesQueue;
+ MonoCandidatesQueue d_monoCandidates;
+ typedef SetNode::iterator SetNodeIter;
+ context::CDO<SetNodeIter> d_si;
+ context::CDO<bool> d_mono_not_first;
+
+ MonoCandidatesQueue d_monoCandidatesNewTerm;
+ context::CDO<SetNodeIter> d_si_new_term;
+ context::CDO<bool> d_mono_not_first_new_term;
+
+
+ MultiCandidatesQueue d_multiCandidates;
+ context::CDO<SetNodeIter> d_si1;
+ context::CDO<SetNodeIter> d_si2;
+ context::CDO<bool> d_multi_not_first;
+
+
+ friend class EfficientEMatcher;
+ friend class HandlerPcDispatcher;
+ friend class HandlerPpDispatcher;
+ friend class HandlerNewTermDispatcher;
+protected:
+ void addMonoCandidate(SetNode & s, size_t index){
+ Assert(!s.empty());
+ d_monoCandidates.push(new MonoCandidates(s,index));
+ }
+ void addMonoCandidateNewTerm(SetNode & s, size_t index){
+ Assert(!s.empty());
+ d_monoCandidatesNewTerm.push(new MonoCandidates(s,index));
+ }
+ void addMultiCandidate(SetNode & s1, size_t index1, SetNode & s2, size_t index2){
+ Assert(!s1.empty() && !s2.empty());
+ d_multiCandidates.push(new MultiCandidates(MonoCandidates(s1,index1),
+ MonoCandidates(s2,index2)));
+ }
+public:
+ EfficientHandler(context::Context * c):
+ //false for d_mono_not_first beacause its the default constructor
+ d_monoCandidates(c), d_si(c), d_mono_not_first(c,false),
+ d_monoCandidatesNewTerm(c), d_si_new_term(c),
+ d_mono_not_first_new_term(c,false),
+ d_multiCandidates(c) , d_si1(c), d_si2(c), d_multi_not_first(c,false) {};
+
+ bool getNextMonoCandidate(MonoCandidate & candidate){
+ if(d_monoCandidates.empty()) return false;
+ const MonoCandidates * front = d_monoCandidates.front();
+ SetNodeIter si_tmp;
+ if(!d_mono_not_first){
+ Assert(front->first.begin() != front->first.end());
+ d_mono_not_first = true;
+ si_tmp=front->first.begin();
+ }else{
+ si_tmp = d_si;
+ ++si_tmp;
+ };
+ if(si_tmp != front->first.end()){
+ candidate.first = (*si_tmp);
+ candidate.second = front->second;
+ d_si = si_tmp;
+ Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
+ return true;
+ };
+ d_monoCandidates.pop();
+ d_mono_not_first = false;
+ return getNextMonoCandidate(candidate);
+ };
+
+ bool getNextMonoCandidateNewTerm(MonoCandidate & candidate){
+ if(d_monoCandidatesNewTerm.empty()) return false;
+ const MonoCandidates * front = d_monoCandidatesNewTerm.front();
+ SetNodeIter si_tmp;
+ if(!d_mono_not_first_new_term){
+ Assert(front->first.begin() != front->first.end());
+ d_mono_not_first_new_term = true;
+ si_tmp=front->first.begin();
+ }else{
+ si_tmp = d_si_new_term;
+ ++si_tmp;
+ };
+ if(si_tmp != front->first.end()){
+ candidate.first = (*si_tmp);
+ candidate.second = front->second;
+ d_si_new_term = si_tmp;
+ Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
+ return true;
+ };
+ d_monoCandidatesNewTerm.pop();
+ d_mono_not_first_new_term = false;
+ return getNextMonoCandidateNewTerm(candidate);
+ };
+
+ bool getNextMultiCandidate(MultiCandidate & candidate){
+ if(d_multiCandidates.empty()) return false;
+ const MultiCandidates* front = d_multiCandidates.front();
+ SetNodeIter si1_tmp;
+ SetNodeIter si2_tmp;
+ if(!d_multi_not_first){
+ Assert(front->first.first.begin() != front->first.first.end());
+ Assert(front->second.first.begin() != front->second.first.end());
+ si1_tmp = front->first.first.begin();
+ si2_tmp = front->second.first.begin();
+ }else{
+ si1_tmp = d_si1;
+ si2_tmp = d_si2;
+ ++si2_tmp;
+ };
+ if(si2_tmp != front->second.first.end()){
+ candidate.first.first = *si1_tmp;
+ candidate.first.second = front->first.second;
+ candidate.second.first = *si2_tmp;
+ candidate.second.second = front->second.second;
+ if(!d_multi_not_first){d_si1 = si1_tmp; d_multi_not_first = true; };
+ d_si2 = si2_tmp;
+ Debug("efficienthandler") << "Multi1 produces "
+ << candidate.first.first << " for "
+ << candidate.first.second << " and "
+ << candidate.second.first << " for "
+ << candidate.second.second << " and "
+ << std::endl;
+ return true;
+ }; // end of the second set
+ si2_tmp = front->second.first.begin();
+ ++si1_tmp;
+ if(si1_tmp != front->first.first.end()){
+ candidate.first.first = *si1_tmp;
+ candidate.first.second = front->first.second;
+ candidate.second.first = *si2_tmp;
+ candidate.second.second = front->second.second;
+ d_si1 = si1_tmp;
+ d_si2 = si2_tmp;
+ Debug("efficienthandler") << "Multi2 produces "
+ << candidate.first.first << " for "
+ << candidate.first.second << " and "
+ << candidate.second.first << " for "
+ << candidate.second.second << " and "
+ << std::endl;
+ return true;
+ }; // end of the first set
+ d_multiCandidates.pop();
+ d_multi_not_first = false;
+ return getNextMultiCandidate(candidate);
+ }
+};
+
+class PcDispatcher{
+public:
+ virtual ~PcDispatcher(){};
+ /* Send the node to the dispatcher */
+ virtual void send(SetNode & s) = 0;
+};
+
+
+class HandlerPcDispatcher: public PcDispatcher{
+ EfficientHandler* d_handler;
+ size_t d_index;
+public:
+ HandlerPcDispatcher(EfficientHandler* handler, size_t index):
+ d_handler(handler), d_index(index) {};
+ void send(SetNode & s){
+ d_handler->addMonoCandidate(s,d_index);
+ }
+};
+
+
+/** All the dispatcher that correspond to this node */
+class NodePcDispatcher: public PcDispatcher{
+#ifdef CVC4_DEBUG
+public:
+ Node pat;
+#endif/* CVC4_DEBUG*/
+private:
+ std::vector<HandlerPcDispatcher> d_dis;
+public:
+ void send(SetNode & s){
+ Assert(!s.empty());
+ for(std::vector<HandlerPcDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+ i != end; ++i){
+ (*i).send(s);
+ }
+ }
+ void addPcDispatcher(EfficientHandler* handler, size_t index){
+ d_dis.push_back(HandlerPcDispatcher(handler,index));
+ }
+};
+
+
+class HandlerNewTermDispatcher: public PcDispatcher{
+ EfficientHandler* d_handler;
+ size_t d_index;
+public:
+ HandlerNewTermDispatcher(EfficientHandler* handler, size_t index):
+ d_handler(handler), d_index(index) {};
+ void send(SetNode & s){
+ d_handler->addMonoCandidateNewTerm(s,d_index);
+ }
+};
+
+/** All the dispatcher that correspond to this node */
+class NodeNewTermDispatcher: public PcDispatcher{
+#ifdef CVC4_DEBUG
+public:
+ Node pat;
+#endif/* CVC4_DEBUG*/
+private:
+ std::vector<HandlerNewTermDispatcher> d_dis;
+public:
+ void send(SetNode & s){
+ Assert(!s.empty());
+ for(std::vector<HandlerNewTermDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+ i != end; ++i){
+ (*i).send(s);
+ }
+ }
+ void addNewTermDispatcher(EfficientHandler* handler, size_t index){
+ d_dis.push_back(HandlerNewTermDispatcher(handler,index));
+ }
+};
+
+class PpDispatcher{
+public:
+ virtual ~PpDispatcher(){};
+ /* Send the node to the dispatcher */
+ virtual void send(SetNode & s1, SetNode & s2, SetNode & sinter) = 0;
+};
+
+
+class HandlerPpDispatcher: public PpDispatcher{
+ EfficientHandler* d_handler;
+ size_t d_index1;
+ size_t d_index2;
+public:
+ HandlerPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2):
+ d_handler(handler), d_index1(index1), d_index2(index2) {};
+ void send(SetNode & s1, SetNode & s2, SetNode & sinter){
+ if(d_index1 == d_index2){
+ if(!sinter.empty())
+ d_handler->addMonoCandidate(sinter,d_index1);
+ }else{
+ d_handler->addMultiCandidate(s1,d_index1,s2,d_index2);
+ }
+ }
+};
+
+
+/** All the dispatcher that correspond to this node */
+class NodePpDispatcher: public PpDispatcher{
+#ifdef CVC4_DEBUG
+public:
+ Node pat1;
+ Node pat2;
+#endif/* CVC4_DEBUG */
+private:
+ std::vector<HandlerPpDispatcher> d_dis;
+ void send(SetNode & s1, SetNode & s2, SetNode & inter){
+ for(std::vector<HandlerPpDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+ i != end; ++i){
+ (*i).send(s1,s2,inter);
+ }
+ }
+public:
+ void send(SetNode & s1, SetNode & s2){
+ // can be done in HandlerPpDispatcher lazily
+ Assert(!s1.empty() && !s2.empty());
+ SetNode inter;
+ std::set_intersection( s1.begin(), s1.end(), s2.begin(), s2.end(),
+ std::inserter( inter, inter.begin() ) );
+ send(s1,s2,inter);
+ }
+ void addPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2){
+ d_dis.push_back(HandlerPpDispatcher(handler,index1,index2));
+ }
+};
+
+//equivalence class info
+class EqClassInfo
+{
+public:
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+ typedef context::CDChunkList<Node> NodeList;
+public:
+ //a list of operators that occur as top symbols in this equivalence class
+ // Efficient E-Matching for SMT Solvers: "funs"
+ BoolMap d_funs;
+ //a list of operators f for which a term of the form f( ... t ... ) exists
+ // Efficient E-Matching for SMT Solvers: "pfuns"
+ BoolMap d_pfuns;
+ //a list of equivalence classes that are disequal
+ BoolMap d_disequal;
+public:
+ EqClassInfo( context::Context* c );
+ ~EqClassInfo(){}
+ //set member
+ void setMember( Node n, quantifiers::TermDb* db );
+ //has function "funs"
+ bool hasFunction( Node op );
+ //has parent "pfuns"
+ bool hasParent( Node op );
+ //merge with another eq class info
+ void merge( EqClassInfo* eci );
+};
+
+class EfficientEMatcher{
+protected:
+ /** reference to the quantifiers engine */
+ QuantifiersEngine* d_quantEngine;
+public:
+ EfficientEMatcher(CVC4::theory::QuantifiersEngine* qe);
+ ~EfficientEMatcher() {
+ for(std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> >::iterator
+ i = d_pat_cand_gens.begin(), end = d_pat_cand_gens.end();
+ i != end; i++){
+ delete(i->second.first);
+ delete(i->second.second);
+ }
+ }
+private:
+ //information for each equivalence class
+ std::map< Node, EqClassInfo* > d_eqc_ops;
+public:
+ /** new node */
+ void newEqClass( TNode n );
+ /** merge */
+ void merge( TNode a, TNode b );
+ /** assert terms are disequal */
+ void assertDisequal( TNode a, TNode b, TNode reason );
+ /** get equivalence class info */
+ EqClassInfo* getEquivalenceClassInfo( Node n );
+ EqClassInfo* getOrCreateEquivalenceClassInfo( Node n );
+ typedef std::vector< std::pair< Node, int > > Ips;
+ typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap;
+ typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap;
+
+private:
+ /** Parent/Child Pairs (for efficient E-matching)
+ So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }.
+ */
+ std::map< Node, std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > > > d_pc_pairs;
+ /** Parent/Parent Pairs (for efficient E-matching) */
+ std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > > d_pp_pairs;
+ /** Constants/Child Pairs
+ So, for example, if we have the pattern f( x ) = c, then d_pc_pairs[f][c] = ..., pcdispatcher, ...
+ */
+ //TODO constant in pattern can use the same thing just add an Ips
+ std::map< Node, std::map< Node, NodePcDispatcher* > > d_cc_pairs;
+ /** list of all candidate generators for each operator */
+ std::map< Node, NodeNewTermDispatcher > d_cand_gens;
+ /** list of all candidate generators for each type */
+ std::map< TypeNode, NodeNewTermDispatcher > d_cand_gen_types;
+ /** map from patterns to candidate generators */
+ std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> > d_pat_cand_gens;
+ /** helper functions */
+ void registerPatternElementPairs2( Node pat, Ips& ips,
+ PpIpsMap & pp_ips_map, NodePcDispatcher* npc);
+ void registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
+ NodePcDispatcher* npc, NodePpDispatcher* npp);
+ /** find the pp-pair between pattern inside multi-pattern*/
+ void combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
+ EfficientHandler& eh, size_t index2,
+ const std::vector<Node> & pats); //pats for debug
+ /** compute candidates for pc pairs */
+ void computeCandidatesPcPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
+ /** compute candidates for pp pairs */
+ void computeCandidatesPpPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
+ /** compute candidates for cc pairs */
+ void computeCandidatesConstants( Node a, EqClassInfo*, Node b, EqClassInfo* );
+ /** collect terms based on inverted path string */
+ void collectTermsIps( Ips& ips, SetNode& terms, int index);
+ bool collectParentsTermsIps( Node n, Node f, int arg, SetNode& terms, bool addRep, bool modEq = true );
+public:
+ void collectTermsIps( Ips& ips, SetNode& terms);
+public:
+ void registerEfficientHandler( EfficientHandler& eh, const std::vector<Node> & pat );
+public:
+ void newTerms(SetNode& s);
+public:
+ /** output eq class */
+ void outputEqClass( const char* c, Node n );
+ /** output inverted path string */
+ void outputIps( const char* c, Ips& ips );
+};/* class EfficientEMatcher */
+
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EFFICIENT_E_MATCHING_H */
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index af4cdeb50..5f10e1daa 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -24,6 +24,7 @@ #include "theory/rewriterules/rr_inst_match_impl.h" #include "theory/rewriterules/rr_candidate_generator.h" #include "theory/quantifiers/candidate_generator.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace CVC4; using namespace CVC4::kind; @@ -1225,8 +1226,8 @@ private: std::vector< PatMatcher* > d_patterns; std::vector< Matcher* > d_direct_patterns; InstMatch d_im; - uf::EfficientHandler d_eh; - uf::EfficientHandler::MultiCandidate d_mc; + EfficientHandler d_eh; + EfficientHandler::MultiCandidate d_mc; InstMatchTrie2Pairs<true> d_cache; std::vector<Node> d_pats; // bool indexDone( size_t i){ @@ -1403,9 +1404,8 @@ public: d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe)); } }; - Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ); - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); - ith->registerEfficientHandler(d_eh, pats); + EfficientEMatcher* eem = qe->getEfficientEMatcher(); + eem->registerEfficientHandler(d_eh, pats); }; void resetInstantiationRound( QuantifiersEngine* qe ){ Assert(d_step == ES_START || d_step == ES_STOP); |