mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix objective value regression in simplex maximation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-01 12:45:26 -07:00
parent 736d43c084
commit 2a907ea52a
3 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/opt/opt_solver.cpp
View file

@ -98,13 +98,14 @@ namespace opt {
lbool r = m_context.check(num_assumptions, assumptions);
if (r == l_true && m_objective_enabled) {
m_objective_values.reset();
smt::theory_opt& opt = get_optimizer();
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
smt::theory_var v = m_objective_vars[i];
bool is_bounded = get_optimizer().maximize(v);
bool is_bounded = opt.maximize(v);
if (is_bounded) {
m_objective_values.push_back(get_optimizer().get_objective_value(v));
m_objective_values.push_back(opt.get_objective_value(v));
} else {
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
inf_eps r(rational(1), inf_rational(0));
m_objective_values.push_back(r);
}
}

9
src/opt/optimize_objectives.cpp
View file

@ -44,6 +44,8 @@ Notes:
#include "opt_solver.h"
#include "arith_decl_plugin.h"
#include "theory_arith.h"
#include "ast_pp.h"
#include "model_pp.h"
namespace opt {
@ -68,6 +70,7 @@ namespace opt {
arith_util autil(m);
opt_solver::scoped_push _push(*s);
opt_solver::toggle_objective _t(*s, true);
for (unsigned i = 0; i < objectives.size(); ++i) {
m_vars.push_back(s->add_objective(objectives[i].get()));
@ -76,7 +79,6 @@ namespace opt {
lbool is_sat = l_true;
// ready to test: is_sat = update_upper();
while (is_sat == l_true && !m_cancel) {
opt_solver::toggle_objective _t(*s, true);
is_sat = update_lower();
}
@ -89,12 +91,15 @@ namespace opt {
lbool optimize_objectives::update_lower() {
lbool is_sat = s->check_sat(0, 0);
if (is_sat == l_true) {
model_ref md;
s->get_model(md);
set_max(m_lower, s->get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < m_lower.size(); ++i) {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << "\n";);
verbose_stream() << "\n";
model_pp(verbose_stream(), *md););
expr_ref_vector disj(m);
expr_ref constraint(m);