Merge pull request #116 from 4tXJ7f/fix_mult

Fix (inactive) `MultSlice` rewrite

2 files changed, 19 insertions, 6 deletions

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);
   }
 };