Add unit test for `MultDistrib` rule

This unit test checks that the issue fixed by commit
c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved.

1 files changed, 21 insertions, 0 deletions

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 1c19a847c..978440576 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -32,6 +32,7 @@
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -45,6 +46,7 @@ using namespace CVC4::expr;
 using namespace CVC4::context;
 using namespace CVC4::kind;
 using namespace CVC4::smt;
+using namespace CVC4::theory::bv;
 
 using namespace std;
 
@@ -423,4 +425,23 @@ public:
     // assert that the rewritten node is what we expect
 //    TS_ASSERT_EQUALS(nOut, nExpected);
   }
+
+  void testRewriterRules() {
+    TypeNode t = d_nm->mkBitVectorType(8);
+    Node x = d_nm->mkVar("x", t);
+    Node y = d_nm->mkVar("y", t);
+    Node z = d_nm->mkVar("z", t);
+
+    // (x - y) * z --> (x * z) - (y * z)
+    Node expr =
+        d_nm->mkNode(BITVECTOR_MULT, d_nm->mkNode(BITVECTOR_SUB, x, y), z);
+    Node result = expr;
+    if (RewriteRule<MultDistrib>::applies(expr)) {
+      result = RewriteRule<MultDistrib>::apply(expr);
+    }
+    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);
+  }
 };