mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-09 23:42:21 +00:00
Code Activity

[code-simplifier] seq_monadic_bench: replace comma-operator chains with explicit statements (#10408)

Browse source 
…ents

Replace confusing comma-operator idioms with clear, explicit
multi-statement code:

- parse_guard: replace comma-chained return with braced blocks
- lo/hi accumulation: replace comma one-liners with separate statements
- collect lambda: replace comma-combined complete/dropped updates

No functional change; behavior is identical.

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-05 09:00:28 -07:00 • committed by GitHub
parent 4af3410d10
commit 650e2a4e5a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/test/seq_monadic_bench.cpp
View file

@ -260,10 +260,12 @@ lbool run_file(
else if (a.is_gt(e, rhs, lhs)) strict = true;
else return false;
rational v;
if (is_int_var(lhs) && a.is_numeral(rhs, v))
return k = lhs, is_lower = false, bound = strict ? v - 1 : v, true;
if (a.is_numeral(lhs, v) && is_int_var(rhs))
return k = rhs, is_lower = true, bound = strict ? v + 1 : v, true;
if (is_int_var(lhs) && a.is_numeral(rhs, v)) {
k = lhs; is_lower = false; bound = strict ? v - 1 : v; return true;
}
if (a.is_numeral(lhs, v) && is_int_var(rhs)) {
k = rhs; is_lower = true; bound = strict ? v + 1 : v; return true;
}
return false;
};
@ -302,10 +304,13 @@ lbool run_file(
ok = false;
break;
}
if (is_lower)
lo = has_lo ? std::max(lo, bound) : bound, has_lo = true;
else
hi = has_hi ? std::min(hi, bound) : bound, has_hi = true;
if (is_lower) {
lo = has_lo ? std::max(lo, bound) : bound;
has_lo = true;
} else {
hi = has_hi ? std::min(hi, bound) : bound;
has_hi = true;
}
guards.push_back(other);
}
if (!ok)
@ -374,13 +379,16 @@ lbool run_file(
else if (m.is_not(e, arg) && u.str.is_in_re(arg, s, r))
negated = true;
else if (!u.str.is_in_re(e, s, r)) {
if (!collect_len(e, false))
complete = false, ++dropped;
if (!collect_len(e, false)) {
complete = false;
++dropped;
}
return;
}
bool is_var = is_seq_var(s);
if (!is_var && !u.str.is_concat(s)) {
complete = false, ++dropped;
complete = false;
++dropped;
return;
}
obj_map<expr, expr*>& map = is_var ? var_re : term_re;