mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

reduce_invertible: recognize (* x -1) as the same as (- x)

Browse source
This commit is contained in:
Nuno Lopes 2020-03-31 10:54:03 +01:00
parent cf0952c232
commit 91497f923a
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -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<expr> 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);