mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

Refactor seq_rewriter to use C++17 structured bindings (#8381)

Browse source 
* Initial plan

* Refactor seq_rewriter.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback - move pair declaration inside loop

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-27 12:06:11 -08:00 • committed by Nikolaj Bjorner
parent 49cb81d538
commit 307982b67e
1 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4981,8 +4981,7 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
void seq_rewriter::intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges) { void seq_rewriter::intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges) {
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < ranges.size(); ++i) { for (unsigned i = 0; i < ranges.size(); ++i) {
unsigned lo1 = ranges[i].first; auto [lo1, hi1] = ranges[i];
unsigned hi1 = ranges[i].second;
if (hi < lo1) if (hi < lo1)
break; break;
if (hi1 >= lo) if (hi1 >= lo)
@ -5244,8 +5243,8 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
if (!changed) { if (!changed) {
return BR_FAILED; return BR_FAILED;
} }
for (auto const& p : new_eqs) { for (auto const& [lhs, rhs] : new_eqs) {
res.push_back(m().mk_eq(p.first, p.second)); res.push_back(m().mk_eq(lhs, rhs));
} }
result = mk_and(res); result = mk_and(res);
TRACE(seq_verbose, tout << result << "\n";); TRACE(seq_verbose, tout << result << "\n";);
@ -5616,11 +5615,14 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
} }
else if (str().is_concat(e)) { else if (str().is_concat(e)) {
bool visited = true; bool visited = true;
std::pair<bool, unsigned> result(true, 0u), r; bool is_valid = true;
unsigned count = 0u;
for (expr* arg : *to_app(e)) { for (expr* arg : *to_app(e)) {
std::pair<bool, unsigned> r;
if (cache.find(arg, r)) { if (cache.find(arg, r)) {
result.first &= r.first; auto [r_valid, r_count] = r;
result.second += r.second; is_valid &= r_valid;
count += r_count;
} }
else { else {
sub.push_back(arg); sub.push_back(arg);
@ -5628,7 +5630,7 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
} }
} }
if (visited) if (visited)
cache.insert(e, result); cache.insert(e, { is_valid, count });
return visited; return visited;
} }
else if (m().is_ite(e, c, th, el)) { else if (m().is_ite(e, c, th, el)) {
@ -5640,7 +5642,9 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
sub.push_back(el); sub.push_back(el);
if (subsz != sub.size()) if (subsz != sub.size())
return false; return false;
cache.insert(e, { r1.first && r2.first && r1.second == r2.second, std::min(r1.second, r2.second)}); auto [r1_valid, r1_count] = r1;
auto [r2_valid, r2_count] = r2;
cache.insert(e, { r1_valid && r2_valid && r1_count == r2_count, std::min(r1_count, r2_count)});
return true; return true;
} }
else { else {