diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/rewriterules | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/rewriterules')
-rw-r--r-- | src/theory/rewriterules/Makefile | 4 | ||||
-rw-r--r-- | src/theory/rewriterules/Makefile.am | 19 | ||||
-rw-r--r-- | src/theory/rewriterules/README.WHATS-NEXT | 29 | ||||
-rw-r--r-- | src/theory/rewriterules/kinds | 37 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.cpp | 519 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.h | 264 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_params.h | 95 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_preprocess.h | 176 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rewriter.h | 104 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rules.cpp | 303 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rules.h | 40 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_type_rules.h | 98 |
12 files changed, 1688 insertions, 0 deletions
diff --git a/src/theory/rewriterules/Makefile b/src/theory/rewriterules/Makefile new file mode 100644 index 000000000..4b1d4fc55 --- /dev/null +++ b/src/theory/rewriterules/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/rewriterules + +include $(topdir)/Makefile.subdir diff --git a/src/theory/rewriterules/Makefile.am b/src/theory/rewriterules/Makefile.am new file mode 100644 index 000000000..46cffda11 --- /dev/null +++ b/src/theory/rewriterules/Makefile.am @@ -0,0 +1,19 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = librewriterules.la + +librewriterules_la_SOURCES = \ + theory_rewriterules_rules.h \ + theory_rewriterules_rules.cpp \ + theory_rewriterules.h \ + theory_rewriterules.cpp \ + theory_rewriterules_rewriter.h \ + theory_rewriterules_type_rules.h \ + theory_rewriterules_preprocess.h \ + theory_rewriterules_params.h + +EXTRA_DIST = \ + kinds diff --git a/src/theory/rewriterules/README.WHATS-NEXT b/src/theory/rewriterules/README.WHATS-NEXT new file mode 100644 index 000000000..eda7dcbe6 --- /dev/null +++ b/src/theory/rewriterules/README.WHATS-NEXT @@ -0,0 +1,29 @@ +Congratulations, you now have a new theory of rewriterules ! + +Your next steps will likely be: + +* to specify theory constants, types, and operators in your \`kinds' file +* to add typing rules to theory_${dir}_type_rules.h for your operators + and constants +* to write code in theory_${dir}_rewriter.h to implement a normal form + for your theory's terms +* to write parser rules in src/parser/cvc/Cvc.g to support the CVC input + language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1 + language, and src/parser/smt2/Smt2.g to support SMT-LIBv2 +* to write printer code in src/printer/*/*_printer* to support printing + your theory terms and types in various output languages + +and finally: + +* to implement a decision procedure for your theory by implementing + TheoryRewriterules::check() in theory_rewriterules.cpp. Before writing the actual + code, you will need : + + * to determine which datastructures are context dependent and use for them + context dependent datastructures (context/cd*.h) + * to choose which work will be done at QUICK_CHECK, STANDARD or at + FULL_EFFORT. + + +Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance +should you need it! diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds new file mode 100644 index 000000000..01fbda51e --- /dev/null +++ b/src/theory/rewriterules/kinds @@ -0,0 +1,37 @@ +# 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... + +# types... +sort RRHB_TYPE \ + Cardinality::INTEGERS \ + not-well-founded \ + "head and body of the rule type" + +# operators... + +# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE +operator REWRITE_RULE 3 "generale rewrite rule" +#HEAD/BODY/TRIGGER +operator RR_REWRITE 2:3 "actual rewrite rule" +operator RR_REDUCTION 2:3 "actual reduction rule" +operator RR_DEDUCTION 2:3 "actual deduction rule" + +typerule REWRITE_RULE ::CVC4::theory::rewriterules::RewriteRuleTypeRule +typerule RR_REWRITE ::CVC4::theory::rewriterules::RRRewriteTypeRule +typerule RR_REDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule +typerule RR_DEDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule + +endtheory diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp new file mode 100644 index 000000000..0072a36e9 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -0,0 +1,519 @@ +/********************* */ +/*! \file rewrite_engine.cpp + ** \verbatim + ** Original author: ajreynolds + ** Major contributors: bobot + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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/rewriterules/theory_rewriterules_rules.h" +#include "theory/rewriterules/theory_rewriterules_params.h" + +#include "theory/rewriterules/theory_rewriterules_preprocess.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; + + +namespace CVC4 { +namespace theory { +namespace rewriterules { + + +inline std::ostream& operator <<(std::ostream& stream, const RuleInst& ri) { + ri.toStream(stream); + return stream; +} + +static const RuleInst* RULEINST_TRUE = (RuleInst*) 1; +static const RuleInst* RULEINST_FALSE = (RuleInst*) 2; + + /** Rule an instantiation with the given match */ +RuleInst::RuleInst(TheoryRewriteRules & re, const RewriteRule * r, + std::vector<Node> & inst_subst, + Node matched): + rule(r), d_matched(matched) +{ + Assert(r != NULL); + Assert(!r->directrr || !d_matched.isNull()); + subst.swap(inst_subst); +}; + +Node RuleInst::substNode(const TheoryRewriteRules & re, TNode r, + TCache cache ) const { + Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); + return r.substitute (rule->free_vars.begin(),rule->free_vars.end(), + subst.begin(),subst.end(),cache); +}; +size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{ + TCache cache; + Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); + while (start < (rule->guards).size()){ + Node g = substNode(re,rule->guards[start],cache); + switch(re.addWatchIfDontKnow(g,this,start)){ + case ATRUE: + Debug("rewriterules") << g << "is true" << std::endl; + ++start; + continue; + case AFALSE: + Debug("rewriterules") << g << "is false" << std::endl; + return -1; + case ADONTKNOW: + Debug("rewriterules") << g << "is unknown" << std::endl; + return start; + } + } + /** All the guards are verified */ + re.propagateRule(this,cache); + return start; +}; + +bool RuleInst::alreadyRewritten(TheoryRewriteRules & re) const{ + Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); + static NoMatchAttribute rewrittenNodeAttribute; + TCache cache; + for(std::vector<Node>::const_iterator + iter = rule->to_remove.begin(); + iter != rule->to_remove.end(); ++iter){ + if (substNode(re,*iter,cache).getAttribute(rewrittenNodeAttribute)) + return true; + }; + return false; +} + +void RuleInst::toStream(std::ostream& out) const{ + if(this == RULEINST_TRUE){ out << "TRUE"; return;}; + if(this == RULEINST_FALSE){ out << "FALSE"; return;}; + out << "(" << *rule << ") "; + for(std::vector<Node>::const_iterator + iter = subst.begin(); iter != subst.end(); ++iter){ + out << *iter << " "; + }; +} + + +void Guarded::nextGuard(TheoryRewriteRules & re)const{ + Assert(inst != RULEINST_TRUE && inst != RULEINST_FALSE); + if(simulateRewritting && inst->alreadyRewritten(re)) return; + inst->findGuard(re,d_guard+1); +}; + +/** start indicate the first guard which is not true */ +Guarded::Guarded(const RuleInst* ri, const size_t start) : + d_guard(start),inst(ri) {}; +Guarded::Guarded(const Guarded & g) : + d_guard(g.d_guard),inst(g.inst) {}; +Guarded::Guarded() : + //dumb value + d_guard(-1),inst(RULEINST_TRUE) {}; + +TheoryRewriteRules::TheoryRewriteRules(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + QuantifiersEngine* qe) : + Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo, qe), + d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0), + d_explanations(c), d_ruleinsts_to_add() + { + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); + Debug("rewriterules") << Node::setdepth(-1); + Debug("rewriterules-rewrite") << Node::setdepth(-1); +} + +void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, + InstMatch & im, + bool delay){ + ++r->nb_matched; + if(rewrite_instantiation) im.applyRewrite(); + if(representative_instantiation) + im.makeRepresentative( getQuantifiersEngine() ); + + if(!cache_match || !r->inCache(*this,im)){ + ++r->nb_applied; + std::vector<Node> subst; + im.computeTermVec(getQuantifiersEngine(), r->inst_vars , subst); + RuleInst * ri = new RuleInst(*this,r,subst, + r->directrr ? im.d_matched : Node::null()); + Debug("rewriterules") << "One matching found" + << (delay? "(delayed)":"") + << ":" << *ri << std::endl; + // Find the first non verified guard, don't save the rule if the + // rule can already be fired In fact I save it otherwise strange + // things append. + Assert(ri->rule != NULL); + if(delay) d_ruleinsts_to_add.push_back(ri); + else{ + if(simulateRewritting && ri->alreadyRewritten(*this)) return; + if(ri->findGuard(*this, 0) != (r->guards).size()) + d_ruleinsts.push_back(ri); + else delete(ri); + }; + }; +} + +void TheoryRewriteRules::check(Effort level) { + CodeTimer codeTimer(d_theoryTime); + + Assert(d_ruleinsts_to_add.empty()); + + while(!done()) { + // Get all the assertions + // TODO: Test that it have already been ppAsserted + 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); + + }; + + Debug("rewriterules") << "Check:" << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl; + + /** Test each rewrite rule */ + for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) { + RewriteRule * r = d_rules[rid]; + if (level!=EFFORT_FULL && r->d_split) continue; + Debug("rewriterules") << " rule: " << r << std::endl; + Trigger & tr = r->trigger; + //reset instantiation round for trigger (set up match production) + tr.resetInstantiationRound(); + //begin iterating from the first match produced by the trigger + tr.reset( Node::null() ); + + /** Test the possible matching one by one */ + InstMatch im; + while(tr.getNextMatch( im )){ + addMatchRuleTrigger(r, im, true); + im.clear(); + } + } + + const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL; + bool polldone = false; + + GuardedMap::const_iterator p = d_guardeds.begin(); + do{ + + + //dequeue instantiated rules + for(; !d_ruleinsts_to_add.empty();){ + RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back(); + if(simulateRewritting && ri->alreadyRewritten(*this)) break; + if(ri->findGuard(*this, 0) != ri->rule->guards.size()) + d_ruleinsts.push_back(ri); + else delete(ri); + }; + + if(do_notification) + /** Temporary way. Poll value */ + for (; p != d_guardeds.end(); ++p){ + TNode g = (*p).first; + const GList * const l = (*p).second; + const Guarded & glast = l->back(); + // Notice() << "Polled?:" << g << std::endl; + if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) continue; + // Notice() << "Polled!:" << g << "->" << (glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) << std::endl; + bool value; + if(getValuation().hasSatValue(g,value)){ + if(value) polldone = true; //One guard is true so pass n check + Debug("rewriterules") << "Poll value:" << g + << " is " << (value ? "true" : "false") << std::endl; + notification(g,value); + //const Guarded & glast2 = (*l)[l->size()-1]; + // Notice() << "Polled!!:" << g << "->" << (glast2.inst == RULEINST_TRUE||glast2.inst == RULEINST_FALSE) << std::endl; + }; + }; + + }while(!d_ruleinsts_to_add.empty() || + (p != d_guardeds.end() && do_notification)); + + if(polldone) d_checkLevel = checkSlowdown; + else d_checkLevel = d_checkLevel > 0 ? (d_checkLevel - 1) : 0; + + /** Narrowing by splitting on the guards */ + /** Perhaps only when no notification? */ + if(narrowing_full_effort && level==EFFORT_FULL){ + for (GuardedMap::const_iterator p = d_guardeds.begin(); + p != d_guardeds.end(); ++p){ + TNode g = (*p).first; + const GList * const l = (*p).second; + const Guarded & glast = (*l)[l->size()-1]; + if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) + continue; + // If it has a value it should already has been notified + bool value; value = value; // avoiding the warning in non debug mode + Assert(!getValuation().hasSatValue(g,value)); + Debug("rewriterules") << "Narrowing on:" << g << std::endl; + /** Can split on already rewritten instrule... but... */ + getOutputChannel().split(g); + } + } + + Assert(d_ruleinsts_to_add.empty()); + Debug("rewriterules") << "Check done:" << d_checkLevel << std::endl; + +}; + +void TheoryRewriteRules::registerQuantifier( Node n ){}; + +Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern ) { + // Debug("rewriterules") << "createTrigger:"; + getQuantifiersEngine()->registerPattern(pattern); + return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern, + match_gen_kind, true); +}; + +bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, + GList * const lpropa) { + Assert(ltested->size() > 0); + const Guarded & glast = (*ltested)[ltested->size()-1]; + if(glast.inst == RULEINST_TRUE || glast.inst == RULEINST_FALSE){ + notification(lpropa,glast.inst == RULEINST_TRUE); + return true; + }; + return false; +}; + +void TheoryRewriteRules::notification(GList * const lpropa, bool b){ + if (b){ + for(GList::const_iterator g = lpropa->begin(); + g != lpropa->end(); ++g) { + (*g).nextGuard(*this); + }; + lpropa->push_back(Guarded(RULEINST_TRUE,0)); + }else{ + lpropa->push_back(Guarded(RULEINST_FALSE,0)); + }; + Assert(lpropa->back().inst == RULEINST_TRUE || + lpropa->back().inst == RULEINST_FALSE); +}; + + + +Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri, + const size_t gid){ + /** TODO: Should use the representative of g, but should I keep the + mapping for myself? */ + /* If it false in one model (current valuation) it's false for all */ + if (useCurrentModel){ + Node val = getValuation().getValue(g0); + Debug("rewriterules") << "getValue:" << g0 << " = " + << val << " is " << (val == d_false) << std::endl; + if (val == d_false) return AFALSE; + }; + /** Currently create a node with a literal */ + Node g = getValuation().ensureLiteral(g0); + GuardedMap::iterator l_i = d_guardeds.find(g); + GList* l; + if( l_i == d_guardeds.end() ) { + /** Normally Not watched so IDONTNOW but since we poll, we can poll now */ + bool value; + if(getValuation().hasSatValue(g,value)){ + if(value) return ATRUE; + else return AFALSE; + }; + //Not watched so IDONTNOW + l = new(getSatContext()->getCMM()) + GList(true, getSatContext());//, + //ContextMemoryAllocator<Guarded>(getContext()->getCMM())); + d_guardeds.insert(g ,l);//.insertDataFromContextMemory(g, l); + /* TODO Add register propagation */ + } else { + l = (*l_i).second; + Assert(l->size() > 0); + const Guarded & glast = (*l)[l->size()-1]; + if(glast.inst == RULEINST_TRUE) return ATRUE; + if(glast.inst == RULEINST_FALSE) return AFALSE; + + }; + /** I DONT KNOW because not watched or because not true nor false */ + l->push_back(Guarded(ri,gid)); + return ADONTKNOW; +}; + +void TheoryRewriteRules::notification(Node g, bool b){ + GuardedMap::const_iterator l = d_guardeds.find(g); + /** Should be a propagated node already known */ + Assert(l != d_guardeds.end()); + notification((*l).second,b); +} + + +void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) { + GuardedMap::const_iterator ilhs = d_guardeds.find(lhs); + GuardedMap::const_iterator irhs = d_guardeds.find(rhs); + /** Should be a propagated node already known */ + Assert(ilhs != d_guardeds.end()); + if( irhs == d_guardeds.end() ) { + /** Not watched so points to the list directly */ + d_guardeds.insertDataFromContextMemory(rhs, (*ilhs).second); + } else { + GList * const llhs = (*ilhs).second; + GList * const lrhs = (*irhs).second; + if(!(notifyIfKnown(llhs,lrhs) || notifyIfKnown(lrhs,llhs))){ + /** If none of the two is known */ + for(GList::const_iterator g = llhs->begin(); g != llhs->end(); ++g){ + lrhs->push_back(*g); + }; + }; + }; +}; + + +void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ + // Debug("rewriterules") << "A rewrite rules is verified. Add lemma:"; + Debug("rewriterules") << "propagateRule" << *inst << std::endl; + const RewriteRule * rule = inst->rule; + ++rule->nb_applied; + // Can be more something else than an equality in fact (eg. propagation rule) + Node equality = inst->substNode(*this,rule->body,cache); + if(propagate_as_lemma){ + Node lemma = equality; + if(rule->guards.size() > 0){ + // TODO: problem with reduction rule => instead of <=> + lemma = substGuards(inst, cache).impNode(equality); + }; + if(rule->directrr){ + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + // if the rule is directly applied by the rewriter, + // we should take care to use the representative that can't be directly rewritable: + // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't + // add the constraint car(cons(x,l) = x because it is rewritten to x = x. + // But we should say cons(a) = x + Assert(lemma.getKind() == kind::EQUAL || + lemma.getKind() == kind::IMPLIES); + Assert(!inst->d_matched.isNull()); + Assert( inst->d_matched.getOperator() == lemma[0].getOperator() ); + // replace the left hand side by the term really matched + Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched; + Node hyp; + NodeBuilder<2> nb; + if(inst->d_matched.getNumChildren() == 1){ + nb.clear( inst->d_matched[0].getType(false) == booleanType ? + kind::IFF : kind::EQUAL ); + nb << inst->d_matched[0] << lemma[0][0]; + hyp = nb; + }else{ + NodeBuilder<> andb(kind::AND); + for(size_t i = 0, + iend = inst->d_matched.getNumChildren(); i < iend; ++i){ + nb.clear( inst->d_matched[i].getType(false) == booleanType ? + kind::IFF : kind::EQUAL ); + nb << inst->d_matched[i] << lemma[0][i]; + andb << static_cast<Node>(nb); + } + hyp = andb; + }; + nb.clear(lemma.getKind()); + nb << inst->d_matched << lemma[1]; + lemma = hyp.impNode(static_cast<Node>(nb)); + Debug("rewriterules-directrr") << " -> " << lemma << std::endl; + }; + // Debug("rewriterules") << "lemma:" << lemma << std::endl; + getOutputChannel().lemma(lemma); + }else{ + Assert(!direct_rewrite); + Node lemma_lit = getValuation().ensureLiteral(equality); + ExplanationMap::const_iterator p = d_explanations.find(lemma_lit); + if(p!=d_explanations.end()) return; //Already propagated + bool value; + if(getValuation().hasSatValue(lemma_lit,value)){ + /* Already assigned */ + if (!value){ + Node conflict = substGuards(inst,cache,lemma_lit); + getOutputChannel().conflict(conflict); + }; + }else{ + getOutputChannel().propagate(lemma_lit); + d_explanations.insert(lemma_lit, *inst); + }; + }; + + if(simulateRewritting){ + static NoMatchAttribute rewrittenNodeAttribute; + // Tag the rewritted terms + for(std::vector<Node>::iterator i = rule->to_remove.begin(); + i == rule->to_remove.end(); ++i){ + (*i).setAttribute(rewrittenNodeAttribute,true); + }; + }; + + //Verify that this instantiation can't immediately fire another rule + for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin(); + p != rule->body_match.end(); ++p){ + RewriteRule * r = (*p).second; + // Debug("rewriterules") << " rule: " << r << std::endl; + // Use trigger2 since we can be in check + Trigger & tr = r->trigger_for_body_match; + InstMatch im; + TNode m = inst->substNode(*this,(*p).first, cache); + tr.getMatch(m,im); + if(!im.empty()){ + im.d_matched = m; + addMatchRuleTrigger(r, im); + } + } +}; + + +Node TheoryRewriteRules::substGuards(const RuleInst *inst, + TCache cache, + /* Already substituted */ + Node last){ + const RewriteRule * r = inst->rule; + /** No guards */ + const size_t size = r->guards.size(); + if(size == 0) return (last.isNull()?d_true:last); + /** One guard */ + if(size == 1 && last.isNull()) return inst->substNode(*this,r->guards[0],cache); + /** Guards */ /* TODO remove the duplicate with a set like in uf? */ + NodeBuilder<> conjunction(kind::AND); + for(std::vector<Node>::const_iterator p = r->guards.begin(); + p != r->guards.end(); ++p) { + Assert(!p->isNull()); + conjunction << inst->substNode(*this,*p,cache); + }; + if (!last.isNull()) conjunction << last; + return conjunction; +} + +Node TheoryRewriteRules::explain(TNode n){ + ExplanationMap::const_iterator p = d_explanations.find(n); + Assert(p!=d_explanations.end(),"I forget the explanation..."); + RuleInst i = (*p).second; + //Notice() << n << "<-" << *(i.rule) << std::endl; + return substGuards(&i, TCache ()); +} + +Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { + addRewriteRule(in); + return PP_ASSERT_STATUS_UNSOLVED; +} + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h new file mode 100644 index 000000000..499535687 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -0,0 +1,264 @@ +/********************* */ +/*! \file rewrite_engine.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/inst_match_impl.h" +#include "util/stats.h" +#include "theory/rewriterules/theory_rewriterules_preprocess.h" + +namespace CVC4 { +namespace theory { +namespace rewriterules { + +typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; + + enum Answer {ATRUE, AFALSE, ADONTKNOW}; + + class TheoryRewriteRules; /** forward */ + + class RewriteRule{ + public: + // constant + const bool d_split; + mutable Trigger trigger; + std::vector<Node> guards; + mutable std::vector<Node> to_remove; /** terms to remove */ + const Node body; + const TNode new_terms; /** new terms included in the body */ + std::vector<Node> free_vars; /* free variable in the rule */ + std::vector<Node> inst_vars; /* corresponding vars in the triggers */ + /* After instantiating the body new match can appear (TNode + because is a subterm of a body on the assicaited rewrite + rule) */ + typedef context::CDList< std::pair<TNode,RewriteRule* > > BodyMatch; + mutable BodyMatch body_match; + mutable Trigger trigger_for_body_match; // used because we can be matching + // trigger when we need new match. + // So currently we use another + // trigger for that. + + //context dependent + typedef InstMatchTrie2<true> CacheNode; + mutable CacheNode d_cache; + + const bool directrr; + + RewriteRule(TheoryRewriteRules & re, + Trigger & tr, Trigger & tr2, + std::vector<Node> & g, Node b, TNode nt, + std::vector<Node> & fv,std::vector<Node> & iv, + std::vector<Node> & to_r, bool drr); + RewriteRule(const RewriteRule & r) CVC4_UNUSED; + RewriteRule& operator=(const RewriteRule &) CVC4_UNUSED; + ~RewriteRule(); + + bool noGuard()const throw () { return guards.size() == 0; }; + bool inCache(TheoryRewriteRules & re, InstMatch & im)const; + + void toStream(std::ostream& out) const; + + /* statistics */ + mutable size_t nb_matched; + mutable size_t nb_applied; + mutable size_t nb_propagated; + + }; + + class RuleInst{ + public: + /** The rule has at least one guard */ + const RewriteRule* rule; + + /** the substitution */ + std::vector<Node> subst; + + /** the term matched (not null if mono-pattern and direct-rr) */ + Node d_matched; + + /** Rule an instantiation with the given match */ + RuleInst(TheoryRewriteRules & re, const RewriteRule* r, + std::vector<Node> & inst_subst, + Node matched); + RuleInst():rule(NULL){} // Dumb + + Node substNode(const TheoryRewriteRules & re, TNode r, TCache cache) const; + size_t findGuard(TheoryRewriteRules & re, size_t start)const; + + void toStream(std::ostream& out) const; + + bool alreadyRewritten(TheoryRewriteRules & re) const; + }; + +/** A pair? */ + class Guarded { + public: + /** The backtracking is done somewhere else */ + const size_t d_guard; /* the id of the guard */ + + /** The shared instantiation data */ + const RuleInst* inst; + + void nextGuard(TheoryRewriteRules & re)const; + + /** start indicate the first guard which is not true */ + Guarded(const RuleInst* ri, const size_t start); + Guarded(const Guarded & g); + /** Should be ssigned by a good garded after */ + Guarded(); + + ~Guarded(){}; + void destroy(){}; + }; + +template<class T> +class CleanUpPointer{ +public: + inline void operator()(T** e){ + delete(*e); + }; +}; + +class TheoryRewriteRules : public Theory { +private: + + KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime"); + + /** list of all rewrite rules */ + /* std::vector< Node > d_rules; */ + // typedef std::vector< std::pair<Node, Trigger > > Rules; + typedef context::CDList< RewriteRule *, + CleanUpPointer<RewriteRule >, + std::allocator< RewriteRule * > > Rules; + Rules d_rules; + typedef context::CDList< RuleInst *, + CleanUpPointer<RuleInst>, + std::allocator< RuleInst * > > RuleInsts; + RuleInsts d_ruleinsts; + + /** The GList* will lead too memory leaks since that doesn't use + CDChunckList */ + typedef context::CDList< Guarded > GList; + typedef context::CDHashMap<Node, GList *, NodeHashFunction> GuardedMap; + GuardedMap d_guardeds; + + /* In order to not monopolize, the system slow down himself: If a + guard stored in d_guardeds become true or false, it waits + checkSlowdown(=10) checks before checking again if some guard take a + value. At FULL_EFFORT regardless of d_checkLevel it check the + guards + */ + context::CDO<size_t> d_checkLevel; + + /** explanation */ + typedef context::CDHashMap<Node, RuleInst , NodeHashFunction> ExplanationMap; + ExplanationMap d_explanations; + + /** new instantiation must be cleared at each conflict used only + inside check */ + typedef std::vector< RuleInst* > QRuleInsts; + QRuleInsts d_ruleinsts_to_add; + public: + /** true and false for predicate */ + Node d_true; + Node d_false; + + /** 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, + QuantifiersEngine* qe); + + /** Usual function for theories */ + void check(Theory::Effort e); + Node explain(TNode n); + void notifyEq(TNode lhs, TNode rhs); + std::string identify() const { + return "THEORY_REWRITERULES"; + } + + Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + + bool ppDontRewriteSubterm(TNode atom){ return true; } + + + private: + void registerQuantifier( Node n ); + + public: + /* TODO modify when notification will be available */ + void notification( Node n, bool b); + + Trigger createTrigger( TNode n, std::vector<Node> & pattern ); + + /** return if the guard (already substituted) is known true or false + or unknown. In the last case it add the Guarded(rid,gid) to the watch + list of this guard */ + Answer addWatchIfDontKnow(Node g, const RuleInst* r, const size_t gid); + + /** An instantiation of a rule is fired (all guards true) we + propagate the body. That can be done by theory propagation if + possible or by lemmas. + */ + void propagateRule(const RuleInst * r, TCache cache); + + /** Auxillary functions */ +private: + /** A guard is verify, notify the Guarded */ + void notification(GList * const lpropa, bool b); + /* If two guards becomes equals we should notify if one of them is + already true */ + bool notifyIfKnown(const GList * const ltested, GList * const lpropa); + + Node substGuards(const RuleInst * inst, + TCache cache, + Node last = Node::null()); + + void addRewriteRule(const Node r); + void computeMatchBody ( const RewriteRule * r, size_t start = 0); + void addMatchRuleTrigger(const RewriteRule* r, + InstMatch & im, bool delay = true); + + /* rewrite pattern */ + typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite; + RegisterRRPpRewrite d_registeredRRPpRewrite; + + bool addRewritePattern(TNode pattern, TNode body, + rewriter::Subst & pvars, + rewriter::Subst & vars); + +};/* class TheoryRewriteRules */ + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h new file mode 100644 index 000000000..ecb5385f9 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -0,0 +1,95 @@ +/********************* */ +/*! \file rewrite_engine.cpp + ** \verbatim + ** Original author: bobot + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 + **/ + + +#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 = 10; + +/** + Use the current model to eliminate guard before asking for notification + */ +static const bool useCurrentModel = false; + +/** + Simulate rewritting by tagging rewritten terms. + */ +static const bool simulateRewritting = false; + +/** + Choose the kind of matching to use: + - InstMatchGenerator::MATCH_GEN_DEFAULT 0 + - InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH 1 +*/ +static const int match_gen_kind = 0; + +/** + 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 = true; + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h new file mode 100644 index 000000000..f17e30758 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h @@ -0,0 +1,176 @@ +/********************* */ +/*! \file rewriterules.h + ** \verbatim + ** Original author: bobot + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief One utilitise for rewriterules definition + ** + **/ + + +#ifndef __CVC4__REWRITERULES_H +#define __CVC4__REWRITERULES_H + +#include <vector> +#include <hash_set> +#include <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 FinalStep : Step { + Node body; + TSubst vars; + + Node subst(Subst & subst){ + return body.substitute(vars.begin(), vars.end(), + subst.begin(), subst.end()); + } + + }; + + 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 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(); + } + }; + +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); + } + +}; + + + +} + +} +} +} +#endif /* __CVC4__REWRITERULES_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h new file mode 100644 index 000000000..d9da095f7 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h @@ -0,0 +1,104 @@ +#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); + } + + /** + * Rewrite an equality, in case special handling is required. + */ + static Node rewriteEquality(TNode equality) { + // often this will suffice + return postRewrite(equality).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() { } + +}; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp new file mode 100644 index 000000000..9847f1727 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -0,0 +1,303 @@ +/********************* */ +/*! \file rewrite_engine.cpp + ** \verbatim + ** Original author: ajreynolds + ** Major contributors: bobot + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::rewriterules; + + +namespace CVC4 { +namespace theory { +namespace rewriterules { + +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) continue; + Trigger & tr = const_cast<Trigger &> (r->trigger_for_body_match); + if(!tr.nonunifiable(t, 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(re.getQuantifiersEngine()-> + 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); + /* 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 = + getQuantifiersEngine()->createInstVariable(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]; + switch(r[2].getKind()){ + case kind::RR_REWRITE: + /* Equality */ + to_remove.push_back(head); + addPattern(*this,head,pattern,vars,inst_constants,r); + body = head.eqNode(body); + break; + case kind::RR_REDUCTION: + /** Add head to remove */ + to_remove.push_back(head); + 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 threee 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].begin(); i != r[2][2].end(); ++i) { + // todo test during typing that its a good term (no not, atom, or term...) + addPattern(*this,(*i)[0],pattern,vars,inst_constants,r); + }; + // Assert(pattern.size() == 1, "currently only single pattern are supported"); + //Every variable must be seen in the pattern + if (!checkPatternVars(pattern,inst_constants)){ + Warning() << "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 && r[2].getKind() == kind::RR_REWRITE) || + (guards.size() == 1 && r[2].getKind() == kind::RR_REDUCTION)) + && pattern.size() == 1){ + directrr = addRewritePattern(pattern[0],new_terms, inst_constants, vars); + } + + // final construction + Trigger trigger = createTrigger(r,pattern); + Trigger trigger2 = createTrigger(r,pattern); //Hack + RewriteRule * rr = new RewriteRule(*this, trigger, trigger2, + 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") << "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 false; + case ITE: + return true; + case NOT: + return willDecide(node[0],!positive); + default: + return false; + } +} + + +RewriteRule::RewriteRule(TheoryRewriteRules & re, + Trigger & tr, Trigger & tr2, + std::vector<Node> & g, Node b, TNode nt, + std::vector<Node> & fv,std::vector<Node> & iv, + std::vector<Node> & to_r, bool drr) : + d_split(willDecide(b)), + trigger(tr), body(b), new_terms(nt), free_vars(), inst_vars(), + body_match(re.getSatContext()),trigger_for_body_match(tr2), + 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, InstMatch & im)const{ + return !d_cache.addInstMatch(im); +}; + +/** A rewrite rule */ +void RewriteRule::toStream(std::ostream& out) const{ + 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 << ")" << ","; + }; + out << "]" << (directrr?"*":"") << std::endl; +} + +RewriteRule::~RewriteRule(){ + Debug("rewriterule-stats") << *this + << " (" << nb_matched + << "," << nb_applied + << "," << nb_propagated + << ")" << std::endl; +} + +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()->getTheory( THEORY_UF ))-> + registerPpRewrite(op,p); + } else p = i->second; + + return p->addRewritePattern(pattern,body,pvars,vars); + +} + + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h new file mode 100644 index 000000000..a8e70f3e6 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_rules.h @@ -0,0 +1,40 @@ +/********************* */ +/*! \file rewrite_engine.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Rewrite Engine classes + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H +#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H + +#include "theory/rewriterules/theory_rewriterules.h" +#include "theory/rewriterules/theory_rewriterules_params.h" + +namespace CVC4 { +namespace theory { +namespace rewriterules { + +inline std::ostream& operator <<(std::ostream& stream, const RewriteRule& r) { + r.toStream(stream); + return stream; +} + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H */ diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h new file mode 100644 index 000000000..5a0e8c5e0 --- /dev/null +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -0,0 +1,98 @@ +#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 { + +class RewriteRuleTypeRule { +public: + + /** + * Compute the type for (and optionally typecheck) a term belonging + * to the theory of rewriterules. + * + * @param check if true, the node's type should be checked as well + * as computed. + */ + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) + throw(TypeCheckingExceptionPrivate) { + Debug("typecheck-r") << "type check for rr " << n << std::endl; + Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); + if( check ){ + if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ + throw TypeCheckingExceptionPrivate(n, + "first argument of rewrite rule is not bound var list"); + } + if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n, + "guard of rewrite rule is not an actual guard"); + } + if( n[2].getType(check) != + TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){ + throw TypeCheckingExceptionPrivate(n, + "not a correct rewrite rule"); + } + } + return nodeManager->booleanType(); + } +};/* class RewriterulesTypeRule */ + + +class RRRewriteTypeRule { +public: + + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::RR_REWRITE ); + if( check ){ + if( n[0].getType(check)!=n[1].getType(check) ){ + throw TypeCheckingExceptionPrivate(n, + "terms of rewrite rule are not equal"); + } + if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ + throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); + } + if( n[0].getKind()!=kind::APPLY_UF ){ + throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); + } + } + return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); + } +};/* struct QuantifierReductionRuleRule */ + +class RRRedDedTypeRule { +public: + + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::RR_REDUCTION || + n.getKind() == kind::RR_DEDUCTION ); + if( check ){ + if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); + } + if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); + } + if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ + throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); + } + if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){ + throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); + } + } + return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); + } +};/* struct QuantifierReductionRuleRule */ + +}/* CVC4::theory::rewriterules namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H */ |