From c04a5884ff2667905a2bce778ea1cba6ec61fa2a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 17 Feb 2025 16:56:30 +0000 Subject: [PATCH] simplify: rewrite bitxnor on booleans to equal This adds the rewrite (a xnor b) --> (a = b) for booleans a, b to the simplifier. --- src/util/simplify_expr_int.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 97fb7242e1e..aad92696471 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -696,6 +696,8 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) new_expr.id(ID_or); else if(expr.id()==ID_bitxor) new_expr.id(ID_xor); + else if(expr.id() == ID_bitxnor) + new_expr.id(ID_equal); else UNREACHABLE; @@ -709,8 +711,8 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) *it=true_exprt(); } - new_expr.type()=bool_typet(); - new_expr = simplify_boolean(new_expr); + new_expr.type() = bool_typet{}; + new_expr = simplify_node(new_expr); return changed(simplify_typecast(typecast_exprt(new_expr, expr.type()))); }