From 2a1f8ac2d89a13d52275e952b2f1e3c2d07be5c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jun 2019 23:48:00 +0200 Subject: [PATCH] revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 5 +++++ src/ast/rewriter/bool_rewriter.h | 5 +---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index a9861093a..90e6c37d7 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -645,6 +645,11 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } +app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) { + // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); + return m().mk_eq(lhs, rhs); +} + br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (m().are_equal(lhs, rhs)) { result = m().mk_true(); diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 987c0a0eb..87f9d370d 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -127,10 +127,7 @@ public: br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result); br_status mk_not_core(expr * t, expr_ref & result); - app* mk_eq(expr* lhs, expr* rhs) { - if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); - return m().mk_eq(lhs, rhs); - } + app* mk_eq(expr* lhs, expr* rhs); void mk_eq(expr * lhs, expr * rhs, expr_ref & result) { if (mk_eq_core(lhs, rhs, result) == BR_FAILED)