From aef9f4e13ddcf2fa48226d98a2a14f9141a761f7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 11 Mar 2014 18:47:18 -0400 Subject: [PATCH] Fix for rewriterules build breakage. --- src/Makefile.am | 5 +- src/options/Makefile.am | 4 - src/prop/options | 2 +- src/theory/logic_info.h | 5 +- src/theory/quantifiers/term_database.cpp | 1 - .../rewriterules/efficient_e_matching.cpp | 680 ------- .../rewriterules/efficient_e_matching.h | 450 ----- src/theory/rewriterules/kinds | 17 - src/theory/rewriterules/options | 14 - .../rewriterules/rr_candidate_generator.cpp | 67 - .../rewriterules/rr_candidate_generator.h | 199 -- src/theory/rewriterules/rr_inst_match.cpp | 1596 ----------------- src/theory/rewriterules/rr_inst_match.h | 341 ---- src/theory/rewriterules/rr_inst_match_impl.h | 126 -- src/theory/rewriterules/rr_trigger.cpp | 385 ---- src/theory/rewriterules/rr_trigger.h | 157 -- .../rewriterules/theory_rewriterules.cpp | 78 - src/theory/rewriterules/theory_rewriterules.h | 62 - .../rewriterules/theory_rewriterules_params.h | 86 - .../theory_rewriterules_preprocess.h | 176 -- .../theory_rewriterules_rewriter.h | 115 -- .../theory_rewriterules_rules.cpp | 403 ----- .../rewriterules/theory_rewriterules_rules.h | 37 - .../theory_rewriterules_type_rules.h | 35 - src/theory/theory_engine.cpp | 30 +- 25 files changed, 17 insertions(+), 5054 deletions(-) delete mode 100644 src/theory/rewriterules/efficient_e_matching.cpp delete mode 100644 src/theory/rewriterules/efficient_e_matching.h delete mode 100644 src/theory/rewriterules/kinds delete mode 100644 src/theory/rewriterules/options delete mode 100644 src/theory/rewriterules/rr_candidate_generator.cpp delete mode 100644 src/theory/rewriterules/rr_candidate_generator.h delete mode 100644 src/theory/rewriterules/rr_inst_match.cpp delete mode 100644 src/theory/rewriterules/rr_inst_match.h delete mode 100644 src/theory/rewriterules/rr_inst_match_impl.h delete mode 100644 src/theory/rewriterules/rr_trigger.cpp delete mode 100644 src/theory/rewriterules/rr_trigger.h delete mode 100644 src/theory/rewriterules/theory_rewriterules.cpp delete mode 100644 src/theory/rewriterules/theory_rewriterules.h delete mode 100644 src/theory/rewriterules/theory_rewriterules_params.h delete mode 100644 src/theory/rewriterules/theory_rewriterules_preprocess.h delete mode 100644 src/theory/rewriterules/theory_rewriterules_rewriter.h delete mode 100644 src/theory/rewriterules/theory_rewriterules_rules.cpp delete mode 100644 src/theory/rewriterules/theory_rewriterules_rules.h delete mode 100644 src/theory/rewriterules/theory_rewriterules_type_rules.h diff --git a/src/Makefile.am b/src/Makefile.am index 450bf063e..03092979a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -20,7 +20,7 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main -THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers rewriterules idl +THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl lib_LTLIBRARIES = libcvc4.la @@ -307,8 +307,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/options_handlers.h \ - theory/rewriterules/theory_rewriterules.h \ - theory/rewriterules/theory_rewriterules.cpp \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ theory/arith/arithvar.h \ @@ -457,7 +455,6 @@ EXTRA_DIST = \ theory/strings/kinds \ theory/arrays/kinds \ theory/quantifiers/kinds \ - theory/rewriterules/kinds \ theory/arith/kinds \ theory/booleans/kinds \ theory/example/ecdata.h \ diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 8780922c9..18b2c42f4 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -21,8 +21,6 @@ OPTIONS_FILES_SRCS = \ ../theory/arrays/options.h \ ../theory/quantifiers/options.cpp \ ../theory/quantifiers/options.h \ - ../theory/rewriterules/options.cpp \ - ../theory/rewriterules/options.h \ ../theory/strings/options.cpp \ ../theory/strings/options.h \ ../prop/options.cpp \ @@ -84,8 +82,6 @@ nodist_liboptions_la_SOURCES = \ ../theory/arrays/options.h \ ../theory/quantifiers/options.cpp \ ../theory/quantifiers/options.h \ - ../theory/rewriterules/options.cpp \ - ../theory/rewriterules/options.h \ ../theory/strings/options.cpp \ ../theory/strings/options.h \ ../prop/options.cpp \ diff --git a/src/prop/options b/src/prop/options index cf241479c..8bb9d9135 100644 --- a/src/prop/options +++ b/src/prop/options @@ -10,7 +10,7 @@ option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-in option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0) sets the frequency of random decisions in the sat solver (P=0.0 by default) -option satRandomSeed random-seed --random-seed=S uint32_t :default +option satRandomSeed random-seed --random-seed=S uint32_t :default :read-write sets the random seed for the sat solver option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0) diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 2448898c0..a0777ae70 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -64,7 +64,6 @@ class CVC4_PUBLIC LogicInfo { case theory::THEORY_BUILTIN: case theory::THEORY_BOOL: case theory::THEORY_QUANTIFIERS: - case theory::THEORY_REWRITERULES: return false; default: return true; @@ -117,7 +116,7 @@ public: /** Is this a quantified logic? */ bool isQuantified() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); + return isTheoryEnabled(theory::THEORY_QUANTIFIERS); } /** Is this the all-inclusive logic? */ @@ -214,7 +213,6 @@ public: */ void enableQuantifiers() { enableTheory(theory::THEORY_QUANTIFIERS); - enableTheory(theory::THEORY_REWRITERULES); } /** @@ -222,7 +220,6 @@ public: */ void disableQuantifiers() { disableTheory(theory::THEORY_QUANTIFIERS); - disableTheory(theory::THEORY_REWRITERULES); } // these are for arithmetic diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a9e77d3d2..08a9f5d9f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -18,7 +18,6 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" -#include "theory/rewriterules/efficient_e_matching.h" #include "theory/quantifiers/theory_quantifiers.h" using namespace std; diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp deleted file mode 100644 index 05934fc8b..000000000 --- a/src/theory/rewriterules/efficient_e_matching.cpp +++ /dev/null @@ -1,680 +0,0 @@ -/********************* */ -/*! \file efficient_e_matching.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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" - -#include "theory/theory_engine.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 ) -{ - -} - -eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){ - //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine(); - return d_quantEngine->getMasterEqualityEngine(); -} - -/** 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==getEqualityEngine()->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(getEqualityEngine()->getRepresentative(itc->first) != a) continue; - SetNode s; - eq::EqClassIterator eqc_iter( b, getEqualityEngine() ); - 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 && getEqualityEngine()->hasTerm( n )){ - Assert( getEqualityEngine()->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, getEqualityEngine() ); - 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; igetRepresentative( 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() ){ - 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 = getEqualityEngine()->getRepresentative(cst); - SetNode ele; - eq::EqClassIterator eqc_iter( cst, getEqualityEngine() ); - 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 { - TermDb* db = d_quantEngine->getTermDatabase(); - Node op = db->getOperator( pats[0] ); - if(db->d_op_map[op].begin() != db->d_op_map[op].end()){ - SetNode ele; - 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( getEqualityEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc_iter( getEqualityEngine()->getRepresentative( n ), - getEqualityEngine() ); - 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 deleted file mode 100644 index b02d465fc..000000000 --- a/src/theory/rewriterules/efficient_e_matching.h +++ /dev/null @@ -1,450 +0,0 @@ -/********************* */ -/*! \file efficient_e_matching.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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" - -#include "theory/uf/equality_engine.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); - } - } - /** get equality engine we are using */ - eq::EqualityEngine* getEqualityEngine(); -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/kinds b/src/theory/rewriterules/kinds deleted file mode 100644 index 4ea0ecd43..000000000 --- a/src/theory/rewriterules/kinds +++ /dev/null @@ -1,17 +0,0 @@ -# kinds -*- sh -*- -# -# For documentation on this file format, please refer to -# src/theory/builtin/kinds. -# - -theory THEORY_REWRITERULES ::CVC4::theory::rewriterules::TheoryRewriteRules "theory/rewriterules/theory_rewriterules.h" -typechecker "theory/rewriterules/theory_rewriterules_type_rules.h" -rewriter ::CVC4::theory::rewriterules::TheoryRewriterulesRewriter "theory/rewriterules/theory_rewriterules_rewriter.h" - -properties check - -# Theory content goes here. - -# constants... - -endtheory diff --git a/src/theory/rewriterules/options b/src/theory/rewriterules/options deleted file mode 100644 index 285e489be..000000000 --- a/src/theory/rewriterules/options +++ /dev/null @@ -1,14 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module REWRITE_RULES "theory/rewriterules/options.h" Rewrite Rules - -option efficientEMatching --efficient-e-matching bool :default false - use efficient E-matching (only for rewrite rules) - -option rewriteRulesAsAxioms --rewrite-rules-as-axioms bool :default false - whether to convert rewrite rules to usual axioms (for debugging only) - -endmodule diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp deleted file mode 100644 index 3ebb3547c..000000000 --- a/src/theory/rewriterules/rr_candidate_generator.cpp +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file rr_candidate_generator.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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 rr candidate generator class - **/ - -#include "theory/rewriterules/rr_candidate_generator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.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::rrinst; - -GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){ - d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine()); -} - -GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){ - delete d_master_can_gen; -} - -void GenericCandidateGeneratorClasses::resetInstantiationRound(){ - d_master_can_gen->resetInstantiationRound(); -} - -void GenericCandidateGeneratorClasses::reset(TNode eqc){ - d_master_can_gen->reset(eqc); -} - -TNode GenericCandidateGeneratorClasses::getNextCandidate(){ - return d_master_can_gen->getNextCandidate(); -} - - -GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { - d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine()); -} - -GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){ - delete d_master_can_gen; -} - -void GenericCandidateGeneratorClass::resetInstantiationRound(){ - d_master_can_gen->resetInstantiationRound(); -} - -void GenericCandidateGeneratorClass::reset(TNode eqc){ - d_master_can_gen->reset(eqc); -} - -TNode GenericCandidateGeneratorClass::getNextCandidate(){ - return d_master_can_gen->getNextCandidate(); -} - diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h deleted file mode 100644 index d00c8ab83..000000000 --- a/src/theory/rewriterules/rr_candidate_generator.h +++ /dev/null @@ -1,199 +0,0 @@ -/********************* */ -/*! \file rr_candidate_generator.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds, Francois Bobot - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief rr candidate generator - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H -#define __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/term_database.h" -#include "theory/rewriterules/rr_inst_match.h" - -using namespace CVC4::theory::quantifiers; - -namespace CVC4 { -namespace theory { -namespace eq { - -namespace rrinst{ -typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; - -//New CandidateGenerator. They have a simpler semantic than the old one - -// Just iterate among the equivalence classes -// node::Null() must be given to reset -class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{ -private: - //the equality classes iterator - eq::EqClassesIterator d_eq; - //equalityengine pointer - EqualityEngine* d_ee; -public: - CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){} - ~CandidateGeneratorTheoryEeClasses(){} - void resetInstantiationRound(){}; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_eq = eq::EqClassesIterator( d_ee ); - }; //* the argument is not used - TNode getNextCandidate(){ - if( !d_eq.isFinished() ) return (*(d_eq++)); - else return Node::null(); - }; -}; - -// Just iterate among the equivalence class of the given node -// node::Null() *can't* be given to reset -class CandidateGeneratorTheoryEeClass : public CandidateGenerator{ -private: - //instantiator pointer - EqualityEngine* d_ee; - //the equality class iterator - eq::EqClassIterator d_eqc; - /* For the case where the given term doesn't exists in uf */ - Node d_retNode; -public: - CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} - ~CandidateGeneratorTheoryEeClass(){} - void resetInstantiationRound(){}; - void reset( TNode eqc ){ - Assert(!eqc.isNull()); - if( d_ee->hasTerm( eqc ) ){ - /* eqc is in uf */ - eqc = d_ee->getRepresentative( eqc ); - d_eqc = eq::EqClassIterator( eqc, d_ee ); - d_retNode = Node::null(); - }else{ - /* If eqc if not a term known by uf, it is the only one in its - equivalence class. So we will return only it */ - d_retNode = eqc; - d_eqc = eq::EqClassIterator(); - } - }; //* the argument is not used - TNode getNextCandidate(){ - if(d_retNode.isNull()){ - if( !d_eqc.isFinished() ) return (*(d_eqc++)); - else return Node::null(); - }else{ - /* the case where eqc not in uf */ - Node ret = d_retNode; - d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ - return ret; - } - }; -}; - - -} /* namespace rrinst */ -} /* namespace eq */ - -namespace uf{ -namespace rrinst { - -typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; - -class CandidateGeneratorTheoryUfOp : public CandidateGenerator{ -private: - Node d_op; - //instantiator pointer - TermDb* d_tdb; - // Since new term can appears we restrict ourself to the one that - // exists at resetInstantiationRound - size_t d_term_iter_limit; - size_t d_term_iter; -public: - CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){} - ~CandidateGeneratorTheoryUfOp(){} - void resetInstantiationRound(){ - d_term_iter_limit = d_tdb->d_op_map[d_op].size(); - }; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_term_iter = 0; - }; //* the argument is not used - TNode getNextCandidate(){ - if( d_term_iterd_op_map[d_op][d_term_iter]; - ++d_term_iter; - return n; - } else return Node::null(); - }; -}; - -class CandidateGeneratorTheoryUfType : public CandidateGenerator{ -private: - TypeNode d_type; - //instantiator pointer - TermDb* d_tdb; - // Since new term can appears we restrict ourself to the one that - // exists at resetInstantiationRound - size_t d_term_iter_limit; - size_t d_term_iter; -public: - CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){} - ~CandidateGeneratorTheoryUfType(){} - void resetInstantiationRound(){ - d_term_iter_limit = d_tdb->d_type_map[d_type].size(); - }; - void reset( TNode eqc ){ - Assert(eqc.isNull()); - d_term_iter = 0; - }; //* the argument is not used - TNode getNextCandidate(){ - if( d_term_iterd_type_map[d_type][d_term_iter]; - ++d_term_iter; - return n; - } else return Node::null(); - }; -}; - -} /* namespace rrinst */ -} /* namespace uf */ - -class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ - - /** The candidate generators */ - rrinst::CandidateGenerator* d_master_can_gen; - /** QuantifierEngine */ - QuantifiersEngine* d_qe; -public: - GenericCandidateGeneratorClasses(QuantifiersEngine * qe); - ~GenericCandidateGeneratorClasses(); - - void resetInstantiationRound(); - void reset(TNode eqc); - TNode getNextCandidate(); - void lookForNextTheory(); -}; - -class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ - - /** The candidate generators */ - rrinst::CandidateGenerator* d_master_can_gen; - /** QuantifierEngine */ - QuantifiersEngine* d_qe; -public: - GenericCandidateGeneratorClass(QuantifiersEngine * qe); - ~GenericCandidateGeneratorClass(); - void resetInstantiationRound(); - void reset(TNode eqc); - TNode getNextCandidate(); -}; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H */ diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp deleted file mode 100644 index 2d7cf85fd..000000000 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ /dev/null @@ -1,1596 +0,0 @@ -/********************* */ -/*! \file rr_inst_match.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Francois Bobot - ** Minor contributors (to current version): Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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 inst match class - **/ - -#include "theory/quantifiers/inst_match.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "theory/uf/equality_engine.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/datatypes/theory_datatypes.h" -#include "theory/rewriterules/rr_inst_match.h" -#include "theory/rewriterules/rr_trigger.h" -#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; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::rrinst; -using namespace CVC4::theory::uf::rrinst; -using namespace CVC4::theory::eq::rrinst; - -namespace CVC4{ -namespace theory{ -namespace rrinst{ - - - - -InstMatch::InstMatch() { -} - -InstMatch::InstMatch( InstMatch* m ) { - d_map = m->d_map; -} - -bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){ - std::map< Node, Node >::iterator vn = d_map.find( v ); - if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){ - set = false; - return false; - }else if( vn==d_map.end() || vn->second.isNull() ){ - set = true; - this->set(v,m); - Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl; - return true; - }else{ - set = false; - return q->areEqual( vn->second, m ); - } -} - -bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ - bool set; - return setMatch(q,v,m,set); -} - -bool InstMatch::add( InstMatch& m ){ - for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - if( !it->second.isNull() ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[it->first] = it->second; - } - } - } - return true; -} - -bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ - for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - if( !it->second.isNull() ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[ it->first ] = it->second; - }else{ - if( !q->areEqual( it->second, itf->second ) ){ - d_map.clear(); - return false; - } - } - } - } - return true; -} - -void InstMatch::debugPrint( const char* c ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - Debug( c ) << " " << it->first << " -> " << it->second << std::endl; - } - //if( !d_splits.empty() ){ - // Debug( c ) << " Conditions: "; - // for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){ - // Debug( c ) << it->first << " = " << it->second << " "; - // } - // Debug( c ) << std::endl; - //} -} - -void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); - if( d_map.find( ic )==d_map.end() ){ - d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } - } -} - -//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ -// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); -// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ -// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); -// } -//} - -void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); - } - } -} - -void InstMatch::applyRewrite(){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - it->second = Rewriter::rewrite(it->second); - } -} - -/** get value */ -Node InstMatch::getValue( Node var ) const{ - std::map< Node, Node >::const_iterator it = d_map.find( var ); - if( it!=d_map.end() ){ - return it->second; - }else{ - return Node::null(); - } -} - -Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { - return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) ); -} - -void InstMatch::set(TNode var, TNode n){ - Assert( !var.isNull() ); - if (Trace.isOn("inst-match-warn")) { - // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ - Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl; - Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; - } - } - Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) ); - d_map[var] = n; -} - -void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { - set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n ); -} - - - - - - -typedef CVC4::theory::rrinst::InstMatch InstMatch; -typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue; - -template -class InstMatchTrie2Pairs -{ - typename std::vector< std::vector < typename InstMatchTrie2Gen::Tree > > d_data; - InstMatchTrie2Gen d_backtrack; -public: - InstMatchTrie2Pairs(context::Context* c, QuantifiersEngine* q, size_t n): - d_backtrack(c,q) { - // resize to a triangle - // - // | * - // | * * - // | * * * - // | -----> i - d_data.resize(n); - for(size_t i=0; i < n; ++i){ - d_data[i].resize(i+1,typename InstMatchTrie2Gen::Tree(0)); - } - }; - InstMatchTrie2Pairs(const InstMatchTrie2Pairs &) CVC4_UNDEFINED; - const InstMatchTrie2Pairs & operator =(const InstMatchTrie2Pairs & e) CVC4_UNDEFINED; - /** add match m in the trie, - return true if it was never seen */ - inline bool addInstMatch( size_t i, size_t j, InstMatch& m){ - size_t k = std::min(i,j); - size_t l = std::max(i,j); - return d_backtrack.addInstMatch(m,&(d_data[l][k])); - }; - inline bool addInstMatch( size_t i, InstMatch& m){ - return d_backtrack.addInstMatch(m,&(d_data[i][i])); - }; - -}; - - -// Currently the implementation doesn't take into account that -// variable should have the same value given. -// TODO use the d_children way perhaps -// TODO replace by a real dictionnary -// We should create a real substitution? slower more precise -// We don't do that often -bool nonunifiable( TNode t0, TNode pat, const std::vector & vars){ - if(pat.isNull()) return true; - - typedef std::vector > tstack; - tstack stack(1,std::make_pair(t0,pat)); // t * pat - - while(!stack.empty()){ - const std::pair p = stack.back(); stack.pop_back(); - const TNode & t = p.first; - const TNode & pat = p.second; - - // t or pat is a variable currently we consider that can match anything - if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; - if( pat.getKind() == INST_CONSTANT ) continue; - - // t and pat are nonunifiable - if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { - if(t == pat) continue; - else return true; - }; - if( t.getOperator() != pat.getOperator() ) return true; - - //put the children on the stack - for( size_t i=0; i < pat.getNumChildren(); i++ ){ - stack.push_back(std::make_pair(t[i],pat[i])); - }; - } - // The heuristic can't find non-unifiability - return false; -}; - -/** New things */ -class DumbMatcher: public Matcher{ - void resetInstantiationRound( QuantifiersEngine* qe ){}; - bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ - return false; - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return false; - } -}; - -class DumbPatMatcher: public PatMatcher{ - void resetInstantiationRound( QuantifiersEngine* qe ){}; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return false; - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return false; - } -}; - - -/* The order of the matching is: - reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */ -ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){ - - //set-up d_variables, d_constants, d_childrens - for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){ - //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType()); - EqualityQuery* q = qe->getEqualityQuery(); - Assert( q != NULL ); - if( quantifiers::TermDb::hasInstConstAttr(d_pattern[i]) ){ - if( d_pattern[i].getKind()==INST_CONSTANT ){ - //It's a variable - d_variables.push_back(make_triple((TNode)d_pattern[i],i,q)); - }else{ - //It's neither a constant argument neither a variable - //we create the matcher for the subpattern - d_childrens.push_back(make_triple(mkMatcher((TNode)d_pattern[i], qe),i,q)); - }; - }else{ - // It's a constant - d_constants.push_back(make_triple((TNode)d_pattern[i],i,q)); - } - } -} - -void ApplyMatcher::resetInstantiationRound( QuantifiersEngine* qe ){ - for( size_t i=0; i< d_childrens.size(); i++ ){ - d_childrens[i].first->resetInstantiationRound( qe ); - } -} - -bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){ - Debug("matching") << "Matching " << t << " against pattern " << d_pattern << " (" - << m.size() << ")" << std::endl; - - //if t is null - Assert( !t.isNull() ); - Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); - Assert( t.getKind()==d_pattern.getKind() ); - Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR) - || t.getOperator()==d_pattern.getOperator() ); - - typedef std::vector< triple >::iterator iterator; - for(iterator i = d_constants.begin(), end = d_constants.end(); - i != end; ++i){ - if( !i->third->areEqual( i->first, t[i->second] ) ){ - Debug("matching-fail") << "Match fail arg: " << i->first << " and " << t[i->second] << std::endl; - //setMatchFail( qe, d_pattern[i], t[i] ); - //ground arguments are not equal - return false; - } - } - - d_binded.clear(); - bool set; - for(iterator i = d_variables.begin(), end = d_variables.end(); - i != end; ++i){ - if( !m.setMatch( i->third, i->first, t[i->second], set) ){ - //match is in conflict - Debug("matching-debug") << "Match in conflict " << t[i->second] << " and " - << i->first << " because " - << m.get(i->first) - << std::endl; - Debug("matching-fail") << "Match fail: " << m.get(i->first) << " and " << t[i->second] << std::endl; - //setMatchFail( qe, partial[0].d_map[d_pattern[i]], t[i] ); - m.erase(d_binded.begin(), d_binded.end()); - return false; - }else{ - if(set){ //The variable has just been set - d_binded.push_back(i->first); - } - } - } - - //now, fit children into match - //we will be requesting candidates for matching terms for each child - d_reps.clear(); - for( size_t i=0; i< d_childrens.size(); i++ ){ - Debug("matching-debug") << "Take the representative of " << t[ d_childrens[i].second ] << std::endl; - Assert( d_childrens[i].third->hasTerm(t[ d_childrens[i].second ]) ); - Node rep = d_childrens[i].third->getRepresentative( t[ d_childrens[i].second ] ); - d_reps.push_back( rep ); - } - - if(d_childrens.size() == 0) return true; - else return getNextMatch(m, qe, true); -} - -bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset){ - Assert(d_childrens.size() > 0); - const size_t max = d_childrens.size() - 1; - size_t index = reset ? 0 : max; - Assert(d_childrens.size() == d_reps.size()); - while(true){ - if(reset ? - d_childrens[index].first->reset( d_reps[index], m, qe ) : - d_childrens[index].first->getNextMatch( m, qe )){ - if(index==max) return true; - ++index; - reset=true; - }else{ - if(index==0){ - m.erase(d_binded.begin(), d_binded.end()); - return false; - } - --index; - reset=false; - }; - } -} - -bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe){ - if(d_childrens.size() == 0){ - m.erase(d_binded.begin(), d_binded.end()); - return false; - } else return getNextMatch(m, qe, false); -} - -/** Proxy that call the sub-matcher on the result return by the given candidate generator */ -template -class CandidateGeneratorMatcher: public Matcher{ - /** candidate generator */ - CG d_cg; - /** the sub-matcher */ - M d_m; -public: - CandidateGeneratorMatcher(CG cg, M m): d_cg(cg), d_m(m) - {/* last is Null */}; - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cg.resetInstantiationRound(); - d_m.resetInstantiationRound(qe); - }; - bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ - d_cg.reset(n); - return findMatch(m,qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - // The sub-matcher has another match - return d_m.getNextMatch(m, qe) || findMatch(m,qe); - } -private: - bool findMatch( InstMatch& m, QuantifiersEngine* qe ){ - // Otherwise try to find a new candidate that has at least one match - while(true){ - TNode n = d_cg.getNextCandidate();//kept somewhere Term-db - Debug("matching") << "GenCand " << n << " (" << this << ")" << std::endl; - if(n.isNull()) return false; - if(d_m.reset(n,m,qe)) return true; - }; - } -}; - -/** Proxy that call the sub-matcher on the result return by the given candidate generator */ -template -class PatOfMatcher: public PatMatcher{ - M d_m; -public: - inline PatOfMatcher(M m): d_m(m){} - void resetInstantiationRound(QuantifiersEngine* qe){ - d_m.resetInstantiationRound(qe); - } - bool reset(InstMatch& m, QuantifiersEngine* qe){ - return d_m.reset(Node::null(),m,qe); - }; - bool getNextMatch(InstMatch& m, QuantifiersEngine* qe){ - return d_m.getNextMatch(m,qe); - }; -}; - -class ArithMatcher: public Matcher{ -private: - /** for arithmetic matching */ - std::map< Node, Node > d_arith_coeffs; - /** get the match against ground term or formula t. - d_match_mattern and t should have the same shape. - only valid for use where !d_match_pattern.isNull(). - */ - /** the variable that are set by this matcher */ - std::vector< TNode > d_binded; /* TNode because the variables are already in d_arith_coeffs */ - Node d_pattern; //for debugging -public: - ArithMatcher(Node pat, QuantifiersEngine* qe); - void resetInstantiationRound( QuantifiersEngine* qe ){}; - bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ); - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); -}; - -/** Match just a variable */ -class VarMatcher: public Matcher{ - Node d_var; - bool d_binded; /* True if the reset bind the variable to some value */ - EqualityQuery* d_q; -public: - VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){ - //d_q = qe->getEqualityQuery(var.getType()); - d_q = qe->getEqualityQuery(); - } - void resetInstantiationRound( QuantifiersEngine* qe ){}; - bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ - if(!m.setMatch( d_q, d_var, n, d_binded )){ - //match is in conflict - Debug("matching-fail") << "Match fail: " << m.get(d_var) - << " and " << n << std::endl; - return false; - } else return true; - }; - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - //match is in conflict - if (d_binded) m.erase(d_var); - return false; - } -}; - -template -class TestMatcher: public Matcher{ - M d_m; - Test d_test; -public: - inline TestMatcher(M m, Test test): d_m(m), d_test(test){} - inline void resetInstantiationRound(QuantifiersEngine* qe){ - d_m.resetInstantiationRound(qe); - } - inline bool reset(TNode n, InstMatch& m, QuantifiersEngine* qe){ - return d_test(n) && d_m.reset(n, m, qe); - } - inline bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_m.getNextMatch(m, qe); - } -}; - -class LegalOpTest/*: public unary_function*/ { - Node d_op; -public: - inline LegalOpTest(Node op): d_op(op){} - inline bool operator() (TNode n) { - return - CandidateGenerator::isLegalCandidate(n) && - // ( // n.getKind()==SELECT || n.getKind()==STORE || - // n.getKind()==APPLY_UF || n.getKind()==APPLY_CONSTRUCTOR) && - n.hasOperator() && - n.getOperator()==d_op; - }; -}; - -class LegalKindTest/* : public unary_function*/ { - Kind d_kind; -public: - inline LegalKindTest(Kind kind): d_kind(kind){} - inline bool operator() (TNode n) { - return - CandidateGenerator::isLegalCandidate(n) && - n.getKind()==d_kind; - }; -}; - -class LegalTypeTest/* : public unary_function*/ { - TypeNode d_type; -public: - inline LegalTypeTest(TypeNode type): d_type(type){} - inline bool operator() (TNode n) { - return - CandidateGenerator::isLegalCandidate(n) && - n.getType()==d_type; - }; -}; - -class LegalTest/* : public unary_function*/ { -public: - inline bool operator() (TNode n) { - return CandidateGenerator::isLegalCandidate(n); - }; -}; - -size_t numFreeVar(TNode t){ - size_t n = 0; - for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){ - if( quantifiers::TermDb::hasInstConstAttr(t[i]) ){ - if( t[i].getKind()==INST_CONSTANT ){ - //variable - ++n; - }else{ - //neither variable nor constant - n += numFreeVar(t[i]); - } - } - } - return n; -} - -class OpMatcher: public Matcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - Assert( pat.getKind() == kind::APPLY_UF ); - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); - /** Iter on the equivalence class of the given term */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); - CandidateGeneratorTheoryEeClass cdtUfEq(ee); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtUfEq,am2); - return am1; - } - size_t d_num_var; - Node d_pat; -public: - OpMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ - // size_t m_size = m.d_map.size(); - // if(m_size == d_num_var){ - // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine(); - // std::cout << "!"; - // return ee->areEqual(m.subst(d_pat),t); - // }else{ - // std::cout << m.d_map.size() << std::endl; - return d_cgm.reset(t, m, qe); - // } - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -class DatatypesMatcher: public Matcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR, - "For datatypes only constructor are accepted in pattern" ); - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); - /** Iter on the equivalence class of the given term */ - datatypes::TheoryDatatypes* dt = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_DATATYPES )); - eq::EqualityEngine* ee = static_cast(dt->getEqualityEngine()); - CandidateGeneratorTheoryEeClass cdtDtEq(ee); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtDtEq,am2); - return am1; - } - Node d_pat; -public: - DatatypesMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching") << "datatypes: " << t << " matches " << d_pat << std::endl; - return d_cgm.reset(t, m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -class ArrayMatcher: public Matcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalKindTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - Assert( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ); - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3, LegalKindTest(pat.getKind())); - /** Iter on the equivalence class of the given term */ - arrays::TheoryArrays* ar = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_ARRAY )); - eq::EqualityEngine* ee = - static_cast(ar->getEqualityEngine()); - CandidateGeneratorTheoryEeClass cdtUfEq(ee); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtUfEq,am2); - return am1; - } - size_t d_num_var; - Node d_pat; -public: - ArrayMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ - // size_t m_size = m.d_map.size(); - // if(m_size == d_num_var){ - // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine(); - // std::cout << "!"; - // return ee->areEqual(m.subst(d_pat),t); - // }else{ - // std::cout << m.d_map.size() << std::endl; - return d_cgm.reset(t, m, qe); - // } - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -class AllOpMatcher: public PatMatcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfOp, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - Assert( pat.hasOperator() ); - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3,LegalTest()); - /** Iter on the equivalence class of the given term */ - TermDb* tdb = qe->getTermDatabase(); - Node op = tdb->getOperator( pat ); - CandidateGeneratorTheoryUfOp cdtUfEq(op,tdb); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtUfEq,am2); - return am1; - } - size_t d_num_var; - Node d_pat; -public: - AllOpMatcher( TNode pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)), d_num_var(numFreeVar(pat)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - // std::cout << m.d_map.size() << "/" << d_num_var << std::endl; - return d_cgm.reset(Node::null(), m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -template /** true classes | false class */ -class GenericCandidateGeneratorClasses: public CandidateGenerator{ -private: - CandidateGenerator* d_cg; - QuantifiersEngine* d_qe; - -public: - void mkCandidateGenerator(){ - if(classes) - d_cg = new GenericCandidateGeneratorClasses(d_qe); - else - d_cg = new GenericCandidateGeneratorClass(d_qe); - } - - GenericCandidateGeneratorClasses(QuantifiersEngine* qe): - d_qe(qe) { - mkCandidateGenerator(); - } - ~GenericCandidateGeneratorClasses(){ - delete(d_cg); - } - const GenericCandidateGeneratorClasses & operator =(const GenericCandidateGeneratorClasses & m){ - mkCandidateGenerator(); - return m; - }; - GenericCandidateGeneratorClasses(const GenericCandidateGeneratorClasses & m): - d_qe(m.d_qe){ - mkCandidateGenerator(); - } - void resetInstantiationRound(){ - d_cg->resetInstantiationRound(); - }; - void reset( TNode eqc ){ - Assert( !classes || eqc.isNull() ); - d_cg->reset(eqc); - }; //* the argument is not used - TNode getNextCandidate(){ - return d_cg->getNextCandidate(); - }; -}; /* MetaCandidateGeneratorClasses */ - - -class GenericMatcher: public Matcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); - /** Iter on the equivalence class of the given term */ - GenericCandidateGeneratorClasses cdtG(qe); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtG,am2); - return am1; - } - Node d_pat; -public: - GenericMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(t, m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - - -class GenericPatMatcher: public PatMatcher{ - /* The matcher */ - typedef ApplyMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses, AuxMatcher2> AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - /** In reverse order of matcher sequence */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good operator */ - AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); - /** Iter on the equivalence class of the given term */ - GenericCandidateGeneratorClasses cdtG(qe); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtG,am2); - return am1; - } - Node d_pat; -public: - GenericPatMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)), - d_pat(pat) {} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(Node::null(), m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -class MetaCandidateGeneratorClasses: public CandidateGenerator{ -private: - CandidateGenerator* d_cg; - TypeNode d_ty; - TheoryEngine* d_te; - -public: - CandidateGenerator* mkCandidateGenerator(TypeNode ty, TheoryEngine* te){ - Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty - << " Theory : " << Theory::theoryOf(ty) << std::endl; - if( Theory::theoryOf(ty) == theory::THEORY_DATATYPES ){ - // datatypes::TheoryDatatypes* dt = static_cast(te->theoryOf( theory::THEORY_DATATYPES )); - // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt); - Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES"); - }else if ( Theory::theoryOf(ty) == theory::THEORY_ARRAY ){ - arrays::TheoryArrays* ar = static_cast(te->theoryOf( theory::THEORY_ARRAY )); - eq::EqualityEngine* ee = - static_cast(ar->getEqualityEngine()); - return new CandidateGeneratorTheoryEeClasses(ee); - } else { - uf::TheoryUF* uf = static_cast(te->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); - return new CandidateGeneratorTheoryEeClasses(ee); - } - } - MetaCandidateGeneratorClasses(TypeNode ty, TheoryEngine* te): - d_ty(ty), d_te(te) { - d_cg = mkCandidateGenerator(ty,te); - } - ~MetaCandidateGeneratorClasses(){ - delete(d_cg); - } - const MetaCandidateGeneratorClasses & operator =(const MetaCandidateGeneratorClasses & m){ - d_cg = mkCandidateGenerator(m.d_ty, m.d_te); - return m; - }; - MetaCandidateGeneratorClasses(const MetaCandidateGeneratorClasses & m): - d_ty(m.d_ty), d_te(m.d_te){ - d_cg = mkCandidateGenerator(m.d_ty, m.d_te); - } - void resetInstantiationRound(){ - d_cg->resetInstantiationRound(); - }; - void reset( TNode eqc ){ - d_cg->reset(eqc); - }; //* the argument is not used - TNode getNextCandidate(){ - return d_cg->getNextCandidate(); - }; -}; /* MetaCandidateGeneratorClasses */ - -/** Match just a variable */ -class AllVarMatcher: public PatMatcher{ -private: - /* generator */ - typedef VarMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< MetaCandidateGeneratorClasses, AuxMatcher2 > AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(TNode pat, QuantifiersEngine* qe){ - Assert( pat.getKind()==INST_CONSTANT ); - TypeNode ty = pat.getType(); - Debug("inst-match-gen") << "create AllVarMatcher for type: " << ty << std::endl; - /** In reverse order of matcher sequence */ - /** Distribute it to all the pattern */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good type */ - AuxMatcher2 am2(am3,LegalTypeTest(ty)); - /** Generate one term by eq classes */ - MetaCandidateGeneratorClasses mcdt(ty,qe->getTheoryEngine()); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(mcdt,am2); - return am1; - } -public: - AllVarMatcher( TNode pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)){} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -/** Match all the pattern with the same term */ -class SplitMatcher: public Matcher{ -private: - const size_t size; - ApplyMatcher d_m; /** Use ApplyMatcher by creating a fake application */ -public: - SplitMatcher(std::vector< Node > pats, QuantifiersEngine* qe): - size(pats.size()), - d_m(NodeManager::currentNM()->mkNode(kind::INST_PATTERN,pats), qe) {} - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_m.resetInstantiationRound(qe); - }; - bool reset( TNode ex, InstMatch& m, QuantifiersEngine* qe ){ - NodeBuilder<> n(kind::INST_PATTERN); - for(size_t i = 0; i < size; ++i) n << ex; - Node nn = n; - return d_m.reset(nn,m,qe); - }; - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return getNextMatch(m, qe); - } -}; - - -/** Match uf term in a fixed equivalence class */ -class UfCstEqMatcher: public PatMatcher{ -private: - /* equivalence class to match */ - Node d_cst; - /* generator */ - OpMatcher d_cgm; -public: - UfCstEqMatcher( Node pat, Node cst, QuantifiersEngine* qe ): - d_cst(cst), - d_cgm(OpMatcher(pat,qe)) {}; - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(d_cst, m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -/** Match equalities */ -class UfEqMatcher: public PatMatcher{ -private: - /* generator */ - typedef SplitMatcher AuxMatcher3; - typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClasses, AuxMatcher2 > AuxMatcher1; - AuxMatcher1 d_cgm; - static inline AuxMatcher1 createCgm(std::vector & pat, QuantifiersEngine* qe){ - Assert( pat.size() > 0); - TypeNode ty = pat[0].getType(); - for(size_t i = 1; i < pat.size(); ++i){ - Assert(pat[i].getType() == ty); - } - /** In reverse order of matcher sequence */ - /** Distribute it to all the pattern */ - AuxMatcher3 am3(pat,qe); - /** Keep only the one that have the good type */ - AuxMatcher2 am2(am3,LegalTypeTest(ty)); - /** Generate one term by eq classes */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); - CandidateGeneratorTheoryEeClasses cdtUfEq(ee); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtUfEq,am2); - return am1; - } -public: - UfEqMatcher( std::vector & pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)){} - - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - - -/** Match dis-equalities */ -class UfDeqMatcher: public PatMatcher{ -private: - /* generator */ - typedef ApplyMatcher AuxMatcher3; - - class EqTest/* : public unary_function*/ { - TypeNode d_type; - public: - inline EqTest(TypeNode type): d_type(type){}; - inline bool operator() (Node n) { - return - CandidateGenerator::isLegalCandidate(n) && - n.getKind() == kind::EQUAL && - n[0].getType()==d_type; - }; - }; - typedef TestMatcher< AuxMatcher3, EqTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2 > AuxMatcher1; - AuxMatcher1 d_cgm; - Node false_term; - static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ - Assert( pat.getKind() == kind::NOT); - TNode eq = pat[0]; - Assert( eq.getKind() == kind::EQUAL); - TypeNode ty = eq[0].getType(); - /** In reverse order of matcher sequence */ - /** Distribute it to all the pattern */ - AuxMatcher3 am3(eq,qe); - /** Keep only the one that have the good type */ - AuxMatcher2 am2(am3,EqTest(ty)); - /** Will generate all the terms of the eq class of false */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); - CandidateGeneratorTheoryEeClass cdtUfEq(ee); - /* Create a matcher from the candidate generator */ - AuxMatcher1 am1(cdtUfEq,am2); - return am1; - } -public: - UfDeqMatcher( Node pat, QuantifiersEngine* qe ): - d_cgm(createCgm(pat, qe)), - false_term((static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine()-> - getRepresentative(NodeManager::currentNM()->mkConst(false) )){}; - void resetInstantiationRound( QuantifiersEngine* qe ){ - d_cgm.resetInstantiationRound(qe); - }; - bool reset( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.reset(false_term, m, qe); - } - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - return d_cgm.getNextMatch(m, qe); - } -}; - -Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ - Debug("inst-match-gen") << "mkMatcher: Pattern term is " << pat << std::endl; - - // if( pat.getKind() == kind::APPLY_UF){ - // return new OpMatcher(pat, qe); - // } else if( pat.getKind() == kind::APPLY_CONSTRUCTOR ){ - // return new DatatypesMatcher(pat, qe); - // } else if( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){ - // return new ArrayMatcher(pat, qe); - if( pat.getKind() == kind::APPLY_UF || - pat.getKind() == kind::APPLY_CONSTRUCTOR || - pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){ - return new GenericMatcher(pat, qe); - } else { /* Arithmetic? */ - /** TODO: something simpler to see if the pattern is a good - arithmetic pattern */ - std::map< Node, Node > d_arith_coeffs; - if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){ - Message() << "(?) Unknown matching pattern is " << pat << std::endl; - Unimplemented("pattern not implemented"); - return new DumbMatcher(); - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - ArithMatcher am3 (pat, qe); - TestMatcher - am2(am3,LegalTypeTest(pat.getType())); - /* generator */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast (uf->getEqualityEngine()); - CandidateGeneratorTheoryEeClass cdtUfEq(ee); - return new CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, - TestMatcher > (cdtUfEq,am2); - } - } -}; - -PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ - Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; - Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); - - if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){ - /* Difference */ - return new UfDeqMatcher(pat, qe); - } else if (pat.getKind() == kind::EQUAL){ - if( !quantifiers::TermDb::hasInstConstAttr(pat[0])){ - Assert(quantifiers::TermDb::hasInstConstAttr(pat[1])); - return new UfCstEqMatcher(pat[1], pat[0], qe); - }else if( !quantifiers::TermDb::hasInstConstAttr(pat[1] )){ - Assert(quantifiers::TermDb::hasInstConstAttr(pat[0])); - return new UfCstEqMatcher(pat[0], pat[1], qe); - }else{ - std::vector< Node > pats(pat.begin(),pat.end()); - return new UfEqMatcher(pats,qe); - } - } else if( Trigger::isAtomicTrigger( pat ) ){ - return new AllOpMatcher(pat, qe); - // return new GenericPatMatcher(pat, qe); - } else if( pat.getKind()==INST_CONSTANT ){ - // just a variable - return new AllVarMatcher(pat, qe); - } else { /* Arithmetic? */ - /** TODO: something simpler to see if the pattern is a good - arithmetic pattern */ - std::map< Node, Node > d_arith_coeffs; - if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){ - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl; - Message() << "(?) Unknown matching pattern is " << pat << std::endl; - return new DumbPatMatcher(); - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - ArithMatcher am3 (pat, qe); - TestMatcher - am2(am3,LegalTest()); - /* generator */ - TermDb* tdb = qe->getTermDatabase(); - CandidateGeneratorTheoryUfType cdtUfEq(pat.getType(),tdb); - typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfType, - TestMatcher > AuxMatcher1; - return new PatOfMatcher(AuxMatcher1(cdtUfEq,am2)); - } - } -}; - -ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){ - - if(Trigger::getPatternArithmetic(quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ) - { - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl; - Assert(false); - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << d_pattern << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - } - -}; - -bool ArithMatcher::reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching-arith") << "Matching " << t << " " << d_pattern << std::endl; - d_binded.clear(); - if( !d_arith_coeffs.empty() ){ - NodeBuilder<> tb(kind::PLUS); - Node ic = Node::null(); - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << it->first << " -> " << it->second << std::endl; - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - //see if we can choose this to set - if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ - ic = it->first; - } - }else{ - Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; - Node tm = m.get( it->first ); - if( !it->second.isNull() ){ - tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); - } - tb << tm; - } - }else{ - tb << it->second; - } - } - if( !ic.isNull() ){ - Node tm; - if( tb.getNumChildren()==0 ){ - tm = t; - }else{ - tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); - } - if( !d_arith_coeffs[ ic ].isNull() ){ - Assert( !ic.getType().isInteger() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst() ); - tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); - } - m.set( ic, Rewriter::rewrite( tm )); - d_binded.push_back(ic); - //set the rest to zeros - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) )); - d_binded.push_back(ic); - } - } - } - Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; - return true; - }else{ - m.erase(d_binded.begin(), d_binded.end()); - return false; - } - }else{ - m.erase(d_binded.begin(), d_binded.end()); - return false; - } -}; - -bool ArithMatcher::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - m.erase(d_binded.begin(), d_binded.end()); - return false; -}; - - -class MultiPatsMatcher: public PatsMatcher{ -private: - bool d_reset_done; - std::vector< PatMatcher* > d_patterns; - InstMatch d_im; - bool reset( QuantifiersEngine* qe ){ - d_im.clear(); - d_reset_done = true; - - return getNextMatch(qe,true); - }; - - bool getNextMatch(QuantifiersEngine* qe, bool reset){ - const size_t max = d_patterns.size() - 1; - size_t index = reset ? 0 : max; - while(true){ - Debug("matching") << "MultiPatsMatcher::index " << index << "/" - << max << (reset ? " reset_phase" : "") << std::endl; - if(reset ? - d_patterns[index]->reset( d_im, qe ) : - d_patterns[index]->getNextMatch( d_im, qe )){ - if(index==max) return true; - ++index; - reset=true; - }else{ - if(index==0) return false; - --index; - reset=false; - }; - } - } - -public: - MultiPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe): - d_reset_done(false){ - Assert(pats.size() > 0); - for( size_t i=0; i< pats.size(); i++ ){ - d_patterns.push_back(mkPattern(pats[i],qe)); - }; - }; - void resetInstantiationRound( QuantifiersEngine* qe ){ - for( size_t i=0; i< d_patterns.size(); i++ ){ - d_patterns[i]->resetInstantiationRound( qe ); - }; - d_reset_done = false; - d_im.clear(); - }; - bool getNextMatch( QuantifiersEngine* qe ){ - Assert(d_patterns.size()>0); - if(d_reset_done) return getNextMatch(qe,false); - else return reset(qe); - } - const InstMatch& getInstMatch(){return d_im;}; - - int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe); -}; - -enum EffiStep{ - ES_STOP, - ES_GET_MONO_CANDIDATE, - ES_GET_MULTI_CANDIDATE, - ES_RESET1, - ES_RESET2, - ES_NEXT1, - ES_NEXT2, - ES_RESET_OTHER, - ES_NEXT_OTHER, -}; -static inline std::ostream& operator<<(std::ostream& out, const EffiStep& step) { - switch(step){ - case ES_STOP: out << "STOP"; break; - case ES_GET_MONO_CANDIDATE: out << "GET_MONO_CANDIDATE"; break; - case ES_GET_MULTI_CANDIDATE: out << "GET_MULTI_CANDIDATE"; break; - case ES_RESET1: out << "RESET1"; break; - case ES_RESET2: out << "RESET2"; break; - case ES_NEXT1: out << "NEXT1"; break; - case ES_NEXT2: out << "NEXT2"; break; - case ES_RESET_OTHER: out << "RESET_OTHER"; break; - case ES_NEXT_OTHER: out << "NEXT_OTHER"; break; - } - return out; -} - - -int MultiPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){ - //now, try to add instantiation for each match produced - int addedLemmas = 0; - resetInstantiationRound( qe ); - d_im.add( baseMatch ); - while( getNextMatch( qe ) ){ - InstMatch im_copy = getInstMatch(); - std::vector< Node > terms; - for( unsigned i=0; igetEqualityQuery() ); - if( qe->addInstantiation( quant, terms ) ){ - addedLemmas++; - } - } - //return number of lemmas added - return addedLemmas; -} - -PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ){ - return new MultiPatsMatcher( pat, qe); -} - -class MultiEfficientPatsMatcher: public PatsMatcher{ -private: - bool d_phase_mono; - bool d_phase_new_term; - std::vector< PatMatcher* > d_patterns; - std::vector< Matcher* > d_direct_patterns; - InstMatch d_im; - EfficientHandler d_eh; - EfficientHandler::MultiCandidate d_mc; - InstMatchTrie2Pairs d_cache; - std::vector d_pats; - // bool indexDone( size_t i){ - // return i == d_c.first.second || - // ( i == d_c.second.second && d_c.second.first.empty()); - // } - - - - static const EffiStep ES_START = ES_GET_MONO_CANDIDATE; - EffiStep d_step; - - //return true if it becomes bigger than d_patterns.size() - 1 - bool incrIndex(size_t & index){ - if(index == d_patterns.size() - 1) return true; - ++index; - if(index == d_mc.first.second - || (!d_phase_mono && index == d_mc.second.second)) - return incrIndex(index); - else return false; - } - - //return true if it becomes smaller than 0 - bool decrIndex(size_t & index){ - if(index == 0) return true; - --index; - if(index == d_mc.first.second - || (!d_phase_mono && index == d_mc.second.second)) - return decrIndex(index); - else return false; - } - - bool resetOther( QuantifiersEngine* qe ){ - return getNextMatchOther(qe,true); - }; - - - bool getNextMatchOther(QuantifiersEngine* qe, bool reset){ - size_t index = reset ? 0 : d_patterns.size(); - if(!reset && decrIndex(index)) return false; - if( reset && - (index == d_mc.first.second - || (!d_phase_mono && index == d_mc.second.second)) - && incrIndex(index)) return true; - while(true){ - Debug("matching") << "MultiEfficientPatsMatcher::index " << index << "/" - << d_patterns.size() - 1 << std::endl; - if(reset ? - d_patterns[index]->reset( d_im, qe ) : - d_patterns[index]->getNextMatch( d_im, qe )){ - if(incrIndex(index)) return true; - reset=true; - }else{ - if(decrIndex(index)) return false; - reset=false; - }; - } - } - - inline EffiStep TestMonoCache(QuantifiersEngine* qe){ - if( //!d_phase_new_term || - d_pats.size() == 1) return ES_RESET_OTHER; - if(d_cache.addInstMatch(d_mc.first.second,d_im)){ - Debug("inst-match::cache") << "Cache miss" << d_im << std::endl; - ++qe->d_statistics.d_mono_candidates_cache_miss; - return ES_RESET_OTHER; - } else { - Debug("inst-match::cache") << "Cache hit" << d_im << std::endl; - ++qe->d_statistics.d_mono_candidates_cache_hit; - return ES_NEXT1; - } - // ++qe->d_statistics.d_mono_candidates_cache_miss; - // return ES_RESET_OTHER; - } - - inline EffiStep TestMultiCache(QuantifiersEngine* qe){ - if(d_cache.addInstMatch(d_mc.first.second,d_mc.second.second,d_im)){ - ++qe->d_statistics.d_multi_candidates_cache_miss; - return ES_RESET_OTHER; - } else { - ++qe->d_statistics.d_multi_candidates_cache_hit; - return ES_NEXT2; - } - } - - -public: - - bool getNextMatch( QuantifiersEngine* qe ){ - Assert( d_step == ES_START || d_step == ES_NEXT_OTHER || d_step == ES_STOP ); - while(true){ - Debug("matching") << "d_step=" << d_step << " " - << "d_im=" << d_im << std::endl; - switch(d_step){ - case ES_GET_MONO_CANDIDATE: - Assert(d_im.empty()); - if(d_phase_new_term ? d_eh.getNextMonoCandidate(d_mc.first) : d_eh.getNextMonoCandidateNewTerm(d_mc.first)){ - if(d_phase_new_term) ++qe->d_statistics.d_num_mono_candidates_new_term; - else ++qe->d_statistics.d_num_mono_candidates; - d_phase_mono = true; - d_step = ES_RESET1; - } else if (!d_phase_new_term){ - d_phase_new_term = true; - d_step = ES_GET_MONO_CANDIDATE; - } else { - d_phase_new_term = false; - d_step = ES_GET_MULTI_CANDIDATE; - } - break; - case ES_GET_MULTI_CANDIDATE: - Assert(d_im.empty()); - if(d_eh.getNextMultiCandidate(d_mc)){ - ++qe->d_statistics.d_num_multi_candidates; - d_phase_mono = false; - d_step = ES_RESET1; - } else d_step = ES_STOP; - break; - case ES_RESET1: - if(d_direct_patterns[d_mc.first.second]->reset(d_mc.first.first,d_im,qe)) - d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2; - else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE; - break; - case ES_RESET2: - Assert(!d_phase_mono); - if(d_direct_patterns[d_mc.second.second]->reset(d_mc.second.first,d_im,qe)) - d_step = TestMultiCache(qe); - else d_step = ES_NEXT1; - break; - case ES_NEXT1: - if(d_direct_patterns[d_mc.first.second]->getNextMatch(d_im,qe)) - d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2; - else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE; - break; - case ES_NEXT2: - if(d_direct_patterns[d_mc.second.second]->getNextMatch(d_im,qe)) - d_step = TestMultiCache(qe); - else d_step = ES_NEXT1; - break; - case ES_RESET_OTHER: - if(resetOther(qe)){ - d_step = ES_NEXT_OTHER; - return true; - } else d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2; - break; - case ES_NEXT_OTHER: - { - if(!getNextMatchOther(qe,false)){ - d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2; - }else{ - d_step = ES_NEXT_OTHER; - return true; - } - } - break; - case ES_STOP: - Assert(d_im.empty()); - return false; - } - } - } - - MultiEfficientPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe): - d_eh(qe->getTheoryEngine()->getSatContext()), - d_cache(qe->getTheoryEngine()->getSatContext(),qe,pats.size()), - d_pats(pats), d_step(ES_START) { - Assert(pats.size() > 0); - for( size_t i=0; i< pats.size(); i++ ){ - d_patterns.push_back(mkPattern(pats[i],qe)); - if(pats[i].getKind()==kind::INST_CONSTANT){ - d_direct_patterns.push_back(new VarMatcher(pats[i],qe)); - } else if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){ - d_direct_patterns.push_back(new ApplyMatcher(pats[i][0],qe)); - } else { - d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe)); - } - }; - EfficientEMatcher* eem = qe->getEfficientEMatcher(); - eem->registerEfficientHandler(d_eh, pats); - }; - void resetInstantiationRound( QuantifiersEngine* qe ){ - Assert(d_step == ES_START || d_step == ES_STOP); - for( size_t i=0; i< d_patterns.size(); i++ ){ - d_patterns[i]->resetInstantiationRound( qe ); - d_direct_patterns[i]->resetInstantiationRound( qe ); - }; - d_step = ES_START; - d_phase_new_term = false; - Assert(d_im.empty()); - }; - - const InstMatch& getInstMatch(){return d_im;}; - - int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe); -}; - -int MultiEfficientPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){ - //now, try to add instantiation for each match produced - int addedLemmas = 0; - Assert(baseMatch.empty()); - resetInstantiationRound( qe ); - while( getNextMatch( qe ) ){ - InstMatch im_copy = getInstMatch(); - std::vector< Node > terms; - for( unsigned i=0; igetEqualityQuery() ); - if( qe->addInstantiation( quant, terms ) ){ - addedLemmas++; - } - } - //return number of lemmas added - return addedLemmas; -}; - -PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ){ - return new MultiEfficientPatsMatcher( pat, qe); -} - -} /* CVC4::theory::rrinst */ -} /* CVC4::theory */ -} /* CVC4 */ diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h deleted file mode 100644 index c42dd8914..000000000 --- a/src/theory/rewriterules/rr_inst_match.h +++ /dev/null @@ -1,341 +0,0 @@ -/********************* */ -/*! \file rr_inst_match.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Francois Bobot - ** Minor contributors (to current version): Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief inst match class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H -#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H - -#include "theory/theory.h" -#include "util/hash.h" -#include "util/ntuple.h" - -#include -#include -#include - -#include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "context/cdlist.h" - -#include "theory/quantifiers/term_database.h" -#include "expr/node_manager.h" -#include "expr/node_builder.h" - -#include "theory/quantifiers/options.h" -#include "theory/rewriterules/options.h" - -//#define USE_EFFICIENT_E_MATCHING - -namespace CVC4 { -namespace theory { - -class EqualityQuery; - -namespace rrinst{ - -/** basic class defining an instantiation */ -class InstMatch { - /* map from variable to ground terms */ - std::map< Node, Node > d_map; -public: - InstMatch(); - InstMatch( InstMatch* m ); - - /** set the match of v to m */ - bool setMatch( EqualityQuery* q, TNode v, TNode m ); - /* This version tell if the variable has been set */ - bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set); - /** fill all unfilled values with m */ - bool add( InstMatch& m ); - /** if compatible, fill all unfilled values with m and return true - return false otherwise */ - bool merge( EqualityQuery* q, InstMatch& m ); - /** debug print method */ - void debugPrint( const char* c ); - /** is complete? */ - bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } - /** make complete */ - void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal representative */ - //void makeInternalRepresentative( QuantifiersEngine* qe ); - /** make representative */ - void makeRepresentative( QuantifiersEngine* qe ); - /** get value */ - Node getValue( Node var ) const; - /** clear */ - void clear(){ d_map.clear(); } - /** is_empty */ - bool empty(){ return d_map.empty(); } - /** to stream */ - inline void toStream(std::ostream& out) const { - out << "INST_MATCH( "; - for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it != d_map.begin() ){ out << ", "; } - out << it->first << " -> " << it->second; - } - out << " )"; - } - - - //for rewrite rules - - /** apply rewrite */ - void applyRewrite(); - /** erase */ - template - void erase(Iterator begin, Iterator end){ - for(Iterator i = begin; i != end; ++i){ - d_map.erase(*i); - }; - } - void erase(Node node){ d_map.erase(node); } - /** get */ - Node get( TNode var ) { return d_map[var]; } - Node get( QuantifiersEngine* qe, Node f, int i ); - /** set */ - void set(TNode var, TNode n); - void set( QuantifiersEngine* qe, Node f, int i, TNode n ); - /** size */ - size_t size(){ return d_map.size(); } - /* iterator */ - std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; - std::map< Node, Node >::iterator end(){ return d_map.end(); }; - std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); }; - /* Node used for matching the trigger only for mono-trigger (just for - efficiency because I need only that) */ - Node d_matched; -};/* class InstMatch */ - - - -class CandidateGenerator -{ -public: - CandidateGenerator(){} - virtual ~CandidateGenerator(){}; - - /** Get candidates functions. These set up a context to get all match candidates. - cg->reset( eqc ); - do{ - Node cand = cg->getNextCandidate(); - //....... - }while( !cand.isNull() ); - - eqc is the equivalence class you are searching in - */ - virtual void reset( TNode eqc ) = 0; - virtual TNode getNextCandidate() = 0; - /** call this at the beginning of each instantiation round */ - virtual void resetInstantiationRound() = 0; -public: - /** legal candidate */ - static inline bool isLegalCandidate( TNode n ){ - return !n.getAttribute(NoMatchAttribute()) && - ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n)) && - ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) ); -} - -}; - - -inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { - m.toStream(out); - return out; -} - -template class InstMatchTrie2; -template class InstMatchTrie2Pairs; - -template -class InstMatchTrie2Gen -{ - friend class InstMatchTrie2; - friend class InstMatchTrie2Pairs; - -private: - - class Tree { - public: - typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel; - MLevel e; - const size_t level; //context level of creation - Tree() CVC4_UNDEFINED; - const Tree & operator =(const Tree & t){ - Assert(t.e.empty()); Assert(e.empty()); - Assert(t.level == level); - return t; - } - Tree(size_t l): level(l) {}; - ~Tree(){ - for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i) - delete(i->second); - }; - }; - - - typedef std::pair Mod; - - class CleanUp{ - public: - inline void operator()(Mod * m){ - typename Tree::MLevel::iterator i = m->first->e.find(m->second); - Assert (i != m->first->e.end()); //should not have been already removed - m->first->e.erase(i); - }; - }; - - EqualityQuery* d_eQ; - CandidateGenerator * d_cG; - - context::Context* d_context; - context::CDList > d_mods; - - - typedef std::map::const_iterator mapIter; - - /** add the substitution given by the iterator*/ - void addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel); - /** test if it exists match, modulo uf-equations if modEq is true if - * return false the deepest point of divergence is put in [e] and - * [diverge]. - */ - bool existsInstMatch( Tree * root, - mapIter & current, mapIter & end, - Tree * & e, mapIter & diverge) const; - - /** add match m in the trie root - return true if it was never seen */ - bool addInstMatch( InstMatch& m, Tree * root); - -public: - InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* q); - InstMatchTrie2Gen(const InstMatchTrie2Gen &) CVC4_UNDEFINED; - const InstMatchTrie2Gen & operator =(const InstMatchTrie2Gen & e) CVC4_UNDEFINED; -}; - -template -class InstMatchTrie2 -{ - typename InstMatchTrie2Gen::Tree d_data; - InstMatchTrie2Gen d_backtrack; -public: - InstMatchTrie2(context::Context* c, QuantifiersEngine* q): d_data(0), - d_backtrack(c,q) {}; - InstMatchTrie2(const InstMatchTrie2 &) CVC4_UNDEFINED; - const InstMatchTrie2 & operator =(const InstMatchTrie2 & e) CVC4_UNDEFINED; - /** add match m in the trie, - return true if it was never seen */ - inline bool addInstMatch( InstMatch& m){ - return d_backtrack.addInstMatch(m,&d_data); - }; - -};/* class InstMatchTrie2 */ - -class Matcher -{ -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; - /** reset the term to match, return false if there is no such term */ - virtual bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ) = 0; - /** get the next match. If it return false once you shouldn't call - getNextMatch again before doing a reset */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** If reset, or getNextMatch return false they remove from the - InstMatch the binding that they have previously created */ - - /** virtual Matcher in order to have defined behavior */ - virtual ~Matcher(){}; -}; - - -class ApplyMatcher: public Matcher{ -private: - /** What to check first: constant and variable */ - std::vector< triple< TNode,size_t,EqualityQuery* > > d_constants; - std::vector< triple< TNode,size_t,EqualityQuery* > > d_variables; - /** children generators, only the sub-pattern which are - neither a variable neither a constant appears */ - std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens; - /** the variable that have been set by this matcher (during its own reset) */ - std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */ - /** the representative of the argument of the term given by the last reset */ - std::vector< Node > d_reps; -public: - /** The pattern we are producing matches for */ - Node d_pattern; -public: - /** constructors */ - ApplyMatcher( Node pat, QuantifiersEngine* qe); - /** destructor */ - ~ApplyMatcher(){/*TODO delete dandling pointers? */} - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ); - /** reset the term to match */ - bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ); - /** get the next match. */ - bool getNextMatch(InstMatch& m, QuantifiersEngine* qe); -private: - bool getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset); -}; - - -/* Match literal so you don't choose the equivalence class( */ -class PatMatcher -{ -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; - /** reset the matcher, return false if there is no such term */ - virtual bool reset( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** get the next match. If it return false once you shouldn't call - getNextMatch again before doing a reset */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** If reset, or getNextMatch return false they remove from the - InstMatch the binding that they have previously created */ -}; - -Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ); -PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ); - -/* Match literal so you don't choose the equivalence class( */ -class PatsMatcher -{ -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; - /** reset the matcher, return false if there is no such term */ - virtual bool getNextMatch( QuantifiersEngine* qe ) = 0; - virtual const InstMatch& getInstMatch() = 0; - /** Add directly the instantiation to quantifiers engine */ - virtual int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe) = 0; -}; - -PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ); -PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ); - -/** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ -bool nonunifiable( TNode t, TNode pat, const std::vector & vars); - -class InstMatchGenerator; - -}/* CVC4::theory rrinst */ - -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */ diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h deleted file mode 100644 index c0dea3ba2..000000000 --- a/src/theory/rewriterules/rr_inst_match_impl.h +++ /dev/null @@ -1,126 +0,0 @@ -/********************* */ -/*! \file rr_inst_match_impl.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Francois Bobot - ** Minor contributors (to current version): Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief inst match class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H -#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H - -#include "theory/rewriterules/rr_inst_match.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "theory/rewriterules/rr_candidate_generator.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { -namespace rrinst { - -template -InstMatchTrie2Gen::InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* qe): - d_context(c), d_mods(c) { - d_eQ = qe->getEqualityQuery(); - d_cG = new GenericCandidateGeneratorClass(qe); -}; - -/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ -template -void InstMatchTrie2Gen::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) { - if( current == end ) return; - - Assert(root->e.find(current->second) == root->e.end()); - Tree * root2 = new Tree(currLevel); - root->e.insert(std::make_pair(current->second, root2)); - addSubTree(root2, ++current, end, currLevel ); -} - -/** exists match */ -template -bool InstMatchTrie2Gen::existsInstMatch(InstMatchTrie2Gen::Tree * root, - mapIter & current, mapIter & end, - Tree * & e, mapIter & diverge) const{ - if( current == end ) { - Debug("Trie2") << "Trie2 Bottom " << std::endl; - --current; - return true; - }; //Already their - - if (current->first > diverge->first){ - // this point is the deepest point currently seen map are ordered - e = root; - diverge = current; - }; - - TNode n = current->second; - typename InstMatchTrie2Gen::Tree::MLevel::iterator it = - root->e.find( n ); - if( it!=root->e.end() && - existsInstMatch( (*it).second, ++current, end, e, diverge) ){ - Debug("Trie2") << "Trie2 Directly here " << n << std::endl; - --current; - return true; - } - Assert( it==root->e.end() || e != root ); - - // Even if n is in the trie others of the equivalence class - // can also be in it since the equality can have appeared - // after they have been added - if( modEq && d_eQ->hasTerm( n ) ){ - //check modulo equality if any other instantiation match exists - d_cG->reset( d_eQ->getRepresentative( n ) ); - for(TNode en = d_cG->getNextCandidate() ; !en.isNull() ; - en = d_cG->getNextCandidate() ){ - if( en == n ) continue; // already tested - typename InstMatchTrie2Gen::Tree::MLevel::iterator itc = - root->e.find( en ); - if( itc!=root->e.end() && - existsInstMatch( (*itc).second, ++current, end, e, diverge) ){ - Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl; - --current; - return true; - } - Assert( itc==root->e.end() || e != root ); - } - } - --current; - return false; -} - -template -bool InstMatchTrie2Gen:: -addInstMatch( InstMatch& m, InstMatchTrie2Gen::Tree* e ) { - d_cG->resetInstantiationRound(); - mapIter begin = m.begin(); - mapIter end = m.end(); - mapIter diverge = begin; - if( !existsInstMatch(e, begin, end, e, diverge ) ){ - Assert(!diverge->second.isNull()); - size_t currLevel = d_context->getLevel(); - addSubTree( e, diverge, end, currLevel ); - if(e->level != currLevel) - //If same level that e, will be removed at the same time than e - d_mods.push_back(std::make_pair(e,diverge->second)); - return true; - }else{ - return false; - } -} - -}/* CVC4::theory::rrinst namespace */ - -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H */ diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp deleted file mode 100644 index 13250cf1b..000000000 --- a/src/theory/rewriterules/rr_trigger.cpp +++ /dev/null @@ -1,385 +0,0 @@ -/********************* */ -/*! \file rr_trigger.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds, Francois Bobot - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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 trigger class - **/ - -#include "theory/rewriterules/rr_trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "theory/rewriterules/rr_candidate_generator.h" -#include "theory/uf/equality_engine.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::rrinst; - -/** trigger class constructor */ -Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : -d_quantEngine( qe ), d_f( f ){ - d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); - Debug("trigger") << "Trigger for " << f << ": " << d_nodes << std::endl; - if(matchOption == MATCH_GEN_DEFAULT) d_mg = mkPatterns( d_nodes, qe ); - else d_mg = mkPatternsEfficient( d_nodes, qe ); - if( d_nodes.size()==1 ){ - if( isSimpleTrigger( d_nodes[0] ) ){ - ++(qe->d_statistics.d_triggers); - }else{ - ++(qe->d_statistics.d_simple_triggers); - } - }else{ - Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; - //std::cout << "Multi-trigger for " << f << " : " << std::endl; - //std::cout << " " << (*this) << std::endl; - ++(qe->d_statistics.d_multi_triggers); - } -} - -void Trigger::resetInstantiationRound(){ - d_mg->resetInstantiationRound( d_quantEngine ); -} - - -bool Trigger::getNextMatch(){ - bool retVal = d_mg->getNextMatch( d_quantEngine ); - //m.makeInternal( d_quantEngine->getEqualityQuery() ); - return retVal; -} - -// bool Trigger::getMatch( Node t, InstMatch& m ){ -// //FIXME: this assumes d_mg is an inst match generator -// return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); -// } - - -int Trigger::addInstantiations( InstMatch& baseMatch ){ - int addedLemmas = d_mg->addInstantiations( baseMatch, - quantifiers::TermDb::getInstConstAttr(d_nodes[0]), - d_quantEngine); - if( addedLemmas>0 ){ - Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; - for( int i=0; i<(int)d_nodes.size(); i++ ){ - Debug("inst-trigger") << d_nodes[i] << " "; - } - Debug("inst-trigger") << std::endl; - } - return addedLemmas; -} - -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, - bool smartTriggers ){ - std::vector< Node > trNodes; - if( !keepAll ){ - //only take nodes that contribute variables to the trigger when added - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::map< Node, bool > vars; - std::map< Node, std::vector< Node > > patterns; - for( int i=0; i<(int)temp.size(); i++ ){ - bool foundVar = false; - qe->getTermDatabase()->computeVarContains( temp[i] ); - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( quantifiers::TermDb::getInstConstAttr(v)==f ){ - if( vars.find( v )==vars.end() ){ - vars[ v ] = true; - foundVar = true; - } - } - } - if( foundVar ){ - trNodes.push_back( temp[i] ); - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - patterns[ v ].push_back( temp[i] ); - } - } - } - //now, minimalize the trigger - for( int i=0; i<(int)trNodes.size(); i++ ){ - bool keepPattern = false; - Node n = trNodes[i]; - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - if( patterns[v].size()==1 ){ - keepPattern = true; - break; - } - } - if( !keepPattern ){ - //remove from pattern vector - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - for( int k=0; k<(int)patterns[v].size(); k++ ){ - if( patterns[v][k]==n ){ - patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); - break; - } - } - } - //remove from trigger nodes - trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); - i--; - } - } - }else{ - trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); - } - - //check for duplicate? - if( trOption==TR_MAKE_NEW ){ - //static int trNew = 0; - //static int trOld = 0; - //Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); - //if( t ){ - // trOld++; - //}else{ - // trNew++; - //} - //if( (trNew+trOld)%100==0 ){ - // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; - //} - }else{ - Trigger* t = qe->getRRTriggerDatabase()->getTrigger( trNodes ); - if( t ){ - if( trOption==TR_GET_OLD ){ - //just return old trigger - return t; - }else{ - return NULL; - } - } - } - Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - qe->getRRTriggerDatabase()->addTrigger( trNodes, t ); - return t; -} -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ - std::vector< Node > nodes; - nodes.push_back( n ); - return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); -} - -bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ - for( int i=0; i<(int)nodes.size(); i++ ){ - if( !isUsableTrigger( nodes[i], f ) ){ - return false; - } - } - return true; -} - -bool Trigger::isUsable( Node n, Node f ){ - if( quantifiers::TermDb::getInstConstAttr(n)==f ){ - if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ - std::map< Node, Node > coeffs; - return getPatternArithmetic( f, n, coeffs ); - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isUsable( n[i], f ) ){ - return false; - } - } - return true; - } - }else{ - return true; - } -} - -bool Trigger::isSimpleTrigger( Node n ){ - if( isAtomicTrigger( n ) ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ - return false; - } - } - return true; - }else{ - return false; - } -} - - -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ - if( patMap.find( n )==patMap.end() ){ - patMap[ n ] = false; - if( tstrt==TS_MIN_TRIGGER ){ - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else - return false; -#endif - }else{ - bool retVal = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ - retVal = true; - } - } - if( retVal ){ - return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; - }else{ - return false; - } - } - }else{ - bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - if( tstrt==TS_MAX_TRIGGER ){ - return true; - }else{ - retVal = true; - } - } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ - retVal = true; - } - } - } - return retVal; - } - }else{ - return patMap[ n ]; - } -} - -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ - std::map< Node, bool > patMap; - if( filterInst ){ - //immediately do not consider any term t for which another term is an instance of t - std::vector< Node > patTerms2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); - std::vector< Node > temp; - temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - qe->getTermDatabase()->filterInstances( temp ); - if( temp.size()!=patTerms2.size() ){ - Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; - Debug("trigger-filter-instance") << "Old: "; - for( int i=0; i<(int)patTerms2.size(); i++ ){ - Debug("trigger-filter-instance") << patTerms2[i] << " "; - } - Debug("trigger-filter-instance") << std::endl << "New: "; - for( int i=0; i<(int)temp.size(); i++ ){ - Debug("trigger-filter-instance") << temp[i] << " "; - } - Debug("trigger-filter-instance") << std::endl; - } - if( tstrt==TS_ALL ){ - patTerms.insert( patTerms.begin(), temp.begin(), temp.end() ); - return; - }else{ - //do not consider terms that have instances - for( int i=0; i<(int)patTerms2.size(); i++ ){ - if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){ - patMap[ patTerms2[i] ] = false; - } - } - } - } - collectPatTerms2( qe, f, n, patMap, tstrt ); - for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ - if( it->second ){ - patTerms.push_back( it->first ); - } - } -} - -bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ - if( n.getKind()==PLUS ){ - Assert( coeffs.empty() ); - NodeBuilder<> t(kind::PLUS); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ - if( n[i].getKind()==INST_CONSTANT ){ - if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ - coeffs[ n[i] ] = Node::null(); - }else{ - coeffs.clear(); - return false; - } - }else if( !getPatternArithmetic( f, n[i], coeffs ) ){ - coeffs.clear(); - return false; - } - }else{ - t << n[i]; - } - } - if( t.getNumChildren()==0 ){ - coeffs[ Node::null() ] = NodeManager::currentNM()->mkConst( Rational(0) ); - }else if( t.getNumChildren()==1 ){ - coeffs[ Node::null() ] = t.getChild( 0 ); - }else{ - coeffs[ Node::null() ] = t; - } - return true; - }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ - Assert( !quantifiers::TermDb::hasInstConstAttr(n[1]) ); - coeffs[ n[0] ] = n[1]; - return true; - }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ - Assert( !quantifiers::TermDb::hasInstConstAttr(n[0]) ); - coeffs[ n[1] ] = n[0]; - return true; - } - } - return false; -} - - - -Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ - if( nodes.empty() ){ - return d_tr; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )!=d_children.end() ){ - return d_children[n]->getTrigger2( nodes ); - }else{ - return NULL; - } - } -} -void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ - if( nodes.empty() ){ - d_tr = t; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )==d_children.end() ){ - d_children[n] = new TriggerTrie; - } - d_children[n]->addTrigger2( nodes, t ); - } -} diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h deleted file mode 100644 index f02f38d0e..000000000 --- a/src/theory/rewriterules/rr_trigger.h +++ /dev/null @@ -1,157 +0,0 @@ -/********************* */ -/*! \file rr_trigger.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds, Francois Bobot - ** Minor contributors (to current version): Tianyi Liang - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief trigger class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H -#define __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H - -#include "theory/rewriterules/rr_inst_match.h" - -namespace CVC4 { -namespace theory { -namespace rrinst { - -//a collect of nodes representing a trigger -class Trigger { -private: - /** the quantifiers engine */ - QuantifiersEngine* d_quantEngine; - /** the quantifier this trigger is for */ - Node d_f; - /** match generators */ - PatsMatcher * d_mg; -private: - /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false ); -public: - ~Trigger(){} -public: - std::vector< Node > d_nodes; -public: - void debugPrint( const char* c ); - PatsMatcher* getGenerator() { return d_mg; } -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound(); - /** get next match. must call reset( eqc ) once before this function. */ - bool getNextMatch(); - const InstMatch & getInstMatch(){return d_mg->getInstMatch();}; - /** return whether this is a multi-trigger */ - bool isMultiTrigger() { return d_nodes.size()>1; } -public: - /** add all available instantiations exhaustively, in any equivalence class - if limitInst>0, limitInst is the max # of instantiations to try */ - int addInstantiations( InstMatch& baseMatch); - /** mkTrigger method - ie : quantifier engine; - f : forall something .... - nodes : (multi-)trigger - matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* ) - keepAll: don't remove unneeded patterns; - trOption : policy for dealing with triggers that already existed (see below) - */ - enum { - //options for producing matches - MATCH_GEN_DEFAULT = 0, - MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E - }; - enum{ - TR_MAKE_NEW, //make new trigger even if it already may exist - TR_GET_OLD, //return a previous trigger if it had already been created - TR_RETURN_NULL //return null if a duplicate is found - }; - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, - int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, - bool smartTriggers = false ); - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, - int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, - bool smartTriggers = false ); -private: - /** is subterm of trigger usable */ - static bool isUsable( Node n, Node f ); - /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ); -public: - //different strategies for choosing trigger terms - enum { - TS_MAX_TRIGGER = 0, - TS_MIN_TRIGGER, - TS_ALL, - }; - static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false ); -public: - /** is usable trigger */ - static inline bool isUsableTrigger( TNode n, TNode f ){ - return quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - } - static inline bool isAtomicTrigger( TNode n ){ - return - n.getKind()==kind::APPLY_UF || - n.getKind() == kind::APPLY_CONSTRUCTOR || - n.getKind()==kind::SELECT || - n.getKind()==kind::STORE; - } - static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); - static bool isSimpleTrigger( Node n ); - /** get pattern arithmetic */ - static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); - - inline void toStream(std::ostream& out) const { - out << "TRIGGER( "; - for( int i=0; i<(int)d_nodes.size(); i++ ){ - if( i>0 ){ out << ", "; } - out << d_nodes[i]; - } - out << " )"; - } -}; - -inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { - tr.toStream(out); - return out; -} - -/** a trie of triggers */ -class TriggerTrie -{ -private: - Trigger* getTrigger2( std::vector< Node >& nodes ); - void addTrigger2( std::vector< Node >& nodes, Trigger* t ); -public: - TriggerTrie() : d_tr( NULL ){} - Trigger* d_tr; - std::map< Node, TriggerTrie* > d_children; - Trigger* getTrigger( std::vector< Node >& nodes ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return getTrigger2( temp ); - } - void addTrigger( std::vector< Node >& nodes, Trigger* t ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return addTrigger2( temp, t ); - } -}; - - -}/* CVC4::theory::rrinst namespace */ - -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H */ diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp deleted file mode 100644 index 37187e684..000000000 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Francois Bobot - ** Minor contributors (to current version): Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Deals with rewrite rules ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/rewriterules/theory_rewriterules.h" -#include "theory/rewriter.h" - - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::rewriterules; -using namespace CVC4::theory::rrinst; - - -namespace CVC4 { -namespace theory { -namespace rewriterules { - - -TheoryRewriteRules::TheoryRewriteRules(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo) : - Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo) -{ - -} - -void TheoryRewriteRules::check(Effort level) { - CodeTimer codeTimer(d_theoryTime); - - while(!done()) { - // Get all the assertions - // TODO: Test that it have already been ppAsserted - - //if we are here and ppAssert has not been done - // that means that ppAssert is off so we need to assert now - Assertion assertion = get(); - // Assertion assertion = get(); - // TNode fact = assertion.assertion; - - // Debug("rewriterules") << "TheoryRewriteRules::check(): processing " << fact << std::endl; - // if (getValuation().getDecisionLevel()>0) - // Unhandled(getValuation().getDecisionLevel()); - // addRewriteRule(fact); - - } -}; - -Node TheoryRewriteRules::explain(TNode n){ - - return Node::null(); -} - -void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){ - -} - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h deleted file mode 100644 index 85cd9a85c..000000000 --- a/src/theory/rewriterules/theory_rewriterules.h +++ /dev/null @@ -1,62 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Andrew Reynolds, Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Rewrite Engine classes - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H - -#include "context/cdlist.h" -#include "context/cdqueue.h" -#include "theory/valuation.h" -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "context/context_mm.h" -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -class TheoryRewriteRules : public Theory { -private: - - KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime"); - public: - /** Constructs a new instance of TheoryRewriteRules - w.r.t. the provided context.*/ - TheoryRewriteRules(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo); - - /** Usual function for theories */ - void check(Theory::Effort e); - Node explain(TNode n); - void collectModelInfo( TheoryModel* m, bool fullModel ); - void notifyEq(TNode lhs, TNode rhs); - std::string identify() const { - return "THEORY_REWRITERULES"; - } - -};/* class TheoryRewriteRules */ - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h deleted file mode 100644 index e20556ef3..000000000 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_params.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Parameters for the rewrite rules theory - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -/** - Specify if the propagation is done by lemma or by real theory propagation - */ -static const bool propagate_as_lemma = true; - -/** - Cache the instantiation of rules in order to remove duplicate - */ -static const bool cache_match = true; - -/** - Compute when the rules are created which terms in the body can lead - to new instantiation (try only single trigger). During propagation - we check if the instantiation of these terms are known terms. - */ -static const bool compute_opt = true; - -/** - rewrite the matching found - */ -static const bool rewrite_instantiation = true; - -/** - use the representative for the matching found - */ -static const bool representative_instantiation = false; - -/** - Wait the specified number of check after a new propagation (a - previous unknown guards becomes true) is found before verifying again the guards. - - Allow to break loop with other theories. - */ -static const size_t checkSlowdown = 0; - -/** - Use the current model to eliminate guard before asking for notification - */ -static const bool useCurrentModel = false; - -/** - Simulate rewriting by tagging rewritten terms. - */ -static const bool simulateRewritting = true; - -/** - Do narrowing at full effort -*/ -static const bool narrowing_full_effort = false; - -/** - Direct rewrite: Add rewrite rules directly in the rewriter. - */ -static const bool direct_rewrite = false; - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h deleted file mode 100644 index cc24357c6..000000000 --- a/src/theory/rewriterules/theory_rewriterules_preprocess.h +++ /dev/null @@ -1,176 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_preprocess.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief One utilitise for rewriterules definition - ** - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H - -#include -#include -#include -#include "expr/expr.h" -#include "expr/node.h" -#include "theory/rewriterules/theory_rewriterules_params.h" -#include "theory/uf/theory_uf.h" - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -namespace rewriter { - - typedef Node TMPNode; - typedef std::vector Subst; - typedef std::vector ESubst; - typedef std::vector TSubst; - - struct Step{ - - /** match the node and add in Vars the found variables */ - virtual Node run(TMPNode node) = 0; - virtual bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars) = 0; - };/* struct Step */ - - struct FinalStep : Step { - Node body; - TSubst vars; - - Node subst(Subst & subst){ - return body.substitute(vars.begin(), vars.end(), - subst.begin(), subst.end()); - } - - };/* struct FinalStep */ - - typedef std::hash_map< Node, int, NodeHashFunction > PVars; - - struct Pattern : FinalStep{ - Node pattern; - PVars pattern_vars; - - Node run(TMPNode node){ - Subst vars = Subst(pattern_vars.size(),Node::null()); - - typedef std::vector > tstack; - tstack stack(1,std::make_pair(node,pattern)); // t * pat - - while(!stack.empty()){ - const std::pair p = stack.back(); stack.pop_back(); - const TMPNode & t = p.first; - const TMPNode & pat = p.second; - - // pat is a variable - if( pat.getKind() == kind::INST_CONSTANT || - pat.getKind() == kind::VARIABLE){ - PVars::iterator i = pattern_vars.find(pat); - Assert(i != pattern_vars.end()); - if(vars[i->second].isNull()) vars[i->second] = t; - if(vars[i->second] == t) continue; - return Node::null(); - }; - - // t is not an UF application - if( t.getKind() != kind::APPLY_UF ){ - if (t == pat) continue; - else return Node::null(); - }; - - //different UF_application - if( t.getOperator() != pat.getOperator() ) return Node::null(); - - //put the children on the stack - for( size_t i=0; i < pat.getNumChildren(); i++ ){ - stack.push_back(std::make_pair(t[i],pat[i])); - }; - } - - // Matching is done - return subst(vars); - } - - bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars){ - return false; - } - - };/* struct Pattern */ - - - struct Args : Step { - typedef std::vector Patterns; - Patterns d_matches; - - Node run(TMPNode node){ - Node n; - for (Patterns::iterator i = d_matches.begin(); - i != d_matches.end() && n.isNull(); ++i){ - Debug("rewriterules-rewrite") << "test?" << i->pattern << std::endl; - n = i->run(node); - } - return n; - } - - bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars){ - Debug("rewriterules-rewrite") << "theoryrewrite::Args::add" << "(" - << d_matches.size() << ")" - << pattern << "->" << body << std::endl; - d_matches.push_back(Pattern()); - Pattern & p = d_matches.back(); - p.body = body; - p.vars.reserve(vars.size()); - for( size_t i=0; i < vars.size(); i++ ){ - p.vars.push_back(vars[i]); - }; - p.pattern = pattern; - for( size_t i=0; i < pvars.size(); i++ ){ - p.pattern_vars[pvars[i]] = i; - }; - return true; - }; - - void clear(){ - d_matches.clear(); - } - };/* struct Args */ - -class RRPpRewrite : public uf::TheoryUF::PpRewrite { - Args d_pattern; -public: - Node ppRewrite(TNode node){ - Debug("rewriterules-rewrite") << "rewrite?" << node << std::endl; - Node t = d_pattern.run(node); - Debug("rewriterules-rewrite") << "rewrite:" << node - << (t.isNull()? " to": " to ") - << t << std::endl; - if (t.isNull()) return node; - else return t; - } - - bool addRewritePattern(TMPNode pattern, TMPNode body, - Subst & pvars, Subst & vars){ - return d_pattern.add(pattern,body,pvars,vars); - } - -};/* class RRPpRewrite */ - - - -}/* CVC4::theory::rewriterules::rewriter namespace */ - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h deleted file mode 100644 index 511ef3515..000000000 --- a/src/theory/rewriterules/theory_rewriterules_rewriter.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_rewriter.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H - -#include "theory/rewriter.h" -#include "theory/rewriter_attributes.h" - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -class TheoryRewriterulesRewriter { -public: - - /** - * Rewrite a node into the normal form for the theory of rewriterules. - * Called in post-order (really reverse-topological order) when - * traversing the expression DAG during rewriting. This is the - * main function of the rewriter, and because of the ordering, - * it can assume its children are all rewritten already. - * - * This function can return one of three rewrite response codes - * along with the rewritten node: - * - * REWRITE_DONE indicates that no more rewriting is needed. - * REWRITE_AGAIN means that the top-level expression should be - * rewritten again, but that its children are in final form. - * REWRITE_AGAIN_FULL means that the entire returned expression - * should be rewritten again (top-down with preRewrite(), then - * bottom-up with postRewrite()). - * - * Even if this function returns REWRITE_DONE, if the returned - * expression belongs to a different theory, it will be fully - * rewritten by that theory's rewriter. - */ - static RewriteResponse postRewrite(TNode node) { - - // Implement me! - - // This default implementation - return RewriteResponse(REWRITE_DONE, node); - } - - /** - * Rewrite a node into the normal form for the theory of rewriterules - * in pre-order (really topological order)---meaning that the - * children may not be in the normal form. This is an optimization - * for theories with cancelling terms (e.g., 0 * (big-nasty-expression) - * in arithmetic rewrites to 0 without the need to look at the big - * nasty expression). Since it's only an optimization, the - * implementation here can do nothing. - */ - static RewriteResponse preRewrite(TNode node) { - // do nothing - return RewriteResponse(REWRITE_DONE, node); - } - - /** - * Initialize the rewriter. - */ - static inline void init() { - // nothing to do - } - - /** - * Shut down the rewriter. - */ - static inline void shutdown() { - // nothing to do - } - -};/* class TheoryRewriterulesRewriter */ - -}/* CVC4::theory::rewriterules namespace */ - -template<> -struct RewriteAttibute { - static Node getPreRewriteCache(TNode node) throw() { - return node; - } - - static void setPreRewriteCache(TNode node, TNode cache) throw() { } - - static Node getPostRewriteCache(TNode node) throw() { - return node; - } - - static void setPostRewriteCache(TNode node, TNode cache) throw() { } - - typedef expr::Attribute< RewriteCacheTag, Node> pre_rewrite; - typedef expr::Attribute< RewriteCacheTag, Node> post_rewrite; -}; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp deleted file mode 100644 index 38e22ed64..000000000 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ /dev/null @@ -1,403 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_rules.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Francois Bobot - ** Minor contributors (to current version): Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Deals with rewrite rules ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/rewriterules/theory_rewriterules_rules.h" -#include "theory/rewriterules/theory_rewriterules_params.h" -#include "theory/rewriterules/theory_rewriterules_preprocess.h" -#include "theory/rewriterules/theory_rewriterules.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::rewriterules; -using namespace CVC4::theory::rrinst; - - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -// TODO replace by a real dictionnary -// We should create a real substitution? slower more precise -// We don't do that often -bool nonunifiable( TNode t0, TNode pattern, const std::vector & vars){ - typedef std::vector > tstack; - tstack stack(1,std::make_pair(t0,pattern)); // t * pat - - while(!stack.empty()){ - const std::pair p = stack.back(); stack.pop_back(); - const TNode & t = p.first; - const TNode & pat = p.second; - - // t or pat is a variable currently we consider that can match anything - if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; - if( pat.getKind() == INST_CONSTANT ) continue; - - // t and pat are nonunifiable - if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { - if(t == pat) continue; - else return true; - }; - if( t.getOperator() != pat.getOperator() ) return true; - - //put the children on the stack - for( size_t i=0; i < pat.getNumChildren(); i++ ){ - stack.push_back(std::make_pair(t[i],pat[i])); - }; - } - // The heuristic can't find non-unifiability - return false; -} - - -void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule, - size_t start){ - std::vector stack(1,rule->new_terms); - - while(!stack.empty()){ - Node t = stack.back(); stack.pop_back(); - - // We don't want to consider variable in t - if( std::find(rule->free_vars.begin(), rule->free_vars.end(), t) - != rule->free_vars.end()) continue; - // t we want to consider only UF function - if( t.getKind() == APPLY_UF ){ - for(size_t rid = start, end = d_rules.size(); rid < end; ++rid) { - RewriteRule * r = d_rules[rid]; - if(r->d_split || r->trigger_for_body_match == NULL) continue; - //the split rules are not computed and the one with multi-pattern - if( !nonunifiable(t, r->trigger_for_body_match->d_pattern, rule->free_vars)){ - rule->body_match.push_back(std::make_pair(t,r)); - } - } - } - - //put the children on the stack - for( size_t i=0; i < t.getNumChildren(); i++ ){ - stack.push_back(t[i]); - }; - - } -} - -inline void addPattern(TheoryRewriteRules & re, - TNode tri, - std::vector & pattern, - std::vector & vars, - std::vector & inst_constants, - TNode r){ - if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF) - tri = tri[0]; - pattern.push_back( - options::rewriteRulesAsAxioms()? - static_cast(tri): - re.getQuantifiersEngine()->getTermDatabase()-> - convertNodeToPattern(tri,r,vars,inst_constants)); -} - -/*** Check that triggers contains all the variables */ -void checkPatternVarsAux(TNode pat,const std::vector & vars, - std::vector & seen){ - for(size_t id=0;id < vars.size(); ++id){ - if(pat == vars[id]){ - seen[id]=true; - break; - }; - }; - for(Node::iterator i = pat.begin(); i != pat.end(); ++i) { - checkPatternVarsAux(*i,vars,seen); - }; -} - -bool checkPatternVars(const std::vector & pattern, - const std::vector & vars){ - std::vector seen(vars.size(),false); - for(std::vector::const_iterator i = pattern.begin(); - i != pattern.end(); ++i) { - checkPatternVarsAux(*i,vars,seen); - }; - return (find(seen.begin(),seen.end(),false) == seen.end()); -} - -/** Main function for construction of RewriteRule */ -void TheoryRewriteRules::addRewriteRule(const Node r) -{ - Assert(r.getKind() == kind::REWRITE_RULE); - Kind rrkind = r[2].getKind(); - /* Replace variables by Inst_* variable and tag the terms that - contain them */ - std::vector vars; - vars.reserve(r[0].getNumChildren()); - for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){ - vars.push_back(*v); - }; - /* Instantiation version */ - std::vector inst_constants = createInstVariable(r,vars); - /* Body/Remove_term/Guards/Triggers */ - Node body = r[2][1]; - TNode new_terms = r[2][1]; - std::vector guards; - std::vector pattern; - std::vector to_remove; /* "remove" the terms from the database - when fired */ - /* shortcut */ - TNode head = r[2][0]; - TypeNode booleanType = NodeManager::currentNM()->booleanType(); - switch(rrkind){ - case kind::RR_REWRITE: - /* Equality */ - to_remove.push_back(head); - addPattern(*this,head,pattern,vars,inst_constants,r); - if(head.getType(false) == booleanType) body = head.iffNode(body); - else body = head.eqNode(body); - break; - case kind::RR_REDUCTION: - /** Add head to remove */ - for(Node::iterator i = head.begin(); i != head.end(); ++i) { - to_remove.push_back(*i); - }; - case kind::RR_DEDUCTION: - /** Add head to guards and pattern */ - switch(head.getKind()){ - case kind::AND: - guards.reserve(head.getNumChildren()); - for(Node::iterator i = head.begin(); i != head.end(); ++i) { - guards.push_back(*i); - addPattern(*this,*i,pattern,vars,inst_constants,r); - }; - break; - default: - if (head != d_true){ - guards.push_back(head); - addPattern(*this,head,pattern,vars,inst_constants,r); - }; - /** otherwise guards is empty */ - }; - break; - default: - Unreachable("RewriteRules can be of only three kinds"); - }; - /* Add the other guards */ - TNode g = r[1]; - switch(g.getKind()){ - case kind::AND: - guards.reserve(g.getNumChildren()); - for(Node::iterator i = g.begin(); i != g.end(); ++i) { - guards.push_back(*i); - }; - break; - default: - if (g != d_true) guards.push_back(g); - /** otherwise guards is empty */ - }; - /* Add the other triggers */ - if( r[2].getNumChildren() >= 3 ) - for(Node::iterator i = r[2][2][0].begin(); i != r[2][2][0].end(); ++i) { - // todo test during typing that its a good term (no not, atom, or term...) - addPattern(*this,*i,pattern,vars,inst_constants,r); - }; - // Assert(pattern.size() == 1, "currently only single pattern are supported"); - - - - - //If we convert to usual axioms - if(options::rewriteRulesAsAxioms()){ - NodeBuilder<> forallB(kind::FORALL); - forallB << r[0]; - NodeBuilder<> guardsB(kind::AND); - guardsB.append(guards); - forallB << normalizeConjunction(guardsB).impNode(body); - NodeBuilder<> patternB(kind::INST_PATTERN); - patternB.append(pattern); - NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); - patternListB << static_cast(patternB); - forallB << static_cast(patternListB); - Node lem = (Node) forallB; - lem = Rewriter::rewrite(lem); - QRewriteRuleAttribute qra; - lem.setAttribute(qra,r); - getOutputChannel().lemma(lem); - return; - } - - //turn all to propagate - // if(true){ - // NodeBuilder<> guardsB(kind::AND); - // guardsB.append(guards); - // body = normalizeConjunction(guardsB).impNode(body); - // guards.clear(); - // rrkind = kind::RR_DEDUCTION; - // } - - - //Every variable must be seen in the pattern - if (!checkPatternVars(pattern,inst_constants)){ - Warning() << Node::setdepth(-1) << "The rule" << r << - " has been removed since it doesn't contain every variables." - << std::endl; - return; - } - - - //Add to direct rewrite rule - bool directrr = false; - if(direct_rewrite && - guards.size() == 0 && rrkind == kind::RR_REWRITE - && pattern.size() == 1){ - directrr = addRewritePattern(pattern[0],new_terms, inst_constants, vars); - } - - - // final construction - Trigger trigger = createTrigger(r,pattern); - ApplyMatcher * applymatcher = - pattern.size() == 1 && pattern[0].getKind() == kind::APPLY_UF? - new ApplyMatcher(pattern[0],getQuantifiersEngine()) : NULL; - RewriteRule * rr = new RewriteRule(*this, trigger, applymatcher, - guards, body, new_terms, - vars, inst_constants, to_remove, - directrr); - /** other -> rr */ - if(compute_opt && !rr->d_split) computeMatchBody(rr); - d_rules.push_back(rr); - /** rr -> all (including himself) */ - if(compute_opt && !rr->d_split) - for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) - computeMatchBody(d_rules[rid], - d_rules.size() - 1); - - Debug("rewriterules::new") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")" - << *rr << std::endl; - -} - - -bool willDecide(TNode node, bool positive = true){ - /* TODO something better */ - switch(node.getKind()) { - case AND: - return !positive; - case OR: - return positive; - case IFF: - return true; - case XOR: - return true; - case IMPLIES: - return true; - case ITE: - return true; - case NOT: - return willDecide(node[0],!positive); - default: - return false; - } -} - -static size_t id_next = 0; -RewriteRule::RewriteRule(TheoryRewriteRules & re, - Trigger & tr, ApplyMatcher * applymatcher, - std::vector & g, Node b, TNode nt, - std::vector & fv,std::vector & iv, - std::vector & to_r, bool drr) : - id(++id_next), d_split(willDecide(b)), - trigger(tr), body(b), new_terms(nt), free_vars(), inst_vars(), - body_match(re.getSatContext()),trigger_for_body_match(applymatcher), - d_cache(re.getSatContext(),re.getQuantifiersEngine()), directrr(drr){ - free_vars.swap(fv); inst_vars.swap(iv); guards.swap(g); to_remove.swap(to_r); -}; - - -bool RewriteRule::inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const{ - bool res = !d_cache.addInstMatch(im); - Debug("rewriterules::matching") << "rewriterules::cache " << im - << (res ? " HIT" : " MISS") << std::endl; - return res; -}; - -/** A rewrite rule */ -void RewriteRule::toStream(std::ostream& out) const{ - out << "[" << id << "] "; - for(std::vector::const_iterator - iter = guards.begin(); iter != guards.end(); ++iter){ - out << *iter; - }; - out << "=>" << body << std::endl; - out << "{"; - for(BodyMatch::const_iterator - iter = body_match.begin(); iter != body_match.end(); ++iter){ - out << (*iter).first << "[" << (*iter).second->id << "]" << ","; - }; - out << "}" << (directrr?"*":"") << std::endl; -} - -RewriteRule::~RewriteRule(){ - Debug("rewriterule::stats") << *this - << " (" << nb_matched - << "," << nb_applied - << "," << nb_propagated - << ")" << std::endl; - delete(trigger_for_body_match); -} - -bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, - rewriter::Subst & pvars, - rewriter::Subst & vars){ - Assert(pattern.getKind() == kind::APPLY_UF); - TNode op = pattern.getOperator(); - TheoryRewriteRules::RegisterRRPpRewrite::iterator i = - d_registeredRRPpRewrite.find(op); - - rewriter::RRPpRewrite * p; - if (i == d_registeredRRPpRewrite.end()){ - p = new rewriter::RRPpRewrite(); - d_registeredRRPpRewrite.insert(std::make_pair(op,p)); - ((uf::TheoryUF*)getQuantifiersEngine()->getTheoryEngine()->theoryOf( THEORY_UF ))-> - registerPpRewrite(op,p); - } else p = i->second; - - return p->addRewritePattern(pattern,body,pvars,vars); - -} - -std::vector TheoryRewriteRules::createInstVariable( Node r, std::vector & vars ){ - std::vector inst_constant; - inst_constant.reserve(vars.size()); - for( std::vector::const_iterator v = vars.begin(); - v != vars.end(); ++v ){ - //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() ); - inst_constant.push_back( ic ); - InstConstantAttribute ica; - ic.setAttribute(ica,r); - //also set the no-match attribute - NoMatchAttribute nma; - ic.setAttribute(nma,true); - }; - return inst_constant; -} - - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h deleted file mode 100644 index 308194667..000000000 --- a/src/theory/rewriterules/theory_rewriterules_rules.h +++ /dev/null @@ -1,37 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_rules.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Rewrite Engine classes - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H - -#include "theory/rewriterules/theory_rewriterules.h" -#include "theory/rewriterules/theory_rewriterules_params.h" - -namespace CVC4 { -namespace theory { -namespace rewriterules { - -inline std::ostream& operator <<(std::ostream& stream, const RewriteRule& r) { - r.toStream(stream); - return stream; -} - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h deleted file mode 100644 index 28b10f91f..000000000 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ /dev/null @@ -1,35 +0,0 @@ -/********************* */ -/*! \file theory_rewriterules_type_rules.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H -#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H - -#include "node_manager.h" - -namespace CVC4 { -namespace theory { -namespace rewriterules { - - - -}/* CVC4::theory::rewriterules namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 45c9402ab..33ff18126 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1639,22 +1639,20 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { void TheoryEngine::checkTheoryAssertionsWithModel() { for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - if(theoryId != THEORY_REWRITERULES) { - Theory* theory = d_theoryTable[theoryId]; - if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { - for(context::CDList::const_iterator it = theory->facts_begin(), - it_end = theory->facts_end(); - it != it_end; - ++it) { - Node assertion = (*it).assertion; - Node val = getModel()->getValue(assertion); - if(val != d_true) { - stringstream ss; - ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; - InternalError(ss.str()); - } + Theory* theory = d_theoryTable[theoryId]; + if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { + for(context::CDList::const_iterator it = theory->facts_begin(), + it_end = theory->facts_end(); + it != it_end; + ++it) { + Node assertion = (*it).assertion; + Node val = getModel()->getValue(assertion); + if(val != d_true) { + stringstream ss; + ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl + << "The fact: " << assertion << endl + << "Model value: " << val << endl; + InternalError(ss.str()); } } } -- 2.30.2