mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-23 00:50:29 +00:00
Code Activity

cosmetics

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-19 10:05:36 -07:00
parent 4bdfb598ea
commit f885fe953f
4 changed files with 354 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ackermannization/ackr_helper.cpp
View file

@ -18,13 +18,13 @@
double ackr_helper::calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2) {
double total = 0;
for (auto const& kv : occs1) {
total += n_choose_2_chk(kv.m_value->var_args.size());
total += kv.m_value->const_args.size() * kv.m_value->var_args.size();
for (auto const &[k, v] : occs1) {
total += n_choose_2_chk(v->var_args.size());
total += v->const_args.size() * v->var_args.size();
}
for (auto const& kv : occs2) {
total += n_choose_2_chk(kv.m_value->var_args.size());
total += kv.m_value->const_args.size() * kv.m_value->var_args.size();
for (auto const &[k, v] : occs2) {
total += n_choose_2_chk(v->var_args.size());
total += v->const_args.size() * v->var_args.size();
}
return total;
}

8
src/ackermannization/ackr_helper.h
View file

@ -70,10 +70,10 @@ public:
void prune_non_select(obj_map<app, app_set*> & sels, expr_mark& non_select) {
ptr_vector<app> nons;
for (auto& kv : sels) {
if (non_select.is_marked(kv.m_key)) {
nons.push_back(kv.m_key);
dealloc(kv.m_value);
for (auto &[k, v] : sels) {
if (non_select.is_marked(k)) {
nons.push_back(k);
dealloc(v);
}
}
for (app* s : nons) {

12
src/ackermannization/lackr.cpp
View file

@ -149,9 +149,9 @@ void lackr::eager_enc() {
checkpoint();
ackr(v);
}
for (auto const& kv : m_sel2terms) {
for (auto const &[k, v] : m_sel2terms) {
checkpoint();
ackr(kv.get_value());
ackr(v);
}
}
@ -190,13 +190,13 @@ void lackr::abstract_fun(fun2terms_map const& apps) {
}
void lackr::abstract_sel(sel2terms_map const& apps) {
for (auto const& kv : apps) {
func_decl * fd = kv.m_key->get_decl();
for (app * t : kv.m_value->const_args) {
for (auto const &[k, v] : apps) {
func_decl * fd = k->get_decl();
for (app * t : v->const_args) {
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
m_info->set_abstr(t, fc);
}
for (app * t : kv.m_value->var_args) {
for (app * t : v->var_args) {
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
m_info->set_abstr(t, fc);
}