mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

seq_eq_solver: add pointer-equality fast path in has_len_offset and use all_of in find_branch_candidate

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/73262603-7733-4009-b5c7-17e55c79fb85

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-01 22:08:19 +00:00 • committed by GitHub
parent fd28976f4c
commit 008a101c08
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/seq_eq_solver.cpp
View file

@ -134,6 +134,11 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
if (!is_var(l_fst) || !is_var(r_fst))
return false;
if (l_fst == r_fst) {
offset = 0;
return true;
}
expr_ref len_l_fst = mk_len(l_fst);
if (!ctx.e_internalized(len_l_fst))
return false;
@ -875,10 +880,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
}
}
bool all_units = true;
for (expr* r : rs) {
all_units &= m_util.str.is_unit(r);
}
bool all_units = all_of(rs, [&](auto* r) { return m_util.str.is_unit(r); });
if (all_units) {
literal_vector lits;
lits.push_back(~mk_eq_empty(l));