From 2fb5ff63e8e80b06450a8a2a33d7d61cc0a0e2ac Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 3 Aug 2020 15:28:29 -0700 Subject: [PATCH] New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769) This PR adds new rewrite rules for BV. None of them is meant to be used by the default BV rewriter. However, they are planned to be used in bv_to_int preprocessing pass. In the pass we use FixpointRewriteStrategy to call various rewrite rules. After consulting @4tXJ7f , we thought that the best way to include more rewrite rules in that call is to implement them using the existing BV rewrites infrastructure. --- src/theory/bv/theory_bv_rewrite_rules.h | 24 ++ ...ry_bv_rewrite_rules_operator_elimination.h | 227 ++++++++++++++++++ 2 files changed, 251 insertions(+) diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 6e7fb37d0..faebe9cfd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -66,9 +66,12 @@ enum RewriteRuleId NorEliminate, XnorEliminate, SdivEliminate, + SdivEliminateFewerBitwiseOps, UdivEliminate, SmodEliminate, + SmodEliminateFewerBitwiseOps, SremEliminate, + SremEliminateFewerBitwiseOps, ZeroExtendEliminate, SignExtendEliminate, BVToNatEliminate, @@ -120,6 +123,9 @@ enum RewriteRuleId AndZero, AndOne, AndOrXorConcatPullUp, + NegEliminate, + OrEliminate, + XorEliminate, OrZero, OrOne, XorDuplicate, @@ -202,6 +208,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ConcatExtractMerge: out << "ConcatExtractMerge"; return out; case ConcatConstantMerge: out << "ConcatConstantMerge"; return out; case AndOrXorConcatPullUp:out << "AndOrXorConcatPullUp";return out; + case NegEliminate: out << "NegEliminate"; return out; + case OrEliminate: out << "OrEliminate"; return out; + case XorEliminate: out << "XorEliminate"; return out; case ExtractExtract: out << "ExtractExtract"; return out; case ExtractWhole: out << "ExtractWhole"; return out; case ExtractConcat: out << "ExtractConcat"; return out; @@ -223,8 +232,17 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case NandEliminate: out << "NandEliminate"; return out; case NorEliminate : out << "NorEliminate"; return out; case SdivEliminate : out << "SdivEliminate"; return out; + case SdivEliminateFewerBitwiseOps: + out << "SdivEliminateFewerBitwiseOps"; + return out; case SremEliminate : out << "SremEliminate"; return out; + case SremEliminateFewerBitwiseOps: + out << "SremEliminateFewerBitwiseOps"; + return out; case SmodEliminate : out << "SmodEliminate"; return out; + case SmodEliminateFewerBitwiseOps: + out << "SmodEliminateFewerBitwiseOps"; + return out; case ZeroExtendEliminate :out << "ZeroExtendEliminate"; return out; case EvalEquals : out << "EvalEquals"; return out; case EvalConcat : out << "EvalConcat"; return out; @@ -585,6 +603,12 @@ struct AllRewriteRules { RewriteRule rule137; RewriteRule rule138; RewriteRule rule139; + RewriteRule rule140; + RewriteRule rule141; + RewriteRule rule142; + RewriteRule rule143; + RewriteRule rule144; + RewriteRule rule145; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 3ff3a88b3..610fff2ef 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -27,6 +27,86 @@ namespace CVC4 { namespace theory { namespace bv { +/* + * This rewrite is not meant to be used by the BV rewriter. + * It is specifically designed for the bv-to-int preprocessing pass. + * Based on Hacker's Delight section 2-2 equation a: + * -x = ~x+1 + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_NEG); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + unsigned size = utils::getSize(a); + Node one = utils::mkOne(size); + Node nota = nm->mkNode(kind::BITVECTOR_NOT, a); + Node bvadd = + nm->mkNode(kind::BITVECTOR_PLUS, nota, one); + return bvadd; +} + +/* + * This rewrite is not meant to be used by the BV rewriter. + * It is specifically designed for the bv-to-int preprocessing pass. + * Based on Hacker's Delight section 2-2 equation h: + * x+y = x|y + x&y + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_OR); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + Node bvadd = nm->mkNode(kind::BITVECTOR_PLUS, a, b); + Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); + Node result = + nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand); + return result; +} + +/* + * This rewrite is not meant to be used by the BV rewriter. + * It is specifically designed for the bv-to-int preprocessing pass. + * Based on Hacker's Delight section 2-2 equation n: + * x xor y = x|y - x&y + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_XOR); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + Node bvor = nm->mkNode(kind::BITVECTOR_OR, a, b); + Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); + Node result = nm->mkNode(kind::BITVECTOR_SUB, bvor, bvand); + return result; +} + template <> inline bool RewriteRule::applies(TNode node) { @@ -397,6 +477,47 @@ inline Node RewriteRule::apply(TNode node) return result; } +/* + * This rewrite is not meant to be used by the BV rewriter + * It is specifically designed for the bv-to-int preprocessing pass. + * Similar to ordinary sdiv elimination. + * The sign-check is done with bvult instead of bit-extraction. + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_SDIV); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node + << ")" << std::endl; + + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + unsigned size = utils::getSize(a); + Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size)); + Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size)); + Node abs_a = + nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = + nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_udiv_b = + nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL + : kind::BITVECTOR_UDIV, + abs_a, + abs_b); + Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); + + Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b); + + return result; +} + template <> inline bool RewriteRule::applies(TNode node) { @@ -435,6 +556,45 @@ inline Node RewriteRule::apply(TNode node) return result; } +/* + * This rewrite is not meant to be used by the BV rewriter + * It is specifically designed for the bv-to-int preprocessing pass. + * Similar to ordinary srem elimination. + * The sign-check is done with bvult instead of bit-extraction. + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_SREM); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node + << ")" << std::endl; + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + unsigned size = utils::getSize(a); + Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size)); + Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size)); + Node abs_a = + nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = + nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); + Node a_urem_b = + nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL + : kind::BITVECTOR_UREM, + abs_a, + abs_b); + Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); + + Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); + + return result; +} + template <> inline bool RewriteRule::applies(TNode node) { @@ -497,6 +657,73 @@ inline Node RewriteRule::apply(TNode node) return result; } +/* + * This rewrite is not meant to be used by the BV rewriter + * It is specifically designed for the bv-to-int preprocessing pass. + * Similar to ordinary smod elimination. + * The sign-check is done with bvult instead of bit-extraction. + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_SMOD); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + NodeManager* nm = NodeManager::currentNM(); + TNode s = node[0]; + TNode t = node[1]; + unsigned size = utils::getSize(s); + + /* + * (bvsmod s t) abbreviates + * (let ((?msb_s ((_ extract |m-1| |m-1|) s)) + * (?msb_t ((_ extract |m-1| |m-1|) t))) + * (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s))) + * (abs_t (ite (= ?msb_t #b0) t (bvneg t)))) + * (let ((u (bvurem abs_s abs_t))) + * (ite (= u (_ bv0 m)) + * u + * (ite (and (= ?msb_s #b0) (= ?msb_t #b0)) + * u + * (ite (and (= ?msb_s #b1) (= ?msb_t #b0)) + * (bvadd (bvneg u) t) + * (ite (and (= ?msb_s #b0) (= ?msb_t #b1)) + * (bvadd u t) + * (bvneg u)))))))) + */ + + Node s_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, s, utils::mkMinSigned(size)); + Node t_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, t, utils::mkMinSigned(size)); + Node abs_s = + nm->mkNode(kind::ITE, s_lt_0, nm->mkNode(kind::BITVECTOR_NEG, s), s); + Node abs_t = + nm->mkNode(kind::ITE, t_lt_0, nm->mkNode(kind::BITVECTOR_NEG, t), t); + + Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t); + Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u); + + Node cond0 = u.eqNode(utils::mkConst(size, 0)); + Node cond1 = + nm->mkNode(kind::NOT, s_lt_0).andNode(nm->mkNode(kind::NOT, t_lt_0)); + Node cond2 = s_lt_0.andNode(nm->mkNode(kind::NOT, t_lt_0)); + Node cond3 = nm->mkNode(kind::NOT, s_lt_0).andNode(t_lt_0); + + Node result = cond0.iteNode( + u, + cond1.iteNode( + u, + cond2.iteNode( + nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t), + cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u)))); + + return result; +} + template <> inline bool RewriteRule::applies(TNode node) { -- 2.30.2