From c8f823af1557b60770e73342504d1ee151e6a59f Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Wed, 30 Nov 2016 09:03:36 -0800 Subject: [PATCH] Add unit test for `MultDistrib` rule This unit test checks that the issue fixed by commit c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved. --- test/unit/theory/theory_engine_white.h | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) 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::applies(expr)) { + result = RewriteRule::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); + } }; -- 2.30.2