mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

save last model to ensure it is available fixes #1514

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-03 19:26:31 -08:00
parent 8e09a78c26
commit 205d77d591
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/opt/opt_solver.cpp
View file

@ -227,9 +227,13 @@ namespace opt {
smt::theory_var v = m_objective_vars[i];
bool has_shared = false;
inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
get_model(m_model);
inf_eps val2;
m_valid_objectives[i] = true;
TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
if (!m_models[i]) {
set_model(i);
}
if (m_context.get_context().update_model(has_shared)) {
if (has_shared && val != current_objective_value(i)) {
decrement_value(i, val);
@ -247,7 +251,7 @@ namespace opt {
tout << "objective: " << mk_pp(m_objective_terms[i].get(), m) << "\n";
tout << "maximal value: " << val << "\n";
tout << "new condition: " << blocker << "\n";
model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
}
void opt_solver::set_model(unsigned i) {
@ -299,6 +303,7 @@ namespace opt {
void opt_solver::get_model(model_ref & m) {
m_context.get_model(m);
if (!m) m = m_model; else m_model = m;
}
proof * opt_solver::get_proof() {

1
src/opt/opt_solver.h
View file

@ -73,6 +73,7 @@ namespace opt {
filter_model_converter& m_fm;
progress_callback * m_callback;
symbol m_logic;
model_ref m_model;
svector<smt::theory_var> m_objective_vars;
vector<inf_eps> m_objective_values;
sref_vector<model> m_models;