mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

Refactor theory_array_base to use structured bindings for enode pairs (#8405)

Browse source 
* Initial plan

* Refactor theory_array_base to use structured bindings for enode pairs

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 20:03:18 -08:00 • committed by GitHub
parent 21cdab0f20
commit 7747a17bb7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_array_base.cpp
View file

@ -428,13 +428,19 @@ namespace smt {
for (unsigned i = 0; i < m_axiom1_todo.size(); ++i) for (unsigned i = 0; i < m_axiom1_todo.size(); ++i)
assert_store_axiom1_core(m_axiom1_todo[i]); assert_store_axiom1_core(m_axiom1_todo[i]);
m_axiom1_todo.reset(); m_axiom1_todo.reset();
for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) {
assert_store_axiom2_core(m_axiom2_todo[i].first, m_axiom2_todo[i].second); auto [store, select] = m_axiom2_todo[i];
assert_store_axiom2_core(store, select);
}
m_axiom2_todo.reset(); m_axiom2_todo.reset();
for (unsigned i = 0; i < m_extensionality_todo.size(); ++i) for (unsigned i = 0; i < m_extensionality_todo.size(); ++i) {
assert_extensionality_core(m_extensionality_todo[i].first, m_extensionality_todo[i].second); auto [a1, a2] = m_extensionality_todo[i];
for (unsigned i = 0; i < m_congruent_todo.size(); ++i) assert_extensionality_core(a1, a2);
assert_congruent_core(m_congruent_todo[i].first, m_congruent_todo[i].second); }
for (unsigned i = 0; i < m_congruent_todo.size(); ++i) {
auto [a1, a2] = m_congruent_todo[i];
assert_congruent_core(a1, a2);
}
m_extensionality_todo.reset(); m_extensionality_todo.reset();
m_congruent_todo.reset(); m_congruent_todo.reset();
if (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()) { if (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()) {
@ -852,9 +858,7 @@ namespace smt {
propagate_selects_to_store_parents(r, todo); propagate_selects_to_store_parents(r, todo);
} }
for (unsigned qhead = 0; qhead < todo.size(); ++qhead) { for (unsigned qhead = 0; qhead < todo.size(); ++qhead) {
enode_pair & pair = todo[qhead]; auto [r, sel] = todo[qhead];
enode * r = pair.first;
enode * sel = pair.second;
propagate_select_to_store_parents(r, sel, todo); propagate_select_to_store_parents(r, sel, todo);
} }
} }