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
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 \
theory/strings/kinds \
theory/arrays/kinds \
theory/quantifiers/kinds \
- theory/rewriterules/kinds \
theory/arith/kinds \
theory/booleans/kinds \
theory/example/ecdata.h \
../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 \
../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 \
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)
case theory::THEORY_BUILTIN:
case theory::THEORY_BOOL:
case theory::THEORY_QUANTIFIERS:
- case theory::THEORY_REWRITERULES:
return false;
default:
return true;
/** 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? */
*/
void enableQuantifiers() {
enableTheory(theory::THEORY_QUANTIFIERS);
- enableTheory(theory::THEORY_REWRITERULES);
}
/**
*/
void disableQuantifiers() {
disableTheory(theory::THEORY_QUANTIFIERS);
- disableTheory(theory::THEORY_REWRITERULES);
}
// these are for arithmetic
#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;
+++ /dev/null
-/********************* */
-/*! \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<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool>
- p = h.insert(make_pair(op,SetNode()));
- is = p.first;
- if(d_cand_gens.find(op) != d_cand_gens.end()){
- is->second.insert(*i);
- } /* else we have inserted an empty set */
- }else if(!is->second.empty()){
- is->second.insert(*i);
- }
- }
- if( !d_cand_gen_types.empty() ){
- //type
- TypeNode ty = i->getType();
- std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator
- is = tyh.find(ty);
- if(is == tyh.end()){
- std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool>
- p = tyh.insert(make_pair(ty,SetNode()));
- is = p.first;
- if(d_cand_gen_types.find(ty) != d_cand_gen_types.end()){
- is->second.insert(*i);
- } /* else we have inserted an empty set */
- }else if(!is->second.empty()){
- is->second.insert(*i);
- }
- }
- }
- //op
- for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end();
- i != end; ++i){
- //new term, add n to candidate generators
- if(i->second.empty()) continue;
- std::map< Node, NodeNewTermDispatcher >::iterator
- inpc = d_cand_gens.find(i->first);
- //we know that this op exists
- Assert(inpc != d_cand_gens.end());
- inpc->second.send(i->second);
- }
- //type
- for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end();
- i != end; ++i){
- //new term, add n to candidate generators
- if(i->second.empty()) continue;
- std::map< TypeNode, NodeNewTermDispatcher >::iterator
- inpc = d_cand_gen_types.find(i->first);
- //we know that this op exists
- Assert(inpc != d_cand_gen_types.end());
- inpc->second.send(i->second);
- }
-
-}
-
-
-/** merge */
-void EfficientEMatcher::merge( TNode a, TNode b ){
- if( options::efficientEMatching() ){
- //merge eqc_ops of b into a
- EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
- EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
-
- if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){
- Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl;
-
- //determine new candidates for instantiation
- computeCandidatesPcPairs( a, eci_a, b, eci_b );
- computeCandidatesPcPairs( b, eci_b, a, eci_a );
- computeCandidatesPpPairs( a, eci_a, b, eci_b );
- computeCandidatesPpPairs( b, eci_b, a, eci_a );
- }
- computeCandidatesConstants( a, eci_a, b, eci_b);
- computeCandidatesConstants( b, eci_b, a, eci_a);
-
- eci_a->merge( eci_b );
- }
-}
-
-/** assert terms are disequal */
-void EfficientEMatcher::assertDisequal( TNode a, TNode b, TNode reason ){
-
-}
-
-EqClassInfo* EfficientEMatcher::getEquivalenceClassInfo( Node n ) {
- return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
-}
-EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){
- Assert( n==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<NodePpDispatcher*, Ips, Ips> > >::iterator it2 = it->second.begin();
- it2 != it->second.end(); ++it2 ){
- Node g = it2->first;
- if( eci_b->hasParent( g ) ){
- Debug("efficient-e-match") << " Checking parent application " << g << std::endl;
- //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
- for( std::vector< triple<NodePpDispatcher*, Ips, Ips> > ::iterator cit = it2->second.begin();
- cit != it2->second.end(); ++cit ){
-#ifdef CVC4_DEBUG
- Debug("efficient-e-match") << " Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl;
-#endif
- Debug("efficient-e-match") << " Check inverted path string ";
- outputIps( "efficient-e-match", cit->second );
- SetNode a_terms;
- a_terms.insert( a );
- collectTermsIps( cit->second, a_terms );
- if( a_terms.empty() ) continue;
- Debug("efficient-e-match") << " And check inverted path string ";
- outputIps( "efficient-e-match", cit->third );
- SetNode b_terms;
- b_terms.insert( b );
- collectTermsIps( cit->third, b_terms );
- if( b_terms.empty() ) continue;
- //Start debug
- Debug("efficient-e-match") << " -> Possibly Added termsA (" << a_terms.size() << "): ";
- for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end();
- t!=end; ++t ){
- Debug("efficient-e-match") << (*t) << " ";
- }
- Debug("efficient-e-match") << std::endl;
- Debug("efficient-e-match") << " -> Possibly Added termsB (" << b_terms.size() << "): ";
- for( SetNode::const_iterator t=b_terms.begin(), end=b_terms.end();
- t!=end; ++t ){
- Debug("efficient-e-match") << (*t) << " ";
- }
- Debug("efficient-e-match") << std::endl;
- //End debug
-
- cit->first->send(a_terms,b_terms);
- }
- }
- }
- }
- }
-}
-
-
-void EfficientEMatcher::computeCandidatesConstants( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
- Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl;
- Debug("efficient-e-match") << " Eq class = [";
- outputEqClass( "efficient-e-match", a);
- Debug("efficient-e-match") << "]" << std::endl;
- outputEqClassInfo("efficient-e-match",eci_a);
- for( std::map< Node, std::map< Node, NodePcDispatcher* > >::iterator
- it = d_cc_pairs.begin(), end = d_cc_pairs.end();
- it != end; ++it ) {
- Debug("efficient-e-match") << " Checking application " << it->first << std::endl;
- if( !eci_b->hasFunction(it->first) ) continue;
- for( std::map< Node, NodePcDispatcher* >::iterator
- itc = it->second.begin(), end = it->second.end();
- itc != end; ++itc ) {
- //The constant
- Debug("efficient-e-match") << " Checking constant " << a << std::endl;
- if(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<Node> & parents = db->getParents(n,f,arg);
- for( size_t i=0; i<parents.size(); ++i ){
- TNode t = parents[i];
- if(!CandidateGenerator::isLegalCandidate(t)) continue;
- if( addRep ) t = getEqualityEngine()->getRepresentative( t );
- terms.insert(t);
- addedTerm = true;
- }
- }
- return addedTerm;
-}
-
-void EfficientEMatcher::registerPatternElementPairs2( Node pat, Ips& ips, PpIpsMap & pp_ips_map, NodePcDispatcher* npc ){
- Assert( pat.hasOperator() );
- //add information for possible pp-pair
- ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); //0 is just a dumb value
-
- for( int i=0; i<(int)pat.getNumChildren(); i++ ){
- if( pat[i].getKind()==INST_CONSTANT ){
- ips.back().second = i;
- pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), Ips( ips ) ) );
- }
- }
-
- for( int i=0; i<(int)pat.getNumChildren(); i++ ){
- if( pat[i].getKind()==APPLY_UF ){
- ips.back().second = i;
- registerPatternElementPairs2( pat[i], ips, pp_ips_map, npc );
- Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl;
- Debug("pattern-element-opt") << " Path = ";
- outputIps( "pattern-element-opt", ips );
- Debug("pattern-element-opt") << std::endl;
- //pat.getOperator() and pat[i].getOperator() are a pc-pair
- d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ]
- .push_back( make_pair(npc,Ips(ips)) );
- }
- }
- ips.pop_back();
-}
-
-void EfficientEMatcher::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
- NodePcDispatcher* npc,
- NodePpDispatcher* npp){
- Ips ips;
- registerPatternElementPairs2( pat, ips, pp_ips_map, npc );
- for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
- // for each variable construct all the pp-pair
- for( size_t j=0; j<it->second.size(); j++ ){
- for( size_t k=j+1; k<it->second.size(); k++ ){
- //found a pp-pair
- Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl;
- Debug("pattern-element-opt") << " Paths = ";
- outputIps( "pattern-element-opt", it->second[j].second );
- Debug("pattern-element-opt") << " and ";
- outputIps( "pattern-element-opt", it->second[k].second );
- Debug("pattern-element-opt") << std::endl;
- d_pp_pairs[ it->second[j].first ][ it->second[k].first ]
- .push_back( make_triple( npp, it->second[j].second, it->second[k].second ));
- }
- }
- }
-};
-
-void findPpSite(Node pat, EfficientEMatcher::Ips& ips, EfficientEMatcher::PpIpsMap & pp_ips_map){
- Assert( pat.getKind()==APPLY_UF );
- //add information for possible pp-pair
-
- ips.push_back( make_pair( pat.getOperator(), 0) );
- for( size_t i=0; i<pat.getNumChildren(); i++ ){
- if( pat[i].getKind()==INST_CONSTANT ){
- ips.back().second = i;
- pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), EfficientEMatcher::Ips( ips ) ) );
- }
- }
-
- for( size_t i=0; i<pat.getNumChildren(); i++ ){
- if( pat[i].getKind()==APPLY_UF ){
- ips.back().second = i;
- findPpSite( pat[i], ips, pp_ips_map );
- }
- }
- ips.pop_back();
-}
-
-void EfficientEMatcher::combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
- EfficientHandler& eh, size_t index2,const std::vector<Node> & pats){
- hash_map<size_t,NodePpDispatcher*> npps;
- for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
- MultiPpIpsMap::iterator mit = multi_pp_ips_map.find(it->first);
- if(mit == multi_pp_ips_map.end()) continue;
- // for each variable construct all the pp-pair
- // j the last pattern treated
- for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
- j != jend; ++j){
- // k one of the previous one
- for( std::vector< triple< size_t, Node, Ips > >::iterator k=mit->second.begin(), kend = mit->second.end() ;
- k != kend; ++k){
- //found a pp-pair
- Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j->first
- << ", " << k->second << " in "<< k->first
- << " )" << std::endl;
- Debug("pattern-element-opt") << " Paths = ";
- outputIps( "pattern-element-opt", j->second );
- Debug("pattern-element-opt") << " and ";
- outputIps( "pattern-element-opt", k->third );
- Debug("pattern-element-opt") << std::endl;
- NodePpDispatcher* dispatcher;
- hash_map<size_t,NodePpDispatcher*>::iterator inpp = npps.find(k->first);
- if( inpp != npps.end() ) dispatcher = inpp->second;
- else{
- dispatcher = new NodePpDispatcher();
-#ifdef CVC4_DEBUG
- dispatcher->pat1 = pats[index2];
- dispatcher->pat2 = pats[k->first];
-#endif
- dispatcher->addPpDispatcher(&eh,index2,k->first);
- };
- d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third ));
- }
- }
- }
-
- /** Put pp_ips_map to multi_pp_ips_map */
- for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
- for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
- j != jend; ++j){
- multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second));
- }
- }
-
-}
-
-
-void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler,
- const std::vector< Node > & pats ){
- Assert(pats.size() > 0);
-
- MultiPpIpsMap multi_pp_ips_map;
- PpIpsMap pp_ips_map;
- //In a multi-pattern Pattern that is only a variable are specials,
- //if the variable appears in another pattern, it can be discarded.
- //Otherwise new term of this term can be candidate. So we stock them
- //here before adding them.
- std::vector< size_t > patVars;
-
- Debug("pattern-element-opt") << "Register patterns" << pats << std::endl;
- for(size_t i = 0; i < pats.size(); ++i){
- if( pats[i].getKind() == kind::INST_CONSTANT){
- patVars.push_back(i);
- continue;
- }
- //to complete
- if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
- Node cst = NodeManager::currentNM()->mkConst<bool>(false);
- TNode op = pats[i][0].getOperator();
- if(d_cc_pairs[op][cst] == NULL){
- d_cc_pairs[op][cst] = new NodePcDispatcher();
- }
- d_cc_pairs[op][cst]->addPcDispatcher(&handler,i);
- continue;
- }
- //end to complete
- Debug("pattern-element-opt") << " Register candidate generator..." << pats[i] << std::endl;
- /* Has the pattern already been seen */
- if( d_pat_cand_gens.find( pats[i] )==d_pat_cand_gens.end() ){
- NodePcDispatcher* npc = new NodePcDispatcher();
- NodePpDispatcher* npp = new NodePpDispatcher();
-#ifdef CVC4_DEBUG
- npc->pat = pats[i];
- npp->pat1 = pats[i];
- npp->pat2 = pats[i];
-#endif
- d_pat_cand_gens[pats[i]] = make_pair(npc,npp);
- registerPatternElementPairs( pats[i], pp_ips_map, npc, npp );
- }else{
- Ips ips;
- findPpSite(pats[i],ips,pp_ips_map);
- }
- //Has the top operator already been seen */
- TNode op = pats[i].getOperator();
- d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
- d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
- d_cand_gens[op].addNewTermDispatcher(&handler,i);
-
- combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
-
- pp_ips_map.clear();
- }
-
- for(size_t i = 0; i < patVars.size(); ++i){
- TNode var = pats[patVars[i]];
- Assert( var.getKind() == kind::INST_CONSTANT );
- if( multi_pp_ips_map.find(var) != multi_pp_ips_map.end() ){
- //The variable appear in another pattern, skip it
- continue;
- };
- d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]);
- }
-
- //take all terms from the uf term db and add to candidate generator
- if( pats[0].getKind() == kind::INST_CONSTANT ){
- TypeNode ty = pats[0].getType();
- rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine);
- cg->reset(Node::null());
- TNode c;
- SetNode ele;
- while( !(c = cg->getNextCandidate()).isNull() ){
- if( c.getType() == ty ) ele.insert(c);
- }
- if( !ele.empty() ){
- if(Debug.isOn("efficient-e-match-stats")){
- Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
- }
- handler.addMonoCandidate(ele, 0);
- }
-
- } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){
- Node cst = NodeManager::currentNM()->mkConst<bool>(false);
- TNode op = pats[0][0].getOperator();
- cst = 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 */
+++ /dev/null
-/********************* */
-/*! \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<Node> SetNode;
-
-template<class T>
-class CleanUpPointer{
-public:
- inline void operator()(T** e){
- delete(*e);
- };
-};
-
-class EfficientHandler{
-public:
- typedef std::pair< Node, size_t > MonoCandidate;
- typedef std::pair< MonoCandidate, MonoCandidate > MultiCandidate;
- typedef std::pair< SetNode, size_t > MonoCandidates;
- typedef std::pair< MonoCandidates, MonoCandidates > MultiCandidates;
-private:
- /* Queue of candidates */
- typedef context::CDQueue< MonoCandidates *, CleanUpPointer<MonoCandidates> > MonoCandidatesQueue;
- typedef context::CDQueue< MultiCandidates *, CleanUpPointer<MultiCandidates> > MultiCandidatesQueue;
- MonoCandidatesQueue d_monoCandidates;
- typedef SetNode::iterator SetNodeIter;
- context::CDO<SetNodeIter> d_si;
- context::CDO<bool> d_mono_not_first;
-
- MonoCandidatesQueue d_monoCandidatesNewTerm;
- context::CDO<SetNodeIter> d_si_new_term;
- context::CDO<bool> d_mono_not_first_new_term;
-
-
- MultiCandidatesQueue d_multiCandidates;
- context::CDO<SetNodeIter> d_si1;
- context::CDO<SetNodeIter> d_si2;
- context::CDO<bool> d_multi_not_first;
-
-
- friend class EfficientEMatcher;
- friend class HandlerPcDispatcher;
- friend class HandlerPpDispatcher;
- friend class HandlerNewTermDispatcher;
-protected:
- void addMonoCandidate(SetNode & s, size_t index){
- Assert(!s.empty());
- d_monoCandidates.push(new MonoCandidates(s,index));
- }
- void addMonoCandidateNewTerm(SetNode & s, size_t index){
- Assert(!s.empty());
- d_monoCandidatesNewTerm.push(new MonoCandidates(s,index));
- }
- void addMultiCandidate(SetNode & s1, size_t index1, SetNode & s2, size_t index2){
- Assert(!s1.empty() && !s2.empty());
- d_multiCandidates.push(new MultiCandidates(MonoCandidates(s1,index1),
- MonoCandidates(s2,index2)));
- }
-public:
- EfficientHandler(context::Context * c):
- //false for d_mono_not_first beacause its the default constructor
- d_monoCandidates(c), d_si(c), d_mono_not_first(c,false),
- d_monoCandidatesNewTerm(c), d_si_new_term(c),
- d_mono_not_first_new_term(c,false),
- d_multiCandidates(c) , d_si1(c), d_si2(c), d_multi_not_first(c,false) {};
-
- bool getNextMonoCandidate(MonoCandidate & candidate){
- if(d_monoCandidates.empty()) return false;
- const MonoCandidates * front = d_monoCandidates.front();
- SetNodeIter si_tmp;
- if(!d_mono_not_first){
- Assert(front->first.begin() != front->first.end());
- d_mono_not_first = true;
- si_tmp=front->first.begin();
- }else{
- si_tmp = d_si;
- ++si_tmp;
- };
- if(si_tmp != front->first.end()){
- candidate.first = (*si_tmp);
- candidate.second = front->second;
- d_si = si_tmp;
- Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
- return true;
- };
- d_monoCandidates.pop();
- d_mono_not_first = false;
- return getNextMonoCandidate(candidate);
- };
-
- bool getNextMonoCandidateNewTerm(MonoCandidate & candidate){
- if(d_monoCandidatesNewTerm.empty()) return false;
- const MonoCandidates * front = d_monoCandidatesNewTerm.front();
- SetNodeIter si_tmp;
- if(!d_mono_not_first_new_term){
- Assert(front->first.begin() != front->first.end());
- d_mono_not_first_new_term = true;
- si_tmp=front->first.begin();
- }else{
- si_tmp = d_si_new_term;
- ++si_tmp;
- };
- if(si_tmp != front->first.end()){
- candidate.first = (*si_tmp);
- candidate.second = front->second;
- d_si_new_term = si_tmp;
- Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
- return true;
- };
- d_monoCandidatesNewTerm.pop();
- d_mono_not_first_new_term = false;
- return getNextMonoCandidateNewTerm(candidate);
- };
-
- bool getNextMultiCandidate(MultiCandidate & candidate){
- if(d_multiCandidates.empty()) return false;
- const MultiCandidates* front = d_multiCandidates.front();
- SetNodeIter si1_tmp;
- SetNodeIter si2_tmp;
- if(!d_multi_not_first){
- Assert(front->first.first.begin() != front->first.first.end());
- Assert(front->second.first.begin() != front->second.first.end());
- si1_tmp = front->first.first.begin();
- si2_tmp = front->second.first.begin();
- }else{
- si1_tmp = d_si1;
- si2_tmp = d_si2;
- ++si2_tmp;
- };
- if(si2_tmp != front->second.first.end()){
- candidate.first.first = *si1_tmp;
- candidate.first.second = front->first.second;
- candidate.second.first = *si2_tmp;
- candidate.second.second = front->second.second;
- if(!d_multi_not_first){d_si1 = si1_tmp; d_multi_not_first = true; };
- d_si2 = si2_tmp;
- Debug("efficienthandler") << "Multi1 produces "
- << candidate.first.first << " for "
- << candidate.first.second << " and "
- << candidate.second.first << " for "
- << candidate.second.second << " and "
- << std::endl;
- return true;
- }; // end of the second set
- si2_tmp = front->second.first.begin();
- ++si1_tmp;
- if(si1_tmp != front->first.first.end()){
- candidate.first.first = *si1_tmp;
- candidate.first.second = front->first.second;
- candidate.second.first = *si2_tmp;
- candidate.second.second = front->second.second;
- d_si1 = si1_tmp;
- d_si2 = si2_tmp;
- Debug("efficienthandler") << "Multi2 produces "
- << candidate.first.first << " for "
- << candidate.first.second << " and "
- << candidate.second.first << " for "
- << candidate.second.second << " and "
- << std::endl;
- return true;
- }; // end of the first set
- d_multiCandidates.pop();
- d_multi_not_first = false;
- return getNextMultiCandidate(candidate);
- }
-};
-
-class PcDispatcher{
-public:
- virtual ~PcDispatcher(){};
- /* Send the node to the dispatcher */
- virtual void send(SetNode & s) = 0;
-};
-
-
-class HandlerPcDispatcher: public PcDispatcher{
- EfficientHandler* d_handler;
- size_t d_index;
-public:
- HandlerPcDispatcher(EfficientHandler* handler, size_t index):
- d_handler(handler), d_index(index) {};
- void send(SetNode & s){
- d_handler->addMonoCandidate(s,d_index);
- }
-};
-
-
-/** All the dispatcher that correspond to this node */
-class NodePcDispatcher: public PcDispatcher{
-#ifdef CVC4_DEBUG
-public:
- Node pat;
-#endif/* CVC4_DEBUG*/
-private:
- std::vector<HandlerPcDispatcher> d_dis;
-public:
- void send(SetNode & s){
- Assert(!s.empty());
- for(std::vector<HandlerPcDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
- i != end; ++i){
- (*i).send(s);
- }
- }
- void addPcDispatcher(EfficientHandler* handler, size_t index){
- d_dis.push_back(HandlerPcDispatcher(handler,index));
- }
-};
-
-
-class HandlerNewTermDispatcher: public PcDispatcher{
- EfficientHandler* d_handler;
- size_t d_index;
-public:
- HandlerNewTermDispatcher(EfficientHandler* handler, size_t index):
- d_handler(handler), d_index(index) {};
- void send(SetNode & s){
- d_handler->addMonoCandidateNewTerm(s,d_index);
- }
-};
-
-/** All the dispatcher that correspond to this node */
-class NodeNewTermDispatcher: public PcDispatcher{
-#ifdef CVC4_DEBUG
-public:
- Node pat;
-#endif/* CVC4_DEBUG*/
-private:
- std::vector<HandlerNewTermDispatcher> d_dis;
-public:
- void send(SetNode & s){
- Assert(!s.empty());
- for(std::vector<HandlerNewTermDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
- i != end; ++i){
- (*i).send(s);
- }
- }
- void addNewTermDispatcher(EfficientHandler* handler, size_t index){
- d_dis.push_back(HandlerNewTermDispatcher(handler,index));
- }
-};
-
-class PpDispatcher{
-public:
- virtual ~PpDispatcher(){};
- /* Send the node to the dispatcher */
- virtual void send(SetNode & s1, SetNode & s2, SetNode & sinter) = 0;
-};
-
-
-class HandlerPpDispatcher: public PpDispatcher{
- EfficientHandler* d_handler;
- size_t d_index1;
- size_t d_index2;
-public:
- HandlerPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2):
- d_handler(handler), d_index1(index1), d_index2(index2) {};
- void send(SetNode & s1, SetNode & s2, SetNode & sinter){
- if(d_index1 == d_index2){
- if(!sinter.empty())
- d_handler->addMonoCandidate(sinter,d_index1);
- }else{
- d_handler->addMultiCandidate(s1,d_index1,s2,d_index2);
- }
- }
-};
-
-
-/** All the dispatcher that correspond to this node */
-class NodePpDispatcher: public PpDispatcher{
-#ifdef CVC4_DEBUG
-public:
- Node pat1;
- Node pat2;
-#endif/* CVC4_DEBUG */
-private:
- std::vector<HandlerPpDispatcher> d_dis;
- void send(SetNode & s1, SetNode & s2, SetNode & inter){
- for(std::vector<HandlerPpDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
- i != end; ++i){
- (*i).send(s1,s2,inter);
- }
- }
-public:
- void send(SetNode & s1, SetNode & s2){
- // can be done in HandlerPpDispatcher lazily
- Assert(!s1.empty() && !s2.empty());
- SetNode inter;
- std::set_intersection( s1.begin(), s1.end(), s2.begin(), s2.end(),
- std::inserter( inter, inter.begin() ) );
- send(s1,s2,inter);
- }
- void addPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2){
- d_dis.push_back(HandlerPpDispatcher(handler,index1,index2));
- }
-};
-
-//equivalence class info
-class EqClassInfo
-{
-public:
- typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
- typedef context::CDChunkList<Node> NodeList;
-public:
- //a list of operators that occur as top symbols in this equivalence class
- // Efficient E-Matching for SMT Solvers: "funs"
- BoolMap d_funs;
- //a list of operators f for which a term of the form f( ... t ... ) exists
- // Efficient E-Matching for SMT Solvers: "pfuns"
- BoolMap d_pfuns;
- //a list of equivalence classes that are disequal
- BoolMap d_disequal;
-public:
- EqClassInfo( context::Context* c );
- ~EqClassInfo(){}
- //set member
- void setMember( Node n, quantifiers::TermDb* db );
- //has function "funs"
- bool hasFunction( Node op );
- //has parent "pfuns"
- bool hasParent( Node op );
- //merge with another eq class info
- void merge( EqClassInfo* eci );
-};
-
-class EfficientEMatcher{
-protected:
- /** reference to the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
-public:
- EfficientEMatcher(CVC4::theory::QuantifiersEngine* qe);
- ~EfficientEMatcher() {
- for(std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> >::iterator
- i = d_pat_cand_gens.begin(), end = d_pat_cand_gens.end();
- i != end; i++){
- delete(i->second.first);
- delete(i->second.second);
- }
- }
- /** 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<NodePcDispatcher*, NodePpDispatcher*> > d_pat_cand_gens;
- /** helper functions */
- void registerPatternElementPairs2( Node pat, Ips& ips,
- PpIpsMap & pp_ips_map, NodePcDispatcher* npc);
- void registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
- NodePcDispatcher* npc, NodePpDispatcher* npp);
- /** find the pp-pair between pattern inside multi-pattern*/
- void combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
- EfficientHandler& eh, size_t index2,
- const std::vector<Node> & pats); //pats for debug
- /** compute candidates for pc pairs */
- void computeCandidatesPcPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
- /** compute candidates for pp pairs */
- void computeCandidatesPpPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
- /** compute candidates for cc pairs */
- void computeCandidatesConstants( Node a, EqClassInfo*, Node b, EqClassInfo* );
- /** collect terms based on inverted path string */
- void collectTermsIps( Ips& ips, SetNode& terms, int index);
- bool collectParentsTermsIps( Node n, Node f, int arg, SetNode& terms, bool addRep, bool modEq = true );
-public:
- void collectTermsIps( Ips& ips, SetNode& terms);
-public:
- void registerEfficientHandler( EfficientHandler& eh, const std::vector<Node> & pat );
-public:
- void newTerms(SetNode& s);
-public:
- /** output eq class */
- void outputEqClass( const char* c, Node n );
- /** output inverted path string */
- void outputIps( const char* c, Ips& ips );
-};/* class EfficientEMatcher */
-
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EFFICIENT_E_MATCHING_H */
+++ /dev/null
-# 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
+++ /dev/null
-#
-# 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
+++ /dev/null
-/********************* */
-/*! \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();
-}
-
+++ /dev/null
-/********************* */
-/*! \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_iter<d_term_iter_limit ){
- TNode n = d_tdb->d_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_iter<d_term_iter_limit ){
- TNode n = d_tdb->d_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 */
+++ /dev/null
-/********************* */
-/*! \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; i<f[0].getNumChildren(); i++ ){
- Node ic = qe->getTermDatabase()->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<bool modEq>
-class InstMatchTrie2Pairs
-{
- typename std::vector< std::vector < typename InstMatchTrie2Gen<modEq>::Tree > > d_data;
- InstMatchTrie2Gen<modEq> 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<modEq>::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<Node> & vars){
- if(pat.isNull()) return true;
-
- typedef std::vector<std::pair<TNode,TNode> > tstack;
- tstack stack(1,std::make_pair(t0,pat)); // t * pat
-
- while(!stack.empty()){
- const std::pair<TNode,TNode> 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<TNode,size_t,EqualityQuery*> >::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 CG, class M>
-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 M>
-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 M, class Test >
-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<TNode,bool>*/ {
- 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<TNode,bool>*/ {
- 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<TNode,bool>*/ {
- 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<TNode,bool>*/ {
-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<uf::TheoryUF *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(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<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_DATATYPES ));
- eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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<arrays::TheoryArrays *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_ARRAY ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(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<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(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 <bool classes> /** 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<false>, 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<false> 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<true>, 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<true> 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<datatypes::TheoryDatatypes *>(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<arrays::TheoryArrays *>(te->theoryOf( theory::THEORY_ARRAY ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
- return new CandidateGeneratorTheoryEeClasses(ee);
- } else {
- uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(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<Node> & 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<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
- CandidateGeneratorTheoryEeClasses cdtUfEq(ee);
- /* Create a matcher from the candidate generator */
- AuxMatcher1 am1(cdtUfEq,am2);
- return am1;
- }
-public:
- UfEqMatcher( std::vector<Node> & 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<Node,bool>*/ {
- 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<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(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<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine()->
- getRepresentative(NodeManager::currentNM()->mkConst<bool>(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<ArithMatcher, LegalTypeTest>
- am2(am3,LegalTypeTest(pat.getType()));
- /* generator */
- uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*> (uf->getEqualityEngine());
- CandidateGeneratorTheoryEeClass cdtUfEq(ee);
- return new CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass,
- TestMatcher<ArithMatcher, LegalTypeTest> > (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<ArithMatcher, LegalTest>
- am2(am3,LegalTest());
- /* generator */
- TermDb* tdb = qe->getTermDatabase();
- CandidateGeneratorTheoryUfType cdtUfEq(pat.getType(),tdb);
- typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfType,
- TestMatcher<ArithMatcher, LegalTest> > AuxMatcher1;
- return new PatOfMatcher<AuxMatcher1>(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<Rational>() );
- 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; i<quant[0].getNumChildren(); i++ ){
- terms.push_back( im_copy.get( qe, quant, i ) );
- }
-
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- 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<true> d_cache;
- std::vector<Node> 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; i<quant[0].getNumChildren(); i++ ){
- terms.push_back( im_copy.get( qe, quant, i ) );
- }
-
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- 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 */
+++ /dev/null
-/********************* */
-/*! \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 <ext/hash_set>
-#include <iostream>
-#include <map>
-
-#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<class Iterator>
- 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<bool modEq = false> class InstMatchTrie2;
-template<bool modEq = false> class InstMatchTrie2Pairs;
-
-template<bool modEq = false>
-class InstMatchTrie2Gen
-{
- friend class InstMatchTrie2<modEq>;
- friend class InstMatchTrie2Pairs<modEq>;
-
-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<Tree *, TNode> 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<Mod, CleanUp, std::allocator<Mod> > d_mods;
-
-
- typedef std::map<Node, Node>::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<bool modEq>
-class InstMatchTrie2
-{
- typename InstMatchTrie2Gen<modEq>::Tree d_data;
- InstMatchTrie2Gen<modEq> 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<Node> & vars);
-
-class InstMatchGenerator;
-
-}/* CVC4::theory rrinst */
-
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */
+++ /dev/null
-/********************* */
-/*! \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<bool modEq>
-InstMatchTrie2Gen<modEq>::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<bool modEq>
-void InstMatchTrie2Gen<modEq>::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 modEq>
-bool InstMatchTrie2Gen<modEq>::existsInstMatch(InstMatchTrie2Gen<modEq>::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<modEq>::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<modEq>::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 modEq>
-bool InstMatchTrie2Gen<modEq>::
-addInstMatch( InstMatch& m, InstMatchTrie2Gen<modEq>::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 */
+++ /dev/null
-/********************* */
-/*! \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 );
- }
-}
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 <vector>
-#include <ext/hash_set>
-#include <ext/hash_map>
-#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<Node> Subst;
- typedef std::vector<Expr> ESubst;
- typedef std::vector<TMPNode> 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<std::pair<TMPNode,TMPNode> > tstack;
- tstack stack(1,std::make_pair(node,pattern)); // t * pat
-
- while(!stack.empty()){
- const std::pair<TMPNode,TMPNode> 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<Pattern> 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 */
+++ /dev/null
-/********************* */
-/*! \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<THEORY_REWRITERULES> {
- 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<true, THEORY_REWRITERULES>, Node> pre_rewrite;
- typedef expr::Attribute< RewriteCacheTag<false, THEORY_REWRITERULES>, Node> post_rewrite;
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H */
+++ /dev/null
-/********************* */
-/*! \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<Node> & vars){
- typedef std::vector<std::pair<TNode,TNode> > tstack;
- tstack stack(1,std::make_pair(t0,pattern)); // t * pat
-
- while(!stack.empty()){
- const std::pair<TNode,TNode> 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<TNode> 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<Node> & pattern,
- std::vector<Node> & vars,
- std::vector<Node> & 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<Node>(tri):
- re.getQuantifiersEngine()->getTermDatabase()->
- convertNodeToPattern(tri,r,vars,inst_constants));
-}
-
-/*** Check that triggers contains all the variables */
-void checkPatternVarsAux(TNode pat,const std::vector<Node> & vars,
- std::vector<bool> & 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<Node> & pattern,
- const std::vector<Node> & vars){
- std::vector<bool> seen(vars.size(),false);
- for(std::vector<Node>::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<Node> 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<Node> inst_constants = createInstVariable(r,vars);
- /* Body/Remove_term/Guards/Triggers */
- Node body = r[2][1];
- TNode new_terms = r[2][1];
- std::vector<Node> guards;
- std::vector<Node> pattern;
- std::vector<Node> 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<Node>(patternB);
- forallB << static_cast<Node>(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<Node> & g, Node b, TNode nt,
- std::vector<Node> & fv,std::vector<Node> & iv,
- std::vector<Node> & 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<Node>::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<Node> TheoryRewriteRules::createInstVariable( Node r, std::vector<Node> & vars ){
- std::vector<Node> inst_constant;
- inst_constant.reserve(vars.size());
- for( std::vector<Node>::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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
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<Assertion>::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<Assertion>::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());
}
}
}
projects / cvc5.git / commitdiff