diff options
author | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
commit | 4bfa927dac67bbcadf219f70e61f1d123e33944b (patch) | |
tree | f295343430799748de8b9a823f1a3c641c096905 /src/theory/rewriterules | |
parent | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (diff) |
Merge quantifiers2-trunk:
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
Diffstat (limited to 'src/theory/rewriterules')
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.cpp | 328 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.h | 33 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_params.h | 14 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rules.cpp | 131 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_type_rules.h | 6 |
5 files changed, 358 insertions, 154 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 265026b39..57bc6d9cf 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -23,6 +23,8 @@ #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriter.h" +#include "util/options.h" + using namespace std; using namespace CVC4; @@ -30,6 +32,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rewriterules; +using namespace CVC4::theory::rrinst; namespace CVC4 { @@ -69,14 +72,14 @@ size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{ Node g = substNode(re,rule->guards[start],cache); switch(re.addWatchIfDontKnow(g,this,start)){ case ATRUE: - Debug("rewriterules") << g << "is true" << std::endl; + Debug("rewriterules::guards") << g << "is true" << std::endl; ++start; continue; case AFALSE: - Debug("rewriterules") << g << "is false" << std::endl; + Debug("rewriterules::guards") << g << "is false" << std::endl; return -1; case ADONTKNOW: - Debug("rewriterules") << g << "is unknown" << std::endl; + Debug("rewriterules::guards") << g << "is unknown" << std::endl; return start; } } @@ -132,31 +135,31 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c, 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_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false) { 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; + ++d_statistics.d_match_found; if(rewrite_instantiation) im.applyRewrite(); if(representative_instantiation) im.makeRepresentative( getQuantifiersEngine() ); if(!cache_match || !r->inCache(*this,im)){ ++r->nb_applied; + ++d_statistics.d_cache_miss; 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; + Debug("rewriterules::matching") << "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. @@ -168,6 +171,8 @@ void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, d_ruleinsts.push_back(ri); else delete(ri); }; + }else{ + ++d_statistics.d_cache_hit; }; } @@ -179,7 +184,11 @@ void TheoryRewriteRules::check(Effort level) { while(!done()) { // Get all the assertions // TODO: Test that it have already been ppAsserted - get(); + + //if we are here and ppAssert has not been done + // that means that ppAssert is off so we need to assert now + if(!d_ppAssert_on) addRewriteRule(get()); + else get(); // Assertion assertion = get(); // TNode fact = assertion.assertion; @@ -190,30 +199,30 @@ void TheoryRewriteRules::check(Effort level) { }; - Debug("rewriterules") << "Check:" << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl; + Debug("rewriterules::check") << "RewriteRules::Check start " << 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; + Debug("rewriterules::check") << "RewriteRules::Check 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 )){ + while(tr.getNextMatch()){ + InstMatch im = tr.getInstMatch(); addMatchRuleTrigger(r, im, true); - im.clear(); } } const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL; bool polldone = false; + if(level==EFFORT_FULL) ++d_statistics.d_full_check; + else ++d_statistics.d_check; + GuardedMap::const_iterator p = d_guardeds.begin(); do{ @@ -221,7 +230,7 @@ void TheoryRewriteRules::check(Effort level) { //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(simulateRewritting && ri->alreadyRewritten(*this)) continue; if(ri->findGuard(*this, 0) != ri->rule->guards.size()) d_ruleinsts.push_back(ri); else delete(ri); @@ -239,7 +248,7 @@ void TheoryRewriteRules::check(Effort level) { bool value; if(getValuation().hasSatValue(g,value)){ if(value) polldone = true; //One guard is true so pass n check - Debug("rewriterules") << "Poll value:" << g + Debug("rewriterules::guards") << "Poll value:" << g << " is " << (value ? "true" : "false") << std::endl; notification(g,value); //const Guarded & glast2 = (*l)[l->size()-1]; @@ -266,14 +275,14 @@ void TheoryRewriteRules::check(Effort level) { // 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; + Debug("rewriterules::check") << "RewriteRules::Check 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; + Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl; }; @@ -283,7 +292,13 @@ 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); + Options::current()->efficientEMatching? + Trigger::MATCH_GEN_EFFICIENT_E_MATCH : + Trigger::MATCH_GEN_DEFAULT, + true, + Trigger::TR_MAKE_NEW, + false); + // Options::current()->smartMultiTriggers); }; bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, @@ -299,9 +314,9 @@ bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, void TheoryRewriteRules::notification(GList * const lpropa, bool b){ if (b){ - for(GList::const_iterator g = lpropa->begin(); - g != lpropa->end(); ++g) { - (*g).nextGuard(*this); + for(size_t ig = 0; + ig != lpropa->size(); ++ig) { + (*lpropa)[ig].nextGuard(*this); }; lpropa->push_back(Guarded(RULEINST_TRUE,0)); }else{ @@ -315,16 +330,6 @@ void TheoryRewriteRules::notification(GList * const lpropa, bool b){ 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? */ - //AJR: removed this code after talking with Francois - ///* 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); @@ -384,68 +389,119 @@ void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) { }; +Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){ + Assert(conjunction.getKind() == kind::AND); + switch(conjunction.getNumChildren()){ + case 0: + return d_true; + case 1: + return conjunction[0]; + default: + return conjunction; + } + +} + +void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){ + 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(!inst->d_matched.isNull()); + Assert( inst->d_matched.getKind() == kind::APPLY_UF); + Assert( substHead.getKind() == kind::APPLY_UF ); + Assert( inst->d_matched.getOperator() == substHead.getOperator() ); + Assert(conjunction.getKind() == kind::AND); + // replace the left hand side by the term really matched + NodeBuilder<2> nb; + 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] << substHead[i]; + conjunction << static_cast<Node>(nb); + } +} + +Node skolemizeBody( Node f ){ + /*TODO skolemize the subformula of s with constant or skolemize + directly in the body of the rewrite rule with an uninterpreted + function. + */ + if ( f.getKind()!=EXISTS ) return f; + std::vector< Node > vars; + std::vector< Node > csts; + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + csts.push_back( NodeManager::currentNM()->mkSkolem( f[0][i].getType()) ); + vars.push_back( f[0][i] ); + } + return f[ 1 ].substitute( vars.begin(), vars.end(), + csts.begin(), csts.end() ); +} + + void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ // Debug("rewriterules") << "A rewrite rules is verified. Add lemma:"; - Debug("rewriterules") << "propagateRule" << *inst << std::endl; + Debug("rewriterules::propagate") << "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); + Node equality = skolemizeBody(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 + NodeBuilder<> conjunction(kind::AND); + explainInstantiation(inst, + rule->guards.size() > 0? + inst->substNode(*this,rule->guards[0],cache) : equality[0], + conjunction); 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)); + //rewrite rule + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + if(equality[1].getType(false) == booleanType) + equality = inst->d_matched.iffNode(equality[1]); + else equality = inst->d_matched.eqNode(equality[1]); + lemma = normalizeConjunction(conjunction).impNode(equality); Debug("rewriterules-directrr") << " -> " << lemma << std::endl; - }; - // Debug("rewriterules") << "lemma:" << lemma << std::endl; + } + else if(rule->guards.size() > 0){ + // We can use implication for reduction rules since the head is known + // to be true + NodeBuilder<> conjunction(kind::AND); + substGuards(inst,cache,conjunction); + lemma = normalizeConjunction(conjunction).impNode(equality); + } + Debug("rewriterules::propagate") << "propagated " << lemma << std::endl; getOutputChannel().lemma(lemma); }else{ - Assert(!direct_rewrite); - Node lemma_lit = getValuation().ensureLiteral(equality); + Node lemma_lit = equality; + if(rule->directrr && rule->guards.size() == 0) + lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules + lemma_lit = getValuation().ensureLiteral(lemma_lit); 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); + NodeBuilder<> conflict(kind::AND); + + if(rule->directrr){ + explainInstantiation(inst, + rule->guards.size() > 0? + inst->substNode(*this,rule->guards[0],cache) : equality[0], + conflict); + if(rule->guards.size() > 0){ + //reduction rule + Assert(rule->guards.size() == 1); + conflict << inst->d_matched; //this one will be two times + } + } + substGuards(inst,cache,conflict); + conflict << lemma_lit; + getOutputChannel().conflict(normalizeConjunction(conflict)); }; }else{ getOutputChannel().propagate(lemma_lit); @@ -456,57 +512,79 @@ void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ 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); + // for(std::vector<Node>::iterator i = rule->to_remove.begin(); + // i == rule->to_remove.end(); ++i){ + // (*i).setAttribute(rewrittenNodeAttribute,true); + // }; + for(size_t i = 0; i < rule->to_remove.size(); ++i){ + Node rewritten = inst->substNode(*this,rule->to_remove[i],cache); + Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl; + rewritten.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); + if ( compute_opt && !rule->body_match.empty() ){ + + uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + + //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; + // Use trigger2 since we can be in check + ApplyMatcher * tr = r->trigger_for_body_match; + Assert(tr != NULL); + tr->resetInstantiationRound(getQuantifiersEngine()); + InstMatch im; + TNode m = inst->substNode(*this,(*p).first, cache); + Assert( m.getKind() == kind::APPLY_UF ); + ee->addTerm(m); + if( tr->reset(m,im,getQuantifiersEngine()) ){ + im.d_matched = m; + Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl; + addMatchRuleTrigger(r, im); + } } + } }; - -Node TheoryRewriteRules::substGuards(const RuleInst *inst, +void TheoryRewriteRules::substGuards(const RuleInst *inst, TCache cache, - /* Already substituted */ - Node last){ + NodeBuilder<> & conjunction){ 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 ()); + RuleInst inst = (*p).second; + const RewriteRule * rule = inst.rule; + TCache cache; + NodeBuilder<> explanation(kind::AND); + if(rule->directrr){ + explainInstantiation(&inst, + rule->guards.size() > 0? + inst.substNode(*this,rule->guards[0],cache): + inst.substNode(*this,rule->body[0] ,cache), + explanation); + if(rule->guards.size() > 0){ + //reduction rule + Assert(rule->guards.size() == 1); + explanation << inst.d_matched; //this one will be two times + } + }; + substGuards(&inst, cache ,explanation); + return normalizeConjunction(explanation); } void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){ @@ -515,9 +593,39 @@ void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){ Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { addRewriteRule(in); + d_ppAssert_on = true; return PP_ASSERT_STATUS_UNSOLVED; } +TheoryRewriteRules::Statistics::Statistics(): + d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0), + d_check("TheoryRewriteRules::Check", 0), + d_full_check("TheoryRewriteRules::FullCheck", 0), + d_poll("TheoryRewriteRules::Poll", 0), + d_match_found("TheoryRewriteRules::MatchFound", 0), + d_cache_hit("TheoryRewriteRules::CacheHit", 0), + d_cache_miss("TheoryRewriteRules::CacheMiss", 0) +{ + StatisticsRegistry::registerStat(&d_num_rewriterules); + StatisticsRegistry::registerStat(&d_check); + StatisticsRegistry::registerStat(&d_full_check); + StatisticsRegistry::registerStat(&d_poll); + StatisticsRegistry::registerStat(&d_match_found); + StatisticsRegistry::registerStat(&d_cache_hit); + StatisticsRegistry::registerStat(&d_cache_miss); +} + +TheoryRewriteRules::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_num_rewriterules); + StatisticsRegistry::unregisterStat(&d_check); + StatisticsRegistry::unregisterStat(&d_full_check); + StatisticsRegistry::unregisterStat(&d_poll); + StatisticsRegistry::unregisterStat(&d_match_found); + StatisticsRegistry::unregisterStat(&d_cache_hit); + StatisticsRegistry::unregisterStat(&d_cache_miss); +} + + }/* 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 index d1c3eecf3..fcbdfe8b9 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -27,7 +27,9 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "context/context_mm.h" -#include "theory/inst_match_impl.h" +#include "theory/rr_inst_match_impl.h" +#include "theory/rr_trigger.h" +#include "theory/rr_inst_match.h" #include "util/stats.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/model.h" @@ -35,6 +37,8 @@ namespace CVC4 { namespace theory { namespace rewriterules { +using namespace CVC4::theory::rrinst; +typedef CVC4::theory::rrinst::Trigger Trigger; typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; @@ -45,6 +49,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; class RewriteRule{ public: // constant + const size_t id; //for debugging const bool d_split; mutable Trigger trigger; std::vector<Node> guards; @@ -58,7 +63,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; 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 + mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching // trigger when we need new match. // So currently we use another // trigger for that. @@ -70,7 +75,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; const bool directrr; RewriteRule(TheoryRewriteRules & re, - Trigger & tr, Trigger & tr2, + Trigger & tr, ApplyMatcher * tr2, std::vector<Node> & g, Node b, TNode nt, std::vector<Node> & fv,std::vector<Node> & iv, std::vector<Node> & to_r, bool drr); @@ -183,6 +188,7 @@ private: inside check */ typedef std::vector< RuleInst* > QRuleInsts; QRuleInsts d_ruleinsts_to_add; + bool d_ppAssert_on; //Indicate if a ppAssert have been done public: /** true and false for predicate */ @@ -240,15 +246,17 @@ private: already true */ bool notifyIfKnown(const GList * const ltested, GList * const lpropa); - Node substGuards(const RuleInst * inst, + void substGuards(const RuleInst * inst, TCache cache, - Node last = Node::null()); + NodeBuilder<> & conjunction); void addRewriteRule(const Node r); void computeMatchBody ( const RewriteRule * r, size_t start = 0); void addMatchRuleTrigger(const RewriteRule* r, InstMatch & im, bool delay = true); + Node normalizeConjunction(NodeBuilder<> & conjunction); + /* rewrite pattern */ typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite; RegisterRRPpRewrite d_registeredRRPpRewrite; @@ -257,6 +265,21 @@ private: rewriter::Subst & pvars, rewriter::Subst & vars); + /** statistics class */ + class Statistics { + public: + IntStat d_num_rewriterules; + IntStat d_check; + IntStat d_full_check; + IntStat d_poll; + IntStat d_match_found; + IntStat d_cache_hit; + IntStat d_cache_miss; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; + };/* class TheoryRewriteRules */ }/* CVC4::theory::rewriterules namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h index 9ab2ae3e7..de51215d1 100644 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -17,7 +17,6 @@ ** \todo document this file **/ - #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H @@ -58,7 +57,7 @@ static const bool representative_instantiation = false; Allow to break loop with other theories. */ -static const size_t checkSlowdown = 10; +static const size_t checkSlowdown = 0; /** Use the current model to eliminate guard before asking for notification @@ -68,14 +67,7 @@ static const bool useCurrentModel = false; /** Simulate rewriting 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; +static const bool simulateRewritting = true; /** Do narrowing at full effort @@ -85,7 +77,7 @@ static const bool narrowing_full_effort = false; /** Direct rewrite: Add rewrite rules directly in the rewriter. */ -static const bool direct_rewrite = true; +static const bool direct_rewrite = false; }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index c3116aba0..1ad8fdaa7 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -21,6 +21,7 @@ #include "theory/rewriterules/theory_rewriterules_params.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriterules/theory_rewriterules.h" +#include "util/options.h" #include "theory/quantifiers/term_database.h" @@ -30,12 +31,46 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rewriterules; +using namespace CVC4::theory::rrinst; namespace CVC4 { namespace theory { namespace rewriterules { +// TODO replace by a real dictionnary +// We should create a real substitution? slower more precise +// We don't do that often +bool nonunifiable( TNode t0, TNode pattern, const std::vector<Node> & vars){ + typedef std::vector<std::pair<TNode,TNode> > tstack; + tstack stack(1,std::make_pair(t0,pattern)); // t * pat + + while(!stack.empty()){ + const std::pair<TNode,TNode> p = stack.back(); stack.pop_back(); + const TNode & t = p.first; + const TNode & pat = p.second; + + // t or pat is a variable currently we consider that can match anything + if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; + if( pat.getKind() == INST_CONSTANT ) continue; + + // t and pat are nonunifiable + if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { + if(t == pat) continue; + else return true; + }; + if( t.getOperator() != pat.getOperator() ) return true; + + //put the children on the stack + for( size_t i=0; i < pat.getNumChildren(); i++ ){ + stack.push_back(std::make_pair(t[i],pat[i])); + }; + } + // The heuristic can't find non-unifiability + return false; +} + + void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule, size_t start){ std::vector<TNode> stack(1,rule->new_terms); @@ -50,9 +85,9 @@ void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule, 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)){ + if(r->d_split || r->trigger_for_body_match == NULL) continue; + //the split rules are not computed and the one with multi-pattern + if( !nonunifiable(t, r->trigger_for_body_match->d_pattern, rule->free_vars)){ rule->body_match.push_back(std::make_pair(t,r)); } } @@ -74,7 +109,10 @@ inline void addPattern(TheoryRewriteRules & re, TNode r){ if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF) tri = tri[0]; - pattern.push_back(re.getQuantifiersEngine()->getTermDatabase()-> + pattern.push_back( + Options::current()->rewriteRulesAsAxioms? + static_cast<Node>(tri): + re.getQuantifiersEngine()->getTermDatabase()-> convertNodeToPattern(tri,r,vars,inst_constants)); } @@ -106,6 +144,7 @@ bool checkPatternVars(const std::vector<Node> & pattern, void TheoryRewriteRules::addRewriteRule(const Node r) { Assert(r.getKind() == kind::REWRITE_RULE); + Kind rrkind = r[2].getKind(); /* Replace variables by Inst_* variable and tag the terms that contain them */ std::vector<Node> vars; @@ -125,16 +164,20 @@ void TheoryRewriteRules::addRewriteRule(const Node r) when fired */ /* shortcut */ TNode head = r[2][0]; - switch(r[2].getKind()){ + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + switch(rrkind){ case kind::RR_REWRITE: /* Equality */ to_remove.push_back(head); addPattern(*this,head,pattern,vars,inst_constants,r); - body = head.eqNode(body); + if(head.getType(false) == booleanType) body = head.iffNode(body); + else body = head.eqNode(body); break; case kind::RR_REDUCTION: /** Add head to remove */ - to_remove.push_back(head); + for(Node::iterator i = head.begin(); i != head.end(); ++i) { + to_remove.push_back(*i); + }; case kind::RR_DEDUCTION: /** Add head to guards and pattern */ switch(head.getKind()){ @@ -171,32 +214,65 @@ void TheoryRewriteRules::addRewriteRule(const Node r) }; /* Add the other triggers */ if( r[2].getNumChildren() >= 3 ) - for(Node::iterator i = r[2][2].begin(); i != r[2][2].end(); ++i) { + for(Node::iterator i = r[2][2][0].begin(); i != r[2][2][0].end(); ++i) { // todo test during typing that its a good term (no not, atom, or term...) - addPattern(*this,(*i)[0],pattern,vars,inst_constants,r); + addPattern(*this,*i,pattern,vars,inst_constants,r); }; // Assert(pattern.size() == 1, "currently only single pattern are supported"); + + + + + //If we convert to usual axioms + if(Options::current()->rewriteRulesAsAxioms){ + NodeBuilder<> forallB(kind::FORALL); + forallB << r[0]; + NodeBuilder<> guardsB(kind::AND); + guardsB.append(guards); + forallB << normalizeConjunction(guardsB).impNode(body); + NodeBuilder<> patternB(kind::INST_PATTERN); + patternB.append(pattern); + NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); + patternListB << static_cast<Node>(patternB); + forallB << static_cast<Node>(patternListB); + getOutputChannel().lemma((Node) forallB); + return; + } + + //turn all to propagate + // if(true){ + // NodeBuilder<> guardsB(kind::AND); + // guardsB.append(guards); + // body = normalizeConjunction(guardsB).impNode(body); + // guards.clear(); + // rrkind = kind::RR_DEDUCTION; + // } + + //Every variable must be seen in the pattern if (!checkPatternVars(pattern,inst_constants)){ - Warning() << "The rule" << r << + Warning() << Node::setdepth(-1) << "The rule" << r << " has been removed since it doesn't contain every variables." << std::endl; return; } + //Add to direct rewrite rule bool directrr = false; if(direct_rewrite && - ((guards.size() == 0 && r[2].getKind() == kind::RR_REWRITE) || - (guards.size() == 1 && r[2].getKind() == kind::RR_REDUCTION)) + guards.size() == 0 && rrkind == kind::RR_REWRITE && pattern.size() == 1){ directrr = addRewritePattern(pattern[0],new_terms, inst_constants, vars); } + // final construction Trigger trigger = createTrigger(r,pattern); - Trigger trigger2 = createTrigger(r,pattern); //Hack - RewriteRule * rr = new RewriteRule(*this, trigger, trigger2, + ApplyMatcher * applymatcher = + pattern.size() == 1 && pattern[0].getKind() == kind::APPLY_UF? + new ApplyMatcher(pattern[0],getQuantifiersEngine()) : NULL; + RewriteRule * rr = new RewriteRule(*this, trigger, applymatcher, guards, body, new_terms, vars, inst_constants, to_remove, directrr); @@ -209,7 +285,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) computeMatchBody(d_rules[rid], d_rules.size() - 1); - Debug("rewriterules") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")" + Debug("rewriterules::new") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")" << *rr << std::endl; } @@ -227,7 +303,7 @@ bool willDecide(TNode node, bool positive = true){ case XOR: return true; case IMPLIES: - return false; + return true; case ITE: return true; case NOT: @@ -237,45 +313,50 @@ bool willDecide(TNode node, bool positive = true){ } } - +static size_t id_next = 0; RewriteRule::RewriteRule(TheoryRewriteRules & re, - Trigger & tr, Trigger & tr2, + Trigger & tr, ApplyMatcher * applymatcher, std::vector<Node> & g, Node b, TNode nt, std::vector<Node> & fv,std::vector<Node> & iv, std::vector<Node> & to_r, bool drr) : - d_split(willDecide(b)), + id(++id_next), d_split(willDecide(b)), trigger(tr), body(b), new_terms(nt), free_vars(), inst_vars(), - body_match(re.getSatContext()),trigger_for_body_match(tr2), + body_match(re.getSatContext()),trigger_for_body_match(applymatcher), d_cache(re.getSatContext(),re.getQuantifiersEngine()), directrr(drr){ free_vars.swap(fv); inst_vars.swap(iv); guards.swap(g); to_remove.swap(to_r); }; bool RewriteRule::inCache(TheoryRewriteRules & re, InstMatch & im)const{ - return !d_cache.addInstMatch(im); + bool res = !d_cache.addInstMatch(im); + Debug("rewriterules::matching") << "rewriterules::cache " << im + << (res ? " HIT" : " MISS") << std::endl; + return res; }; /** A rewrite rule */ void RewriteRule::toStream(std::ostream& out) const{ + out << "[" << id << "] "; for(std::vector<Node>::const_iterator iter = guards.begin(); iter != guards.end(); ++iter){ out << *iter; }; out << "=>" << body << std::endl; - out << "["; + out << "{"; for(BodyMatch::const_iterator iter = body_match.begin(); iter != body_match.end(); ++iter){ - out << (*iter).first << "(" << (*iter).second << ")" << ","; + out << (*iter).first << "[" << (*iter).second->id << "]" << ","; }; - out << "]" << (directrr?"*":"") << std::endl; + out << "}" << (directrr?"*":"") << std::endl; } RewriteRule::~RewriteRule(){ - Debug("rewriterule-stats") << *this + Debug("rewriterule::stats") << *this << " (" << nb_matched << "," << nb_applied << "," << nb_propagated << ")" << std::endl; + delete(trigger_for_body_match); } bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index 8bc4522a1..605324b20 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -45,16 +45,16 @@ public: Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[0], "first argument of rewrite rule is not bound var list"); } if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[1], "guard of rewrite rule is not an actual guard"); } if( n[2].getType(check) != TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[2], "not a correct rewrite rule"); } } |