From: Andres Notzli <andres.noetzli@gmail.com>
Date: Thu, 8 Dec 2016 22:21:28 +0000 (-0800)
Subject: Fix (inactive) `MultSlice` rewrite
X-Git-Tag: cvc5-1.0.0~5942^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=762c8a3cf028fa7c12c2ee32d8643bd73ff2f07c;p=cvc5.git

Fix (inactive) `MultSlice` rewrite

The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.
---

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 6ef591760..871380467 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1108,13 +1108,10 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<MultSlice>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_MULT) {
+  if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) {
     return false; 
   }
-  if (utils::getSize(node[0]) % 2 != 0) {
-    return false; 
-  }
-  return true; 
+  return utils::getSize(node[0]) % 2 == 0;
 }
 
 /** 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 978440576..9775dca1b 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -33,6 +33,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -442,6 +443,21 @@ public:
     Node expected =
         d_nm->mkNode(BITVECTOR_SUB, d_nm->mkNode(BITVECTOR_MULT, x, z),
                      d_nm->mkNode(BITVECTOR_MULT, y, z));
-    TS_ASSERT(result == expected);
+    TS_ASSERT_EQUALS(result, expected);
+
+    // Try to apply MultSlice to a multiplication of two and three different
+    // variables, expect different results (x * y and x * y * z should not get
+    // rewritten to the same term).
+    expr = d_nm->mkNode(BITVECTOR_MULT, x, y, z);
+    result = expr;
+    Node expr2 = d_nm->mkNode(BITVECTOR_MULT, x, y);
+    Node result2 = expr;
+    if (RewriteRule<MultSlice>::applies(expr)) {
+      result = RewriteRule<MultSlice>::apply(expr);
+    }
+    if (RewriteRule<MultSlice>::applies(expr2)) {
+      result2 = RewriteRule<MultSlice>::apply(expr2);
+    }
+    TS_ASSERT_DIFFERS(result, result2);
   }
 };