mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #1655

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-25 21:21:27 -07:00
parent 727ba13566
commit da0239d200
2 changed files with 5 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/opt/opt_context.cpp
View file

@ -128,7 +128,7 @@ namespace opt {
m_optsmt(m), m_optsmt(m),
m_scoped_state(m), m_scoped_state(m),
m_fm(alloc(generic_model_converter, m, "opt")), m_fm(alloc(generic_model_converter, m, "opt")),
m_model_fixed(false), m_model_fixed(),
m_objective_refs(m), m_objective_refs(m),
m_enable_sat(false), m_enable_sat(false),
m_is_clausal(false), m_is_clausal(false),
@ -340,10 +340,10 @@ namespace opt {
} }
void context::fix_model(model_ref& mdl) { void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed) { if (mdl && !m_model_fixed.contains(mdl.get())) {
(*m_fm)(mdl); (*m_fm)(mdl);
apply(m_model_converter, mdl); apply(m_model_converter, mdl);
m_model_fixed = true; m_model_fixed.push_back(mdl.get());
} }
} }
@ -444,13 +444,11 @@ 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];
m_model_fixed = false;
++m_box_index; ++m_box_index;
return l_true; return l_true;
} }
if (m_box_index < m_objectives.size()) { if (m_box_index < m_objectives.size()) {
m_model = nullptr; m_model = nullptr;
m_model_fixed = false;
++m_box_index; ++m_box_index;
return l_undef; return l_undef;
} }
@ -475,7 +473,6 @@ namespace opt {
} }
if (r == l_true && m_box_models.size() > 0) { if (r == l_true && m_box_models.size() > 0) {
m_model = m_box_models[0]; m_model = m_box_models[0];
m_model_fixed = false;
} }
return r; return r;
} }
@ -563,7 +560,6 @@ namespace opt {
void context::yield() { void context::yield() {
SASSERT (m_pareto); SASSERT (m_pareto);
m_pareto->get_model(m_model, m_labels); m_pareto->get_model(m_model, m_labels);
m_model_fixed = false;
update_bound(true); update_bound(true);
update_bound(false); update_bound(false);
TRACE("opt", model_smt2_pp(tout, m, *m_model.get(), 0);); TRACE("opt", model_smt2_pp(tout, m, *m_model.get(), 0););
@ -1410,7 +1406,7 @@ namespace opt {
m_pareto = nullptr; m_pareto = nullptr;
m_box_index = UINT_MAX; m_box_index = UINT_MAX;
m_model.reset(); m_model.reset();
m_model_fixed = false; m_model_fixed.reset();
} }
void context::set_pareto(pareto_base* p) { void context::set_pareto(pareto_base* p) {

2
src/opt/opt_context.h
View file

@ -159,7 +159,7 @@ namespace opt {
model_ref m_model; model_ref m_model;
model_converter_ref m_model_converter; model_converter_ref m_model_converter;
generic_model_converter_ref m_fm; generic_model_converter_ref m_fm;
bool m_model_fixed; sref_vector<model> m_model_fixed;
unsigned m_model_counter; unsigned m_model_counter;
obj_map<func_decl, unsigned> m_objective_fns; obj_map<func_decl, unsigned> m_objective_fns;
obj_map<func_decl, expr*> m_objective_orig; obj_map<func_decl, expr*> m_objective_orig;