mirror of
https://github.com/Z3Prover/z3
synced 2026-02-02 07:16:17 +00:00
Refactor dyn_ack.cpp to use structured bindings for app_pair/app_triple (#8359)
* 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
GitHub
parent
3f9fa59811
commit
ebed679287
1 changed files with 51 additions and 40 deletions
|
|
@ -175,8 +175,9 @@ namespace smt {
|
|||
|
||||
void dyn_ack_manager::reset_app_pairs() {
|
||||
for (app_pair& p : m_app_pairs) {
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
auto [a1, a2] = p;
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
}
|
||||
m_app_pairs.reset();
|
||||
}
|
||||
|
|
@ -282,10 +283,12 @@ namespace smt {
|
|||
}
|
||||
|
||||
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 n2 = 0;
|
||||
m_app_pair2num_occs.find(p1.first, p1.second, n1);
|
||||
m_app_pair2num_occs.find(p2.first, p2.second, n2);
|
||||
m_app_pair2num_occs.find(a1_1, a1_2, n1);
|
||||
m_app_pair2num_occs.find(a2_1, a2_2, n2);
|
||||
SASSERT(n1 > 0);
|
||||
SASSERT(n2 > 0);
|
||||
return n1 > n2;
|
||||
|
|
@ -301,32 +304,33 @@ namespace smt {
|
|||
svector<app_pair>::iterator it2 = it;
|
||||
for (; it != end; ++it) {
|
||||
app_pair & p = *it;
|
||||
auto [a1, a2] = 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";);
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
SASSERT(!m_app_pair2num_occs.contains(p.first, p.second));
|
||||
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
|
||||
continue;
|
||||
}
|
||||
unsigned num_occs = 0;
|
||||
m_app_pair2num_occs.find(p.first, p.second, num_occs);
|
||||
// The following invariant is not true. p.first and
|
||||
// p.second may have been instantiated, and removed from
|
||||
m_app_pair2num_occs.find(a1, a2, num_occs);
|
||||
// The following invariant is not true. a1 and
|
||||
// a2 may have been instantiated, and removed from
|
||||
// m_app_pair2num_occs, but not from m_app_pairs.
|
||||
//
|
||||
// SASSERT(num_occs > 0);
|
||||
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
|
||||
if (num_occs <= 1) {
|
||||
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
|
||||
m_app_pair2num_occs.erase(p.first, p.second);
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
|
||||
m_app_pair2num_occs.erase(a1, a2);
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
continue;
|
||||
}
|
||||
*it2 = p;
|
||||
++it2;
|
||||
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)
|
||||
m_to_instantiate.push_back(p);
|
||||
}
|
||||
|
|
@ -353,18 +357,20 @@ namespace smt {
|
|||
m_context.m_stats.m_num_del_dyn_ack++;
|
||||
app_pair p((app*)nullptr,(app*)nullptr);
|
||||
if (m_clause2app_pair.find(cls, p)) {
|
||||
SASSERT(p.first && p.second);
|
||||
auto [a1, a2] = p;
|
||||
SASSERT(a1 && a2);
|
||||
m_instantiated.erase(p);
|
||||
m_clause2app_pair.erase(cls);
|
||||
SASSERT(!m_app_pair2num_occs.contains(p.first, p.second));
|
||||
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
|
||||
return;
|
||||
}
|
||||
app_triple tr(0,0,0);
|
||||
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_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;
|
||||
}
|
||||
}
|
||||
|
|
@ -450,9 +456,10 @@ namespace smt {
|
|||
|
||||
void dyn_ack_manager::reset_app_triples() {
|
||||
for (app_triple& p : m_triple.m_apps) {
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
m.dec_ref(p.third);
|
||||
auto [a1, a2, a3] = p;
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
m.dec_ref(a3);
|
||||
}
|
||||
m_triple.m_apps.reset();
|
||||
}
|
||||
|
|
@ -510,10 +517,12 @@ namespace smt {
|
|||
}
|
||||
|
||||
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 n2 = 0;
|
||||
m_app_triple2num_occs.find(p1.first, p1.second, p1.third, n1);
|
||||
m_app_triple2num_occs.find(p2.first, p2.second, p2.third, n2);
|
||||
m_app_triple2num_occs.find(a1_1, a1_2, a1_3, n1);
|
||||
m_app_triple2num_occs.find(a2_1, a2_2, a2_3, n2);
|
||||
SASSERT(n1 > 0);
|
||||
SASSERT(n2 > 0);
|
||||
return n1 > n2;
|
||||
|
|
@ -529,34 +538,35 @@ namespace smt {
|
|||
svector<app_triple>::iterator it2 = it;
|
||||
for (; it != end; ++it) {
|
||||
app_triple & p = *it;
|
||||
auto [a1, a2, a3] = 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";);
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
m.dec_ref(p.third);
|
||||
SASSERT(!m_triple.m_app2num_occs.contains(p.first, p.second, p.third));
|
||||
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
m.dec_ref(a3);
|
||||
SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
|
||||
continue;
|
||||
}
|
||||
unsigned num_occs = 0;
|
||||
m_triple.m_app2num_occs.find(p.first, p.second, p.third, num_occs);
|
||||
// The following invariant is not true. p.first and
|
||||
// p.second may have been instantiated, and removed from
|
||||
m_triple.m_app2num_occs.find(a1, a2, a3, num_occs);
|
||||
// The following invariant is not true. a1 and
|
||||
// a2 may have been instantiated, and removed from
|
||||
// m_app_triple2num_occs, but not from m_app_triples.
|
||||
//
|
||||
// SASSERT(num_occs > 0);
|
||||
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
|
||||
if (num_occs <= 1) {
|
||||
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
|
||||
m_triple.m_app2num_occs.erase(p.first, p.second, p.third);
|
||||
m.dec_ref(p.first);
|
||||
m.dec_ref(p.second);
|
||||
m.dec_ref(p.third);
|
||||
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
|
||||
m_triple.m_app2num_occs.erase(a1, a2, a3);
|
||||
m.dec_ref(a1);
|
||||
m.dec_ref(a2);
|
||||
m.dec_ref(a3);
|
||||
continue;
|
||||
}
|
||||
*it2 = p;
|
||||
++it2;
|
||||
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)
|
||||
m_triple.m_to_instantiate.push_back(p);
|
||||
}
|
||||
|
|
@ -572,8 +582,9 @@ namespace smt {
|
|||
bool dyn_ack_manager::check_invariant() const {
|
||||
for (auto const& kv : m_clause2app_pair) {
|
||||
app_pair const & p = kv.get_value();
|
||||
auto [a1, a2] = 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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue