summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules/theory_rewriterules.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.cpp')
-rw-r--r--src/theory/rewriterules/theory_rewriterules.cpp519
1 files changed, 519 insertions, 0 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback