From: Aina Niemetz Date: Tue, 7 Aug 2018 18:22:05 +0000 (-0700) Subject: Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273) X-Git-Tag: cvc5-1.0.0~4809 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e1efe98961c87e96767ee362378b5573b49c2ff;p=cvc5.git Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273) --- diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index d8f360492..97284a01b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -108,6 +108,10 @@ enum RewriteRuleId BvIteEqualChildren, BvIteConstChildren, BvIteEqualCond, + BvIteMergeThenIf, + BvIteMergeElseIf, + BvIteMergeThenElse, + BvIteMergeElseElse, BvComp, ShlByConst, LshrByConst, @@ -249,6 +253,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BvIteEqualChildren : out << "BvIteEqualChildren"; return out; case BvIteConstChildren : out << "BvIteConstChildren"; return out; case BvIteEqualCond : out << "BvIteEqualCond"; return out; + case BvIteMergeThenIf : out << "BvIteMergeThenIf"; return out; + case BvIteMergeElseIf : out << "BvIteMergeElseIf"; return out; + case BvIteMergeThenElse : out << "BvIteMergeThenElse"; return out; + case BvIteMergeElseElse : out << "BvIteMergeElseElse"; return out; case BvComp : out << "BvComp"; return out; case ShlByConst : out << "ShlByConst"; return out; case LshrByConst : out << "LshrByConst"; return out; @@ -567,6 +575,10 @@ struct AllRewriteRules { RewriteRule rule132; RewriteRule rule133; RewriteRule rule134; + RewriteRule rule135; + RewriteRule rule136; + RewriteRule rule137; + RewriteRule rule138; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index a59f6524a..9df3a0cd5 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -125,6 +125,113 @@ inline Node RewriteRule::apply(TNode node) : node[2]; return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1); } + +/** + * BvIteMergeThenIf + * + * Nested BITVECTOR_ITE of the form + * c0 ? (c1 ? t1 : e1) : t1 -> c0 AND NOT(c1) ? e1 : t1 + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE + && node[1].getKind() == kind::BITVECTOR_ITE + && node[1][1] == node[2]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Assert(node[1].getKind() == kind::BITVECTOR_ITE); + Node cond = nm->mkNode(kind::BITVECTOR_AND, + node[0], + nm->mkNode(kind::BITVECTOR_NOT, node[1][0])); + return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]); +} + +/** + * BvIteMergeElseIf + * + * Nested BITVECTOR_ITE of the form + * c0 ? (c1 ? t1 : e1) : e1 -> c0 AND c1 ? t1 : e1 + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE + && node[1].getKind() == kind::BITVECTOR_ITE + && node[1][2] == node[2]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Assert(node[1].getKind() == kind::BITVECTOR_ITE); + Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]); + return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]); +} + +/** + * BvIteMergeThenElse + * + * Nested BITVECTOR_ITE of the form + * c0 ? t0 : (c1 ? t0 : e1) -> NOT(c0) AND NOT(c1) ? e1 : t0 + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE + && node[2].getKind() == kind::BITVECTOR_ITE + && node[1] == node[2][1]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Assert(node[2].getKind() == kind::BITVECTOR_ITE); + Node cond = nm->mkNode(kind::BITVECTOR_AND, + nm->mkNode(kind::BITVECTOR_NOT, node[0]), + nm->mkNode(kind::BITVECTOR_NOT, node[2][0])); + return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]); +} + +/** + * BvIteMergeElseElse + * + * Nested BITVECTOR_ITE of the form + * c0 ? t0 : (c1 ? t1 : t0) -> NOT(c0) AND c1 ? t1 : t0 + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE + && node[2].getKind() == kind::BITVECTOR_ITE + && node[1] == node[2][2]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Assert(node[2].getKind() == kind::BITVECTOR_ITE); + Node cond = nm->mkNode(kind::BITVECTOR_AND, + nm->mkNode(kind::BITVECTOR_NOT, node[0]), + node[2][0]); + return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]); +} + /** * BvComp * diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index d63fe4009..8b5d34cf4 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -173,7 +173,11 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) RewriteRule, RewriteRule, RewriteRule, - RewriteRule>::apply(node); + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule, + RewriteRule>::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); }