summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules')
-rw-r--r--src/theory/rewriterules/Makefile4
-rw-r--r--src/theory/rewriterules/Makefile.am19
-rw-r--r--src/theory/rewriterules/README.WHATS-NEXT29
-rw-r--r--src/theory/rewriterules/kinds37
-rw-r--r--src/theory/rewriterules/theory_rewriterules.cpp519
-rw-r--r--src/theory/rewriterules/theory_rewriterules.h264
-rw-r--r--src/theory/rewriterules/theory_rewriterules_params.h95
-rw-r--r--src/theory/rewriterules/theory_rewriterules_preprocess.h176
-rw-r--r--src/theory/rewriterules/theory_rewriterules_rewriter.h104
-rw-r--r--src/theory/rewriterules/theory_rewriterules_rules.cpp303
-rw-r--r--src/theory/rewriterules/theory_rewriterules_rules.h40
-rw-r--r--src/theory/rewriterules/theory_rewriterules_type_rules.h98
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback