From c0c424283c12cfce2874ea92188487d91acecdf3 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Mon, 21 Nov 2016 18:07:45 -0800 Subject: [PATCH] Fix `MultDistrib` rewrite rule The assertion in the `MultDistrib` rule would fail when doing: ``` Node expr = d_nm->mkNode(BITVECTOR_MULT, mkNode(BITVECTOR_SUB, x, y), z); if (RewriteRule::applies(expr)) RewriteRule::apply(expr); ``` When checking which side to distribute over, the code only checked for `BITVECTOR_PLUS` instead of `BITVECTOR_PLUS` or `BITVECTOR_SUB` in contrast to the other conditions in `RewriteRule::applies()` and the assert. NOTE: I was only able to reproduce this issue when testing the rewrite rule in isolation. The rule `SubEliminate` generally seems to turn the `BITVECTOR_SUB` node into a `BITVECTOR_PLUS` node before the rewriter tries `MultDistrib`. --- src/theory/bv/theory_bv_rewrite_rules_normalization.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4abd02e73..89bb3d7ac 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -492,8 +492,10 @@ template<> inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - TNode factor = node[0].getKind() != kind::BITVECTOR_PLUS ? node[0] : node[1]; - TNode sum = node[0].getKind() == kind::BITVECTOR_PLUS? node[0] : node[1]; + bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS || + node[0].getKind() == kind::BITVECTOR_SUB; + TNode factor = !is_rhs_factor ? node[0] : node[1]; + TNode sum = is_rhs_factor ? node[0] : node[1]; Assert (factor.getKind() != kind::BITVECTOR_PLUS && factor.getKind() != kind::BITVECTOR_SUB && (sum.getKind() == kind::BITVECTOR_PLUS || -- 2.30.2