From dc6e0f9c0489e733a70e6715b8dfba4e7fa4f0bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Apr 2018 13:55:08 -0500 Subject: [PATCH] Core improvements to extended rewriter (#1820) --- src/theory/quantifiers/extended_rewrite.cpp | 67 ++++++++++++++++----- src/theory/quantifiers/extended_rewrite.h | 7 +++ src/theory/quantifiers/term_util.cpp | 5 ++ src/theory/quantifiers/term_util.h | 5 ++ 4 files changed, 70 insertions(+), 14 deletions(-) diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index dd21822ed..c52d22cdb 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -42,6 +42,20 @@ void ExtendedRewriter::setCache(Node n, Node ret) n.setAttribute(era, ret); } +bool ExtendedRewriter::addToChildren(Node nc, + std::vector& children, + bool dropDup) +{ + // If the operator is non-additive, do not consider duplicates + if (dropDup + && std::find(children.begin(), children.end(), nc) != children.end()) + { + return false; + } + children.push_back(nc); + return true; +} + Node ExtendedRewriter::extendedRewrite(Node n) { n = Rewriter::rewrite(n); @@ -97,19 +111,24 @@ Node ExtendedRewriter::extendedRewrite(Node n) Kind k = n.getKind(); bool childChanged = false; bool isNonAdditive = TermUtil::isNonAdditive(k); + bool isAssoc = TermUtil::isAssoc(k); for (unsigned i = 0; i < n.getNumChildren(); i++) { Node nc = extendedRewrite(n[i]); childChanged = nc != n[i] || childChanged; - // If the operator is non-additive, do not consider duplicates - if (isNonAdditive - && std::find(children.begin(), children.end(), nc) != children.end()) + if (isAssoc && nc.getKind() == n.getKind()) { - childChanged = true; + for (const Node& ncc : nc) + { + if (!addToChildren(ncc, children, isNonAdditive)) + { + childChanged = true; + } + } } - else + else if (!addToChildren(nc, children, isNonAdditive)) { - children.push_back(nc); + childChanged = true; } } Assert(!children.empty()); @@ -923,16 +942,16 @@ Node ExtendedRewriter::extendedRewriteEqChain( } // sorted right associative chain - bool has_const = false; - unsigned const_index = 0; + bool has_nvar = false; + unsigned nvar_index = 0; for (std::pair& cp : cstatus) { if (cp.second) { - if (cp.first.isConst()) + if (!cp.first.isVar()) { - has_const = true; - const_index = children.size(); + has_nvar = true; + nvar_index = children.size(); } children.push_back(cp.first); } @@ -943,7 +962,7 @@ Node ExtendedRewriter::extendedRewriteEqChain( if (!gpol) { // negate the constant child if it exists - unsigned nindex = has_const ? const_index : 0; + unsigned nindex = has_nvar ? nvar_index : 0; children[nindex] = TermUtil::mkNegate(notk, children[nindex]); } new_ret = children.back(); @@ -1051,12 +1070,32 @@ bool ExtendedRewriter::inferSubstitution(Node n, { n = slv_eq; } + NodeManager* nm = NodeManager::currentNM(); + + Node v[2]; for (unsigned i = 0; i < 2; i++) { - TNode r1 = n[i]; - TNode r2 = n[1 - i]; + if (n[i].isVar() || n[i].isConst()) + { + v[i] = n[i]; + } + else if (TermUtil::isNegate(n[i].getKind()) && n[i][0].isVar()) + { + v[i] = n[i][0]; + } + } + for (unsigned i = 0; i < 2; i++) + { + TNode r1 = v[i]; + Node r2 = v[1 - i]; if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst())) { + r2 = n[1 - i]; + if (v[i] != n[i]) + { + Assert( TermUtil::isNegate( n[i].getKind() ) ); + r2 = TermUtil::mkNegate(n[i].getKind(), r2); + } // TODO (#1706) : union find if (std::find(vars.begin(), vars.end(), r1) == vars.end()) { diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index bfae55730..937f522b2 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -66,6 +66,13 @@ class ExtendedRewriter bool d_aggr; /** cache that the extended rewritten form of n is ret */ void setCache(Node n, Node ret); + /** add to children + * + * Adds nc to the vector of children, if dropDup is true, we do not add + * nc if it already occurs in children. This method returns false in this + * case, otherwise it returns true. + */ + bool addToChildren(Node nc, std::vector& children, bool dropDup); //--------------------------------------generic utilities /** Rewrite ITE, for example: diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index a80737fe2..9b04ce9b5 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -811,6 +811,11 @@ Node TermUtil::mkNegate(Kind notk, Node n) return NodeManager::currentNM()->mkNode(notk, n); } +bool TermUtil::isNegate(Kind k) +{ + return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS; +} + bool TermUtil::isAssoc( Kind k ) { return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index df88c1b30..70f8bbcee 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -291,6 +291,11 @@ public: static int getTermDepth( Node n ); /** simple negate */ static Node simpleNegate( Node n ); + /** is the kind k a negation kind? + * + * A kind k is a negation kind if ( ( n ) ) = n. + */ + static bool isNegate(Kind k); /** * Make negated term, returns the negation of n wrt Kind notk, eliminating * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x. -- 2.30.2