diff options
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 7 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 18 |
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); } }; |