diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-30 09:03:36 -0800 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-30 09:03:36 -0800 |
commit | c8f823af1557b60770e73342504d1ee151e6a59f (patch) | |
tree | 4303bdad7ddfe7b1b119e8fd6f51538fe5404ab8 /test | |
parent | bc2378517a2f4100ba614cd44b3aa047089c82c8 (diff) |
Add unit test for `MultDistrib` rule
This unit test checks that the issue fixed by commit
c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 21 |
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); + } }; |