mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

param order evaluation

Browse source
This commit is contained in:
Lev Nachmanson 2025-10-07 08:34:56 -07:00 • committed by Nikolaj Bjorner
parent 427c774961
commit 8feb8fa951
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2725,7 +2725,10 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
return BR_REWRITE2;
}
else if (re().is_union(r, r1, r2)) {
result = re().mk_union(re().mk_reverse(r1), re().mk_reverse(r2));
// ensure deterministic evaluation order of parameters
auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_union(a, b);
return BR_REWRITE2;
}
else if (re().is_intersection(r, r1, r2)) {
@ -4624,11 +4627,17 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
expr *e1 = nullptr, *e2 = nullptr;
if (re().is_intersection(a, e1, e2)) {
result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2));
// enforce deterministic evaluation order for nested complement arguments
auto a1 = re().mk_complement(e1);
auto b1 = re().mk_complement(e2);
result = re().mk_union(a1, b1);
return BR_REWRITE2;
}
if (re().is_union(a, e1, e2)) {
result = re().mk_inter(re().mk_complement(e1), re().mk_complement(e2));
// enforce deterministic evaluation order for nested complement arguments
auto a1 = re().mk_complement(e1);
auto b1 = re().mk_complement(e2);
result = re().mk_inter(a1, b1);
return BR_REWRITE2;
}
if (re().is_empty(a)) {