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.

2 files changed, 251 insertions, 0 deletions

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<BvIteMergeThenElse>             rule137;
   RewriteRule<BvIteMergeElseElse>             rule138;
   RewriteRule<AndOrXorConcatPullUp>           rule139;
+  RewriteRule<NegEliminate> rule140;
+  RewriteRule<OrEliminate> rule141;
+  RewriteRule<XorEliminate> rule142;
+  RewriteRule<SdivEliminate> rule143;
+  RewriteRule<SremEliminate> rule144;
+  RewriteRule<SmodEliminate> 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<NegEliminate>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_NEG);
+}
+
+template <>
+inline Node RewriteRule<NegEliminate>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<NegEliminate>(" << 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<OrEliminate>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_OR);
+}
+
+template <>
+inline Node RewriteRule<OrEliminate>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<OrEliminate>(" << 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<XorEliminate>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_XOR);
+}
+
+template <>
+inline Node RewriteRule<XorEliminate>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<XorEliminate>(" << 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<UgtEliminate>::applies(TNode node)
 {
@@ -397,6 +477,47 @@ inline Node RewriteRule<SdivEliminate>::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<SdivEliminateFewerBitwiseOps>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_SDIV);
+}
+
+template <>
+inline Node RewriteRule<SdivEliminateFewerBitwiseOps>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<SdivEliminateFewerBitwiseOps>(" << 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<SremEliminate>::applies(TNode node)
 {
@@ -435,6 +556,45 @@ inline Node RewriteRule<SremEliminate>::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<SremEliminateFewerBitwiseOps>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_SREM);
+}
+
+template <>
+inline Node RewriteRule<SremEliminateFewerBitwiseOps>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<SremEliminateFewerBitwiseOps>(" << 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<SmodEliminate>::applies(TNode node)
 {
@@ -497,6 +657,73 @@ inline Node RewriteRule<SmodEliminate>::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<SmodEliminateFewerBitwiseOps>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_SMOD);
+}
+
+template <>
+inline Node RewriteRule<SmodEliminateFewerBitwiseOps>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << 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<ZeroExtendEliminate>::applies(TNode node)
 {