mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 22:33:35 +00:00
Code Activity

Refactor dyn_ack.cpp to use structured bindings for app_pair/app_triple (#8359)

Browse source 
* Initial plan

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

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

* Rename structured binding variables from app1/app2/app3 to a1/a2/a3

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-28 19:39:25 -08:00 • committed by Nikolaj Bjorner
parent 1853cdeb3d
commit abd488f173
1 changed files with 51 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

91
src/smt/dyn_ack.cpp
View file

@ -175,8 +175,9 @@ namespace smt {
void dyn_ack_manager::reset_app_pairs() { void dyn_ack_manager::reset_app_pairs() {
for (app_pair& p : m_app_pairs) { for (app_pair& p : m_app_pairs) {
m.dec_ref(p.first); auto [a1, a2] = p;
m.dec_ref(p.second); m.dec_ref(a1);
m.dec_ref(a2);
} }
m_app_pairs.reset(); m_app_pairs.reset();
} }
@ -282,10 +283,12 @@ namespace smt {
} }
bool operator()(app_pair const & p1, app_pair const & p2) const { bool operator()(app_pair const & p1, app_pair const & p2) const {
auto [a1_1, a1_2] = p1;
auto [a2_1, a2_2] = p2;
unsigned n1 = 0; unsigned n1 = 0;
unsigned n2 = 0; unsigned n2 = 0;
m_app_pair2num_occs.find(p1.first, p1.second, n1); m_app_pair2num_occs.find(a1_1, a1_2, n1);
m_app_pair2num_occs.find(p2.first, p2.second, n2); m_app_pair2num_occs.find(a2_1, a2_2, n2);
SASSERT(n1 > 0); SASSERT(n1 > 0);
SASSERT(n2 > 0); SASSERT(n2 > 0);
return n1 > n2; return n1 > n2;
@ -301,32 +304,33 @@ namespace smt {
svector<app_pair>::iterator it2 = it; svector<app_pair>::iterator it2 = it;
for (; it != end; ++it) { for (; it != end; ++it) {
app_pair & p = *it; app_pair & p = *it;
auto [a1, a2] = p;
if (m_instantiated.contains(p)) { if (m_instantiated.contains(p)) {
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
m.dec_ref(p.first); m.dec_ref(a1);
m.dec_ref(p.second); m.dec_ref(a2);
SASSERT(!m_app_pair2num_occs.contains(p.first, p.second)); SASSERT(!m_app_pair2num_occs.contains(a1, a2));
continue; continue;
} }
unsigned num_occs = 0; unsigned num_occs = 0;
m_app_pair2num_occs.find(p.first, p.second, num_occs); m_app_pair2num_occs.find(a1, a2, num_occs);
// The following invariant is not true. p.first and // The following invariant is not true. a1 and
// p.second may have been instantiated, and removed from // a2 may have been instantiated, and removed from
// m_app_pair2num_occs, but not from m_app_pairs. // m_app_pair2num_occs, but not from m_app_pairs.
// //
// SASSERT(num_occs > 0); // SASSERT(num_occs > 0);
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay); num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
if (num_occs <= 1) { if (num_occs <= 1) {
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
m_app_pair2num_occs.erase(p.first, p.second); m_app_pair2num_occs.erase(a1, a2);
m.dec_ref(p.first); m.dec_ref(a1);
m.dec_ref(p.second); m.dec_ref(a2);
continue; continue;
} }
*it2 = p; *it2 = p;
++it2; ++it2;
SASSERT(num_occs > 0); SASSERT(num_occs > 0);
m_app_pair2num_occs.insert(p.first, p.second, num_occs); m_app_pair2num_occs.insert(a1, a2, num_occs);
if (num_occs >= m_params.m_dack_threshold) if (num_occs >= m_params.m_dack_threshold)
m_to_instantiate.push_back(p); m_to_instantiate.push_back(p);
} }
@ -353,18 +357,20 @@ namespace smt {
m_context.m_stats.m_num_del_dyn_ack++; m_context.m_stats.m_num_del_dyn_ack++;
app_pair p((app*)nullptr,(app*)nullptr); app_pair p((app*)nullptr,(app*)nullptr);
if (m_clause2app_pair.find(cls, p)) { if (m_clause2app_pair.find(cls, p)) {
SASSERT(p.first && p.second); auto [a1, a2] = p;
SASSERT(a1 && a2);
m_instantiated.erase(p); m_instantiated.erase(p);
m_clause2app_pair.erase(cls); m_clause2app_pair.erase(cls);
SASSERT(!m_app_pair2num_occs.contains(p.first, p.second)); SASSERT(!m_app_pair2num_occs.contains(a1, a2));
return; return;
} }
app_triple tr(0,0,0); app_triple tr(0,0,0);
if (m_triple.m_clause2apps.find(cls, tr)) { if (m_triple.m_clause2apps.find(cls, tr)) {
SASSERT(tr.first && tr.second && tr.third); auto [a1, a2, a3] = tr;
SASSERT(a1 && a2 && a3);
m_triple.m_instantiated.erase(tr); m_triple.m_instantiated.erase(tr);
m_triple.m_clause2apps.erase(cls); m_triple.m_clause2apps.erase(cls);
SASSERT(!m_triple.m_app2num_occs.contains(tr.first, tr.second, tr.third)); SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
return; return;
} }
} }
@ -450,9 +456,10 @@ namespace smt {
void dyn_ack_manager::reset_app_triples() { void dyn_ack_manager::reset_app_triples() {
for (app_triple& p : m_triple.m_apps) { for (app_triple& p : m_triple.m_apps) {
m.dec_ref(p.first); auto [a1, a2, a3] = p;
m.dec_ref(p.second); m.dec_ref(a1);
m.dec_ref(p.third); m.dec_ref(a2);
m.dec_ref(a3);
} }
m_triple.m_apps.reset(); m_triple.m_apps.reset();
} }
@ -510,10 +517,12 @@ namespace smt {
} }
bool operator()(app_triple const & p1, app_triple const & p2) const { bool operator()(app_triple const & p1, app_triple const & p2) const {
auto [a1_1, a1_2, a1_3] = p1;
auto [a2_1, a2_2, a2_3] = p2;
unsigned n1 = 0; unsigned n1 = 0;
unsigned n2 = 0; unsigned n2 = 0;
m_app_triple2num_occs.find(p1.first, p1.second, p1.third, n1); m_app_triple2num_occs.find(a1_1, a1_2, a1_3, n1);
m_app_triple2num_occs.find(p2.first, p2.second, p2.third, n2); m_app_triple2num_occs.find(a2_1, a2_2, a2_3, n2);
SASSERT(n1 > 0); SASSERT(n1 > 0);
SASSERT(n2 > 0); SASSERT(n2 > 0);
return n1 > n2; return n1 > n2;
@ -529,34 +538,35 @@ namespace smt {
svector<app_triple>::iterator it2 = it; svector<app_triple>::iterator it2 = it;
for (; it != end; ++it) { for (; it != end; ++it) {
app_triple & p = *it; app_triple & p = *it;
auto [a1, a2, a3] = p;
if (m_triple.m_instantiated.contains(p)) { if (m_triple.m_instantiated.contains(p)) {
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
m.dec_ref(p.first); m.dec_ref(a1);
m.dec_ref(p.second); m.dec_ref(a2);
m.dec_ref(p.third); m.dec_ref(a3);
SASSERT(!m_triple.m_app2num_occs.contains(p.first, p.second, p.third)); SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
continue; continue;
} }
unsigned num_occs = 0; unsigned num_occs = 0;
m_triple.m_app2num_occs.find(p.first, p.second, p.third, num_occs); m_triple.m_app2num_occs.find(a1, a2, a3, num_occs);
// The following invariant is not true. p.first and // The following invariant is not true. a1 and
// p.second may have been instantiated, and removed from // a2 may have been instantiated, and removed from
// m_app_triple2num_occs, but not from m_app_triples. // m_app_triple2num_occs, but not from m_app_triples.
// //
// SASSERT(num_occs > 0); // SASSERT(num_occs > 0);
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay); num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
if (num_occs <= 1) { if (num_occs <= 1) {
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
m_triple.m_app2num_occs.erase(p.first, p.second, p.third); m_triple.m_app2num_occs.erase(a1, a2, a3);
m.dec_ref(p.first); m.dec_ref(a1);
m.dec_ref(p.second); m.dec_ref(a2);
m.dec_ref(p.third); m.dec_ref(a3);
continue; continue;
} }
*it2 = p; *it2 = p;
++it2; ++it2;
SASSERT(num_occs > 0); SASSERT(num_occs > 0);
m_triple.m_app2num_occs.insert(p.first, p.second, p.third, num_occs); m_triple.m_app2num_occs.insert(a1, a2, a3, num_occs);
if (num_occs >= m_params.m_dack_threshold) if (num_occs >= m_params.m_dack_threshold)
m_triple.m_to_instantiate.push_back(p); m_triple.m_to_instantiate.push_back(p);
} }
@ -572,8 +582,9 @@ namespace smt {
bool dyn_ack_manager::check_invariant() const { bool dyn_ack_manager::check_invariant() const {
for (auto const& kv : m_clause2app_pair) { for (auto const& kv : m_clause2app_pair) {
app_pair const & p = kv.get_value(); app_pair const & p = kv.get_value();
auto [a1, a2] = p;
SASSERT(m_instantiated.contains(p)); SASSERT(m_instantiated.contains(p));
SASSERT(!m_app_pair2num_occs.contains(p.first, p.second)); SASSERT(!m_app_pair2num_occs.contains(a1, a2));
} }
return true; return true;