From: Andrew Reynolds Date: Wed, 24 Oct 2012 01:06:15 +0000 (+0000) Subject: efficient e-matching now specific to rewrite rules X-Git-Tag: cvc5-1.0.0~7680 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ebe47d38892131b96521a729c915365a3369110;p=cvc5.git efficient e-matching now specific to rewrite rules --- diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 43548f021..493b9e931 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -18,6 +18,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -82,11 +83,11 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); if( options::efficientEMatching() ){ - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); + EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher(); if( d_parents[n[i]][op].empty() ){ //must add parent to equivalence class info - Node nir = ith->getRepresentative( n[i] ); - uf::EqClassInfo* eci_nir = ith->getEquivalenceClassInfo( nir ); + Node nir = d_quantEngine->getEqualityQuery()->getRepresentative( n[i] ); + EqClassInfo* eci_nir = eem->getEquivalenceClassInfo( nir ); if( eci_nir ){ eci_nir->d_pfuns[ op ] = true; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a44a3ff1f..486e6721b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -39,6 +40,7 @@ d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_tr_trie = new inst::TriggerTrie; + d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; //the model object @@ -194,8 +196,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); if( options::efficientEMatching() ){ - uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF ); - d_ith->newTerms(added); + d_eem->newTerms( added ); } //added contains also the Node that just have been asserted in this branch for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 18635a823..f9c016cb9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -66,6 +66,8 @@ namespace inst { class TriggerTrie; }/* CVC4::theory::inst */ +class EfficientEMatcher; + class QuantifiersEngine { friend class quantifiers::InstantiationEngine; friend class quantifiers::ModelEngine; @@ -86,6 +88,8 @@ private: QuantRelevance d_quant_rel; /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; + /** efficient e-matcher */ + EfficientEMatcher* d_eem; private: /** list of all quantifiers seen */ std::vector< Node > d_quants; @@ -131,6 +135,8 @@ public: QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); + /** get efficient e-matching utility */ + EfficientEMatcher* getEfficientEMatcher() { return d_eem; } public: /** check at level */ void check( Theory::Effort e ); 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::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::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 > >::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 > ::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 & parents = db->getParents(n,f,arg); + for( size_t i=0; igetEqualityQuery()->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; jsecond.size(); j++ ){ + for( size_t k=j+1; ksecond.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 & pats){ + hash_map 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::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(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::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(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::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 SetNode; + +template +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 > MonoCandidatesQueue; + typedef context::CDQueue< MultiCandidates *, CleanUpPointer > MultiCandidatesQueue; + MonoCandidatesQueue d_monoCandidates; + typedef SetNode::iterator SetNodeIter; + context::CDO d_si; + context::CDO d_mono_not_first; + + MonoCandidatesQueue d_monoCandidatesNewTerm; + context::CDO d_si_new_term; + context::CDO d_mono_not_first_new_term; + + + MultiCandidatesQueue d_multiCandidates; + context::CDO d_si1; + context::CDO d_si2; + context::CDO 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 d_dis; +public: + void send(SetNode & s){ + Assert(!s.empty()); + for(std::vector::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 d_dis; +public: + void send(SetNode & s){ + Assert(!s.empty()); + for(std::vector::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 d_dis; + void send(SetNode & s1, SetNode & s2, SetNode & inter){ + for(std::vector::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 BoolMap; + typedef context::CDChunkList 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 >::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 > 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 & 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 & 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 d_cache; std::vector 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); 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::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::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 > >::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 > ::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 & parents = db->getParents(n,f,arg); - for( size_t i=0; i( 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; jsecond.size(); j++ ){ - for( size_t k=j+1; ksecond.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 & pats){ - hash_map 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::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(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::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(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::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(getTheory()); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); } rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){ uf::TheoryUF* uf = static_cast(getTheory()); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast(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 SetNode; - -template -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 > MonoCandidatesQueue; - typedef context::CDQueue< MultiCandidates *, CleanUpPointer > MultiCandidatesQueue; - MonoCandidatesQueue d_monoCandidates; - typedef uf::SetNode::iterator SetNodeIter; - context::CDO d_si; - context::CDO d_mono_not_first; - - MonoCandidatesQueue d_monoCandidatesNewTerm; - context::CDO d_si_new_term; - context::CDO d_mono_not_first_new_term; - - - MultiCandidatesQueue d_multiCandidates; - context::CDO d_si1; - context::CDO d_si2; - context::CDO 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 d_dis; -public: - void send(SetNode & s){ - Assert(!s.empty()); - for(std::vector::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 d_dis; -public: - void send(SetNode & s){ - Assert(!s.empty()); - for(std::vector::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 d_dis; - void send(SetNode & s1, SetNode & s2, SetNode & inter){ - for(std::vector::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 BoolMap; - typedef context::CDChunkList 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 >::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 > 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 & 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 & 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 */