From 91497f923ac1c810cc38e5ed5075003497580491 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 31 Mar 2020 10:54:03 +0100 Subject: [PATCH] reduce_invertible: recognize (* x -1) as the same as (- x) --- src/tactic/core/reduce_invertible_tactic.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 5467e3af6..f7c0dadbf 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -105,6 +105,17 @@ private: throw tactic_exception(m.limit().get_cancel_msg()); } + bool is_bv_neg(expr * e) { + if (m_bv.is_bv_neg(e)) + return true; + + expr *a, *b; + if (m_bv.is_bv_mul(e, a, b)) { + return m_bv.is_allone(a) || m_bv.is_allone(b); + } + return false; + } + expr_mark m_inverted; void mark_inverted(expr *p) { ptr_buffer todo; @@ -256,7 +267,7 @@ private: if (m_bv.is_bv_xor(p) || m_bv.is_bv_not(p) || - m_bv.is_bv_neg(p)) { + is_bv_neg(p)) { if (mc) { ensure_mc(mc); (*mc)->add(v, p);