mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

add shortcut to equality mk utility

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-16 03:47:01 -08:00
parent 55ab7778f4
commit 98fc8c99db
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/bool_rewriter.cpp
View file

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