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

Fix order of checks in mk_in to handle singleton same element case first

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-14 17:10:38 +00:00
parent deca1aede8
commit 49779a2492
1 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/ast/rewriter/finite_set_rewriter.cpp
View file

@ -176,23 +176,23 @@ br_status finite_set_rewriter::mk_singleton(expr * arg, expr_ref & result) {
}
br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) {
// set.in(x, singleton(y)) -> x = y
expr* singleton_elem;
if (m_util.is_singleton(set, singleton_elem)) {
result = m().mk_eq(elem, singleton_elem);
return BR_REWRITE1;
}
// set.in(x, empty) -> false
if (m_util.is_empty(set)) {
result = m().mk_false();
return BR_DONE;
}
// set.in(x, singleton(x)) -> true (when x is the same)
if (m_util.is_singleton(set, singleton_elem) && elem == singleton_elem) {
result = m().mk_true();
return BR_DONE;
// set.in(x, singleton(y)) checks
expr* singleton_elem;
if (m_util.is_singleton(set, singleton_elem)) {
// set.in(x, singleton(x)) -> true (when x is the same)
if (elem == singleton_elem) {
result = m().mk_true();
return BR_DONE;
}
// set.in(x, singleton(y)) -> x = y (when x != y)
result = m().mk_eq(elem, singleton_elem);
return BR_REWRITE1;
}
return BR_FAILED;