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