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/uf | |
parent | 304404e3709ff7e95156c87f65a3e2647d9f3441 (diff) |
efficient e-matching now specific to rewrite rules
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 621 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 390 |
2 files changed, 6 insertions, 1005 deletions
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index eceb4715b..0cc32d420 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -15,12 +15,12 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -#include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" #include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -34,61 +34,6 @@ namespace CVC4 { namespace theory { namespace uf { -inline std::ostream& operator<<(std::ostream& out, const InstantiatorTheoryUf::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; -} - - - InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) : Instantiator( c, qe, th ) { @@ -269,94 +214,9 @@ void InstantiatorTheoryUf::newEqClass( TNode n ){ d_quantEngine->addTermToDatabase( n ); } -void InstantiatorTheoryUf::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 InstantiatorTheoryUf::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 ); - } + d_quantEngine->getEfficientEMatcher()->merge( a, b ); } /** assert terms are disequal */ @@ -364,468 +224,6 @@ void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){ } -EqClassInfo* InstantiatorTheoryUf::getEquivalenceClassInfo( Node n ) { - return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n]; -} -EqClassInfo* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n ){ - Assert( n==getRepresentative( n ) ); - if( d_eqc_ops.find( n )==d_eqc_ops.end() ){ - EqClassInfo* eci = new EqClassInfo( d_th->getSatContext() ); - eci->setMember( n, d_quantEngine->getTermDatabase() ); - d_eqc_ops[n] = eci; - } - return d_eqc_ops[n]; -} - -void InstantiatorTheoryUf::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( 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 InstantiatorTheoryUf::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 InstantiatorTheoryUf::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(getRepresentative(itc->first) != a) continue; - SetNode s; - eq::EqClassIterator eqc_iter( b, &((TheoryUF*)d_th)->d_equalityEngine ); - 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 InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode & terms ){ - Assert( ips.size() > 0); - return collectTermsIps( ips, terms, ips.size() - 1); -} - -void InstantiatorTheoryUf::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 InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true - bool addedTerm = false; - - if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){ - Assert( 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, &((TheoryUF*)d_th)->d_equalityEngine ); - 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 = getRepresentative( t ); - terms.insert(t); - addedTerm = true; - } - } - return addedTerm; -} - -void InstantiatorTheoryUf::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 InstantiatorTheoryUf::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, InstantiatorTheoryUf::Ips& ips, InstantiatorTheoryUf::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(), InstantiatorTheoryUf::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 InstantiatorTheoryUf::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 InstantiatorTheoryUf::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 = getRepresentative(cst); - SetNode ele; - eq::EqClassIterator eqc_iter( cst, &((TheoryUF*)d_th)->d_equalityEngine ); - 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 InstantiatorTheoryUf::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); @@ -848,24 +246,15 @@ void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ } } -void InstantiatorTheoryUf::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; - } -} - rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){ uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); } rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){ uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); } diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 501ef9a6d..324fa6386 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -39,330 +39,6 @@ namespace quantifiers{ namespace uf { -class InstantiatorTheoryUf; -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 uf::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 InstantiatorTheoryUf; - 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 InstantiatorTheoryUf : public Instantiator{ friend class ::CVC4::theory::inst::InstMatchGenerator; friend class ::CVC4::theory::quantifiers::TermDb; @@ -378,14 +54,7 @@ protected: InstStrategyUserPatterns* d_isup; public: InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th); - ~InstantiatorTheoryUf() { - 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); - } - } + ~InstantiatorTheoryUf() {} /** assertNode method */ void assertNode( Node assertion ); /** Pre-register a term. Done one time for a Node, ever. */ @@ -420,9 +89,6 @@ public: public: /** the base match */ std::map< Node, InstMatch > d_baseMatch; -private: - //for each equivalence class - std::map< Node, EqClassInfo* > d_eqc_ops; public: /** general queries about equality */ bool hasTerm( Node a ); @@ -441,69 +107,15 @@ public: 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); - /** Register candidate generator cg for pattern pat. (for use with efficient e-matching) - This request will ensure that calls will be made to cg->addCandidate( n ) for all - ground terms n that are relevant for matching with pat. - */ private: /** triggers */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; public: /** register trigger (for eager quantifier instantiation) */ void registerTrigger( inst::Trigger* tr, Node op ); - 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 InstantiatorTheoryUf */ /** equality query object using instantiator theory uf */ |