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

fix #4403

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-05 12:13:39 -07:00
parent bb9cd5dd49
commit a32fabf5ee
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/opt/opt_context.cpp
View file

@ -367,6 +367,7 @@ namespace opt {
void context::fix_model(model_ref& mdl) { void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed.contains(mdl.get())) { if (mdl && !m_model_fixed.contains(mdl.get())) {
TRACE("opt", m_fm->display(tout << "fix-model\n"); TRACE("opt", m_fm->display(tout << "fix-model\n");
tout << *mdl << "\n";
if (m_model_converter) m_model_converter->display(tout);); if (m_model_converter) m_model_converter->display(tout););
(*m_fm)(mdl); (*m_fm)(mdl);
apply(m_model_converter, mdl); apply(m_model_converter, mdl);
@ -482,6 +483,7 @@ namespace opt {
lbool context::execute_box() { lbool context::execute_box() {
if (m_box_index < m_box_models.size()) { if (m_box_index < m_box_models.size()) {
m_model = m_box_models[m_box_index]; m_model = m_box_models[m_box_index];
CTRACE("opt", m_model, tout << *m_model << "\n";);
++m_box_index; ++m_box_index;
return l_true; return l_true;
} }
@ -505,12 +507,15 @@ namespace opt {
m_box_models.push_back(m_model.get()); m_box_models.push_back(m_model.get());
} }
else { else {
m_box_models.push_back(m_optsmt.get_model(j)); model* mdl = m_optsmt.get_model(j);
if (!mdl) mdl = m_model.get();
m_box_models.push_back(mdl);
++j; ++j;
} }
} }
if (r == l_true && !m_box_models.empty()) { if (r == l_true && !m_box_models.empty()) {
m_model = m_box_models[0]; m_model = m_box_models[0];
CTRACE("opt", m_model, tout << *m_model << "\n";);
} }
return r; return r;
} }
@ -787,6 +792,7 @@ namespace opt {
void context::normalize(expr_ref_vector const& asms) { void context::normalize(expr_ref_vector const& asms) {
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
m_model_converter = nullptr;
to_fmls(fmls); to_fmls(fmls);
simplify_fmls(fmls, asms); simplify_fmls(fmls, asms);
from_fmls(fmls); from_fmls(fmls);
@ -1248,7 +1254,7 @@ namespace opt {
case O_MAXSMT: { case O_MAXSMT: {
maxsmt& ms = *m_maxsmts.find(obj.m_id); maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < obj.m_terms.size(); ++j) { for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
ms.add(obj.m_terms[j].get(), obj.m_weights[j]); ms.add(obj.m_terms.get(j), obj.m_weights[j]);
} }
break; break;
} }
@ -1468,6 +1474,7 @@ namespace opt {
void context::clear_state() { void context::clear_state() {
m_pareto = nullptr; m_pareto = nullptr;
m_box_index = UINT_MAX; m_box_index = UINT_MAX;
m_box_models.reset();
m_model.reset(); m_model.reset();
m_model_fixed.reset(); m_model_fixed.reset();
m_core.reset(); m_core.reset();

3
src/opt/optsmt.cpp
View file

@ -469,6 +469,7 @@ namespace opt {
return l_true; return l_true;
} }
void optsmt::setup(opt_solver& solver) { void optsmt::setup(opt_solver& solver) {
m_s = &solver; m_s = &solver;
solver.reset_objectives(); solver.reset_objectives();
@ -578,6 +579,8 @@ namespace opt {
m_objs.reset(); m_objs.reset();
m_vars.reset(); m_vars.reset();
m_model.reset(); m_model.reset();
m_best_model = nullptr;
m_models.reset();
m_lower_fmls.reset(); m_lower_fmls.reset();
m_s = nullptr; m_s = nullptr;
} }