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

fix #3950

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-15 15:07:53 -07:00
parent 357ec2fd01
commit 40b4ca7f86
2 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/opt/opt_solver.cpp
View file

@ -53,6 +53,7 @@ namespace opt {
m_params.m_relevancy_lvl = 0; m_params.m_relevancy_lvl = 0;
} }
m_params.m_arith_auto_config_simplex = false; m_params.m_arith_auto_config_simplex = false;
m_was_sat = false;
// m_params.m_auto_config = false; // m_params.m_auto_config = false;
} }
@ -87,6 +88,7 @@ namespace opt {
m_params.m_relevancy_lvl = 2; m_params.m_relevancy_lvl = 2;
} }
m_context.assert_expr(t); m_context.assert_expr(t);
m_was_sat = false;
} }
void opt_solver::push_core() { void opt_solver::push_core() {
@ -186,6 +188,7 @@ namespace opt {
r = m_context.check(num_assumptions, assumptions); r = m_context.check(num_assumptions, assumptions);
} }
r = adjust_result(r); r = adjust_result(r);
m_was_sat = r == l_true;
if (r == l_true) { if (r == l_true) {
m_context.get_model(m_model); m_context.get_model(m_model);
} }
@ -253,6 +256,7 @@ namespace opt {
decrement_value(i, val); decrement_value(i, val);
if (l_true != m_context.check(0, nullptr)) if (l_true != m_context.check(0, nullptr))
throw default_exception("maximization suspended"); throw default_exception("maximization suspended");
m_was_sat = true;
} }
else { else {
set_model(i); set_model(i);
@ -263,6 +267,7 @@ namespace opt {
decrement_value(i, val); decrement_value(i, val);
if (l_true != m_context.check(0, nullptr)) if (l_true != m_context.check(0, nullptr))
throw default_exception("maximization suspended"); throw default_exception("maximization suspended");
m_was_sat = true;
} }
m_objective_values[i] = val; m_objective_values[i] = val;
TRACE("opt", { TRACE("opt", {
@ -285,6 +290,7 @@ namespace opt {
assert_expr(ge); assert_expr(ge);
lbool is_sat = m_context.check(0, nullptr); lbool is_sat = m_context.check(0, nullptr);
is_sat = adjust_result(is_sat); is_sat = adjust_result(is_sat);
m_was_sat = is_sat == l_true;
if (is_sat == l_true) { if (is_sat == l_true) {
set_model(i); set_model(i);
} }
@ -321,8 +327,13 @@ namespace opt {
} }
void opt_solver::get_model_core(model_ref & m) { void opt_solver::get_model_core(model_ref & m) {
m_context.get_model(m); if (m_was_sat) {
if (!m) m = m_model; else m_model = m; m_context.get_model(m);
if (!m) m = m_model; else m_model = m;
}
else {
m = nullptr;
}
} }
proof * opt_solver::get_proof() { proof * opt_solver::get_proof() {

1
src/opt/opt_solver.h
View file

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