mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-16 18:30:35 +02:00
parent b5309d5fd0
commit 7496f11542
1 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/opt/maxres.cpp
View file

@ -763,19 +763,16 @@ public:
unfold_record r;
if (!m_unfold.find(c, r))
continue;
IF_VERBOSE(2, verbose_stream() << "to unfold " << mk_pp(c, m) << "\n");
IF_VERBOSE(1, verbose_stream() << "to unfold " << mk_pp(c, m) << " unfold size " << m_unfold.size() << " core " << core.size() << "\n");
for (expr* f : r.ws) {
IF_VERBOSE(2, verbose_stream() << "unfold " << mk_pp(f, m) << "\n");
IF_VERBOSE(1, verbose_stream() << "unfold " << mk_pp(f, m) << "\n");
new_assumption(f, r.weight);
}
m_unfold_upper -= r.weight * rational(r.ws.size() - 1);
m_unfold.remove(c);
}
for (expr* _ : core)
partial.push_back(nullptr);
std::cout << "Core size " << core.size() << "\n";
partial.resize(core.size(), nullptr);
if (core.size() > 2)
m_unfold_upper += rational(core.size()-2)*weight;
@ -808,16 +805,21 @@ public:
if (partial.get(i + 1))
r.ws.push_back(partial.get(i + 1));
m_trail.append(r.ws.size(), r.ws.data());
w = mk_fresh_bool("w");
cls = m.mk_and(r.ws);
fml = m.mk_implies(w, cls);
partial.push_back(w);
add(fml);
update_model(w, cls);
m_defs.push_back(fml);
m_unfold.insert(w, r);
if (r.ws.size() == 1)
w = u;
else {
w = mk_fresh_bool("w");
cls = m.mk_and(r.ws);
fml = m.mk_implies(w, cls);
add(fml);
update_model(w, cls);
m_defs.push_back(fml);
m_unfold.insert(w, r);
}
partial.push_back(w);
}
new_assumption(w, weight);
if (w)
new_assumption(w, weight);
s().assert_expr(m.mk_not(core.back()));
}