mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

Refactor: extract saturating_add helper, simplify hash-check condition

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/da8647c4-ddff-47ce-9364-2eee3810c38d

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-28 16:12:33 +00:00 • committed by GitHub
parent 581ad12efa
commit 8bbac04a26
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/euf/euf_seq_plugin.cpp
View file

@ -46,6 +46,11 @@ namespace euf {
}
}
// Saturating unsigned addition: returns UINT_MAX instead of wrapping.
static unsigned saturating_add(unsigned a, unsigned b) {
return (b > UINT_MAX - a) ? UINT_MAX : a + b;
}
unsigned enode_concat_hash::operator()(enode* n) const {
snode* sn = sg.find(n->get_expr());
if (sn && sn->has_cached_hash())
@ -70,8 +75,8 @@ namespace euf {
if (sa && sb && sa->length() != sb->length())
return false;
// fast-path: cached associativity hash (O(1))
if (sa && sa->has_cached_hash() && sb && sb->has_cached_hash() &&
sa->assoc_hash() != sb->assoc_hash())
bool both_have_hash = sa && sa->has_cached_hash() && sb && sb->has_cached_hash();
if (both_have_hash && sa->assoc_hash() != sb->assoc_hash())
return false;
enode_vector la, lb;
collect_enode_leaves(a, seq, la);
@ -264,8 +269,8 @@ namespace euf {
ast_manager& m = g.get_manager();
enode* body_n = a->get_arg(0);
// saturating add: prevent silent unsigned wrap-around on large bounds
unsigned lo_merged = (lo2 > UINT_MAX - lo1) ? UINT_MAX : lo1 + lo2;
unsigned hi_merged = (hi2 > UINT_MAX - hi1) ? UINT_MAX : hi1 + hi2;
unsigned lo_merged = saturating_add(lo1, lo2);
unsigned hi_merged = saturating_add(hi1, hi2);
expr_ref merged(m_seq.re.mk_loop(body_n->get_expr(), lo_merged, hi_merged), m);
enode* merged_n = mk(merged, 1, &body_n);
push_merge(n, merged_n);