From 98fc8c99db60f5ec8a79a4dbeaf029fca05befc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Nov 2022 03:47:01 -0800 Subject: [PATCH] add shortcut to equality mk utility --- src/ast/rewriter/bool_rewriter.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 84552282b..ffceec277 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -690,8 +690,10 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) { - // degrades simplification - // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); + if (m().are_equal(lhs, rhs)) + return m().mk_true(); + if (m().are_distinct(lhs, rhs)) + return m().mk_false(); return m().mk_eq(lhs, rhs); }