From 1b0aa1c39ff7abe15bbd9305d376d10b007d69d0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 12 Feb 2018 18:16:59 -0600 Subject: [PATCH] Option to use extended rewriter as a preprocessing pass (#1600) --- src/options/smt_options | 5 + src/smt/smt_engine.cpp | 10 + src/theory/quantifiers/extended_rewrite.cpp | 315 +++++++++--------- src/theory/quantifiers/extended_rewrite.h | 15 +- .../quantifiers/term_database_sygus.cpp | 2 +- 5 files changed, 185 insertions(+), 162 deletions(-) diff --git a/src/options/smt_options b/src/options/smt_options index b19420060..72189ea13 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -70,6 +70,11 @@ option doITESimp --ite-simp bool :read-write option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false do the ite simplification pass again if repeating simplification + +option extRewPrep --ext-rew-prep bool :read-write :default false + use extended rewriter as a preprocessing pass +option extRewPrepAgg --ext-rew-prep-agg bool :read-write :default false + use aggressive extended rewriter as a preprocessing pass option simplifyWithCareEnabled --simp-with-care bool :default false :read-write enables simplifyWithCare in ite simplificiation diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fdd72ba2e..7e2f6c38c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4293,6 +4293,16 @@ void SmtEnginePrivate::processAssertions() { bool noConflict = true; + if (options::extRewPrep()) + { + theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); + for (unsigned i = 0; i < d_assertions.size(); ++i) + { + Node a = d_assertions[i]; + d_assertions.replace(i, extr.extendedRewrite(a)); + } + } + // Unconstrained simplification if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index ba0860d38..dd4fc86ba 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -ExtendedRewriter::ExtendedRewriter() +ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -76,8 +76,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Node n) Trace("q-ext-rewrite") << "sygus-extr : " << n << " rewrites to " << nc << " by simple ITE pulling." << std::endl; - // recurse - return extendedRewrite(nc); + return nc; } } } @@ -87,205 +86,201 @@ Node ExtendedRewriter::extendedRewritePullIte(Node n) Node ExtendedRewriter::extendedRewrite(Node n) { + n = Rewriter::rewrite(n); std::unordered_map::iterator it = d_ext_rewrite_cache.find(n); - if (it == d_ext_rewrite_cache.end()) + if (it != d_ext_rewrite_cache.end()) { - Node ret = n; - if (n.getNumChildren() > 0) + return it->second; + } + Node ret = n; + if (n.getNumChildren() > 0) + { + std::vector children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - std::vector children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) - { - children.push_back(n.getOperator()); - } - bool childChanged = false; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - Node nc = extendedRewrite(n[i]); - childChanged = nc != n[i] || childChanged; - children.push_back(nc); - } - // Some commutative operators have rewriters that are agnostic to order, - // thus, we sort here. - if (TermUtil::isComm(n.getKind())) - { - childChanged = true; - std::sort(children.begin(), children.end()); - } - if (childChanged) - { - ret = NodeManager::currentNM()->mkNode(n.getKind(), children); - } + children.push_back(n.getOperator()); } - ret = Rewriter::rewrite(ret); - Trace("q-ext-rewrite-debug") << "Do extended rewrite on : " << ret - << " (from " << n << ")" << std::endl; + bool childChanged = false; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + Node nc = extendedRewrite(n[i]); + childChanged = nc != n[i] || childChanged; + children.push_back(nc); + } + // Some commutative operators have rewriters that are agnostic to order, + // thus, we sort here. + if (TermUtil::isComm(n.getKind()) && (d_aggr || children.size() <= 5)) + { + childChanged = true; + std::sort(children.begin(), children.end()); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + } + } + ret = Rewriter::rewrite(ret); + Trace("q-ext-rewrite-debug") << "Do extended rewrite on : " << ret + << " (from " << n << ")" << std::endl; - Node new_ret; - if (ret.getKind() == kind::EQUAL) + Node new_ret; + if (ret.getKind() == kind::EQUAL) + { + if (new_ret.isNull()) { - if (new_ret.isNull()) - { - // simple ITE pulling - new_ret = extendedRewritePullIte(ret); - } + // simple ITE pulling + new_ret = extendedRewritePullIte(ret); + } + } + else if (ret.getKind() == kind::ITE) + { + Assert(ret[1] != ret[2]); + if (ret[0].getKind() == NOT) + { + ret = NodeManager::currentNM()->mkNode( + kind::ITE, ret[0][0], ret[2], ret[1]); } - else if (ret.getKind() == kind::ITE) + if (ret[0].getKind() == kind::EQUAL) { - Assert(ret[1] != ret[2]); - if (ret[0].getKind() == NOT) + // simple invariant ITE + for (unsigned i = 0; i < 2; i++) { - ret = NodeManager::currentNM()->mkNode( - kind::ITE, ret[0][0], ret[2], ret[1]); + if (ret[1] == ret[0][i] && ret[2] == ret[0][1 - i]) + { + Trace("q-ext-rewrite") + << "sygus-extr : " << ret << " rewrites to " << ret[2] + << " due to simple invariant ITE." << std::endl; + new_ret = ret[2]; + break; + } } - if (ret[0].getKind() == kind::EQUAL) + // notice this is strictly more general than the above + if (new_ret.isNull()) { - // simple invariant ITE + // simple substitution for (unsigned i = 0; i < 2; i++) { - if (ret[1] == ret[0][i] && ret[2] == ret[0][1 - i]) + TNode r1 = ret[0][i]; + TNode r2 = ret[0][1 - i]; + if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst())) { - Trace("q-ext-rewrite") << "sygus-extr : " << ret << " rewrites to " - << ret[2] << " due to simple invariant ITE." - << std::endl; - new_ret = ret[2]; - break; - } - } - // notice this is strictly more general than the above - if (new_ret.isNull()) - { - // simple substitution - for (unsigned i = 0; i < 2; i++) - { - TNode r1 = ret[0][i]; - TNode r2 = ret[0][1 - i]; - if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst())) + Node retn = ret[1].substitute(r1, r2); + if (retn != ret[1]) { - Node retn = ret[1].substitute(r1, r2); - if (retn != ret[1]) - { - new_ret = NodeManager::currentNM()->mkNode( - kind::ITE, ret[0], retn, ret[2]); - Trace("q-ext-rewrite") - << "sygus-extr : " << ret << " rewrites to " << new_ret - << " due to simple ITE substitution." << std::endl; - } + new_ret = NodeManager::currentNM()->mkNode( + kind::ITE, ret[0], retn, ret[2]); + Trace("q-ext-rewrite") + << "sygus-extr : " << ret << " rewrites to " << new_ret + << " due to simple ITE substitution." << std::endl; } } } } } - else if (ret.getKind() == DIVISION || ret.getKind() == INTS_DIVISION - || ret.getKind() == INTS_MODULUS) + } + else if (ret.getKind() == DIVISION || ret.getKind() == INTS_DIVISION + || ret.getKind() == INTS_MODULUS) + { + // rewrite as though total + std::vector children; + bool all_const = true; + for (unsigned i = 0; i < ret.getNumChildren(); i++) { - // rewrite as though total - std::vector children; - bool all_const = true; - for (unsigned i = 0; i < ret.getNumChildren(); i++) + if (ret[i].isConst()) { - if (ret[i].isConst()) - { - children.push_back(ret[i]); - } - else - { - all_const = false; - break; - } + children.push_back(ret[i]); } - if (all_const) + else { - Kind new_k = - (ret.getKind() == DIVISION - ? DIVISION_TOTAL - : (ret.getKind() == INTS_DIVISION ? INTS_DIVISION_TOTAL - : INTS_MODULUS_TOTAL)); - new_ret = NodeManager::currentNM()->mkNode(new_k, children); - Trace("q-ext-rewrite") << "sygus-extr : " << ret << " rewrites to " - << new_ret << " due to total interpretation." - << std::endl; + all_const = false; + break; } } - // more expensive rewrites - if (new_ret.isNull()) + if (all_const) { - Trace("q-ext-rewrite-debug2") << "Do expensive rewrites on " << ret - << std::endl; - bool polarity = ret.getKind() != NOT; - Node ret_atom = ret.getKind() == NOT ? ret[0] : ret; - if ((ret_atom.getKind() == EQUAL && ret_atom[0].getType().isReal()) - || ret_atom.getKind() == GEQ) + Kind new_k = (ret.getKind() == DIVISION ? DIVISION_TOTAL + : (ret.getKind() == INTS_DIVISION + ? INTS_DIVISION_TOTAL + : INTS_MODULUS_TOTAL)); + new_ret = NodeManager::currentNM()->mkNode(new_k, children); + Trace("q-ext-rewrite") + << "sygus-extr : " << ret << " rewrites to " << new_ret + << " due to total interpretation." << std::endl; + } + } + // more expensive rewrites + if (new_ret.isNull() && d_aggr) + { + new_ret = extendedRewriteAggr(ret); + } + + d_ext_rewrite_cache[n] = ret; + if (!new_ret.isNull()) + { + ret = extendedRewrite(new_ret); + } + d_ext_rewrite_cache[n] = ret; + return ret; +} + +Node ExtendedRewriter::extendedRewriteAggr(Node n) +{ + Node new_ret; + Trace("q-ext-rewrite-debug2") + << "Do aggressive rewrites on " << n << std::endl; + bool polarity = n.getKind() != NOT; + Node ret_atom = n.getKind() == NOT ? n[0] : n; + if ((ret_atom.getKind() == EQUAL && ret_atom[0].getType().isReal()) + || ret_atom.getKind() == GEQ) + { + Trace("q-ext-rewrite-debug2") + << "Compute monomial sum " << ret_atom << std::endl; + // compute monomial sum + std::map msum; + if (ArithMSum::getMonomialSumLit(ret_atom, msum)) + { + for (std::map::iterator itm = msum.begin(); itm != msum.end(); + ++itm) { - Trace("q-ext-rewrite-debug2") << "Compute monomial sum " << ret_atom - << std::endl; - // compute monomial sum - std::map msum; - if (ArithMSum::getMonomialSumLit(ret_atom, msum)) + Node v = itm->first; + Trace("q-ext-rewrite-debug2") + << itm->first << " * " << itm->second << std::endl; + if (v.getKind() == ITE) { - for (std::map::iterator itm = msum.begin(); - itm != msum.end(); - ++itm) + Node veq; + int res = ArithMSum::isolate(v, msum, veq, ret_atom.getKind()); + if (res != 0) { - Node v = itm->first; - Trace("q-ext-rewrite-debug2") << itm->first << " * " << itm->second - << std::endl; - if (v.getKind() == ITE) + Trace("q-ext-rewrite-debug") + << " have ITE relation, solved form : " << veq << std::endl; + // try pulling ITE + new_ret = extendedRewritePullIte(veq); + if (!new_ret.isNull()) { - Node veq; - int res = ArithMSum::isolate(v, msum, veq, ret_atom.getKind()); - if (res != 0) + if (!polarity) { - Trace("q-ext-rewrite-debug") - << " have ITE relation, solved form : " << veq - << std::endl; - // try pulling ITE - new_ret = extendedRewritePullIte(veq); - if (!new_ret.isNull()) - { - if (!polarity) - { - new_ret = new_ret.negate(); - } - break; - } - } - else - { - Trace("q-ext-rewrite-debug") << " failed to isolate " << v - << " in " << ret << std::endl; + new_ret = new_ret.negate(); } + break; } } - } - else - { - Trace("q-ext-rewrite-debug") << " failed to get monomial sum of " - << ret << std::endl; + else + { + Trace("q-ext-rewrite-debug") + << " failed to isolate " << v << " in " << n << std::endl; + } } } - else if (ret_atom.getKind() == ITE) - { - // TODO : conditional rewriting - } - else if (ret.getKind() == kind::AND || ret.getKind() == kind::OR) - { - // TODO condition merging - } } - - if (!new_ret.isNull()) + else { - ret = Rewriter::rewrite(new_ret); + Trace("q-ext-rewrite-debug") + << " failed to get monomial sum of " << n << std::endl; } - d_ext_rewrite_cache[n] = ret; - return ret; - } - else - { - return it->second; } + // TODO (#1599) : conditional rewriting, condition merging + return new_ret; } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 3a9fdb918..25d710a6b 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -43,12 +43,23 @@ namespace quantifiers { class ExtendedRewriter { public: - ExtendedRewriter(); + ExtendedRewriter(bool aggr = true); ~ExtendedRewriter() {} /** return the extended rewritten form of n */ Node extendedRewrite(Node n); private: + /** + * Whether this extended rewriter applies aggressive rewriting techniques, + * which are more expensive. Examples of aggressive rewriting include: + * - conditional rewriting, + * - condition merging, + * - sorting childing of commutative operators with more than 5 children. + * + * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting + * may be applied as a preprocessing step. + */ + bool d_aggr; /** true and false nodes */ Node d_true; Node d_false; @@ -62,6 +73,8 @@ class ExtendedRewriter * where ---->^E denotes extended rewriting. */ Node extendedRewritePullIte(Node n); + /** extended rewrite aggressive */ + Node extendedRewriteAggr(Node n); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index cda652ee7..4c80108f1 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -33,7 +33,7 @@ namespace quantifiers { TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) : d_quantEngine(qe), d_syexp(new SygusExplain(this)), - d_ext_rw(new ExtendedRewriter) + d_ext_rw(new ExtendedRewriter(true)) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); -- 2.30.2