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

fixing optimizer for multi-objectives and epsilon

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-22 10:36:13 +08:00
parent 3441fc2942
commit 36d7948399
6 changed files with 127 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/opt/opt_context.cpp
View file

@ -29,6 +29,9 @@ Notes:
#include "optimize_objectives.h"
#include "ast_pp.h"
#include "opt_solver.h"
#include "arith_decl_plugin.h"
#include "th_rewriter.h"
namespace opt {
@ -74,7 +77,7 @@ namespace opt {
}
// SASSERT(instanceof(*s, opt_solver));
// if (!instsanceof ...) { throw ... invalid usage ..}
is_sat = optimize_objectives(dynamic_cast<opt_solver&>(*s), m_objectives, m_is_max, values);
is_sat = optimize_objectives(dynamic_cast<opt_solver&>(*s), m_objectives, values);
std::cout << "is-sat: " << is_sat << "\n";
if (is_sat != l_true) {
@ -82,6 +85,9 @@ namespace opt {
}
for (unsigned i = 0; i < values.size(); ++i) {
if (!m_is_max[i]) {
values[i].neg();
}
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << values[i].to_string() << "\n";
}
}
@ -115,4 +121,18 @@ namespace opt {
}
}
void context::add_objective(app* t, bool is_max) {
expr_ref t1(t, m), t2(m);
th_rewriter rw(m);
if (!is_max) {
arith_util a(m);
t1 = a.mk_uminus(t);
}
rw(t1, t2);
SASSERT(is_app(t2));
m_objectives.push_back(to_app(t2));
m_is_max.push_back(is_max);
}
}

5
src/opt/opt_context.h
View file

@ -52,10 +52,7 @@ namespace opt {
m_weights.push_back(w);
}
void add_objective(app* t, bool is_max) {
m_objectives.push_back(t);
m_is_max.push_back(is_max);
}
void add_objective(app* t, bool is_max);
void add_hard_constraint(expr* f) {
m_hard_constraints.push_back(f);

39
src/opt/opt_solver.cpp
View file

@ -66,12 +66,16 @@ namespace opt {
TRACE("opt_solver_na2as", tout << "opt_opt_solver::check_sat_core: " << num_assumptions << "\n";);
lbool r = m_context.check(num_assumptions, assumptions);
if (r == l_true && m_objective_enabled) {
bool is_bounded = get_optimizer().maximize(m_objective_var);
if (is_bounded) {
m_objective_value = get_optimizer().get_objective_value(m_objective_var);
} else {
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
m_objective_value = r;
m_objective_values.reset();
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);
if (is_bounded) {
m_objective_values.push_back(get_optimizer().get_objective_value(v));
} else {
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
m_objective_values.push_back(r);
}
}
}
return r;
@ -123,16 +127,27 @@ namespace opt {
m_context.display(out);
}
void opt_solver::set_objective(app* term) {
m_objective_var = get_optimizer().add_objective(term);
smt::theory_var opt_solver::add_objective(app* term) {
m_objective_vars.push_back(get_optimizer().add_objective(term));
return m_objective_vars.back();
}
void opt_solver::toggle_objective(bool enable) {
m_objective_enabled = enable;
vector<opt_solver::inf_value> const& opt_solver::get_objective_values() {
return m_objective_values;
}
inf_eps_rational<inf_rational> opt_solver::get_objective_value() {
return m_objective_value;
void opt_solver::reset_objectives() {
m_objective_vars.reset();
m_objective_values.reset();
}
opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) {
s.m_objective_enabled = new_value;
}
opt_solver::toggle_objective::~toggle_objective() {
s.m_objective_enabled = m_old_value;
}
}

32
src/opt/opt_solver.h
View file

@ -1,21 +1,22 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Copyright (c) 2013 Microsoft Corporation
Module Name:
smt_solver.h
opt_solver.h
Abstract:
Wraps smt::kernel as a solver for the external API and cmd_context.
Wraps smt::kernel as a solver for optimization
Author:
Leonardo (leonardo) 2012-10-21
Anh-Dung Phan (t-anphan) 2013-10-16
Notes:
Based directly on smt_solver.
Variant of smt_solver that exposes kernel object.
--*/
#ifndef _OPT_SOLVER_H_
#define _OPT_SOLVER_H_
@ -33,13 +34,16 @@ Notes:
namespace opt {
class opt_solver : public solver_na2as {
public:
typedef inf_eps_rational<inf_rational> inf_value;
private:
smt_params m_params;
smt::kernel m_context;
progress_callback * m_callback;
symbol m_logic;
bool m_objective_enabled;
smt::theory_var m_objective_var;
inf_eps_rational<inf_rational> m_objective_value;
svector<smt::theory_var> m_objective_vars;
vector<inf_value> m_objective_values;
public:
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
virtual ~opt_solver();
@ -62,10 +66,18 @@ namespace opt {
virtual expr * get_assertion(unsigned idx) const;
virtual void display(std::ostream & out) const;
void set_objective(app* term);
void toggle_objective(bool enable);
smt::theory_var add_objective(app* term);
void reset_objectives();
vector<inf_value> const& get_objective_values();
inf_eps_rational<inf_rational> get_objective_value();
class toggle_objective {
opt_solver& s;
bool m_old_value;
public:
toggle_objective(opt_solver& s, bool new_value);
~toggle_objective();
};
private:
smt::theory_opt& get_optimizer();
};

87
src/opt/optimize_objectives.cpp
View file

@ -15,6 +15,26 @@ Author:
Notes:
Suppose we obtain solution t1 = k1, ..., tn = kn-epsilon
Assert:
t1 > k1 \/ t2 > k2 \/ ... \/ tn >= kn
If this solution is satisfiable, then for each t_i, maximize the
assignment and assert the new frontier.
Claim: we don't necessarily have to freeze assignments of
t_i when optimizing assignment for t_j
because the state will always satisfy the disjunction.
If one of the k_i is unbounded, then omit a disjunction for it.
Claim: the end result (when the constraints are no longer feasible)
is Pareto optimal, but convergence will probably not be as fast
as when fixing one parameter at a time.
E.g., a different approach is first to find a global maximal for one
variable. Then add a method to "freeze" that variable at the extremum if it is finite.
To do this, add lower and upper bounds for that variable using infinitesimals.
If the variable is unbounded, then this is of course not sufficient by itself.
--*/
#ifndef _OPT_OBJECTIVE_H_
@ -31,13 +51,14 @@ namespace opt {
*/
lbool mathsat_style_opt(
opt_solver& s,
app_ref_vector& objectives,
svector<bool> const& is_max,
app_ref_vector const& objectives,
vector<inf_eps_rational<inf_rational> >& values)
{
SASSERT(is_max.size() == objectives.size());
ast_manager& m = objectives.get_manager();
arith_util autil(m);
// First check_sat call for initialize theories
s.reset_objectives();
// First check_sat call to initialize theories
lbool is_sat = s.check_sat(0, 0);
if (is_sat == l_false) {
return is_sat;
@ -45,38 +66,41 @@ namespace opt {
s.push();
// Temporarily ignore the assertion to run the first objective function
//SASSERT(is_max.size() == 1);
ast_manager& m = objectives.get_manager();
arith_util autil(m);
bool ismax = is_max[0];
app_ref objective_var(m), objective_term(m), obj_eq(m);
objective_term = ismax?objectives[0].get():autil.mk_uminus(objectives[0].get());
sort* srt = m.get_sort(objective_term);
objective_var = m.mk_fresh_const("objective", srt);
obj_eq = autil.mk_eq(objective_var, objective_term);
s.assert_expr(obj_eq);
s.set_objective(objective_var); // NSB review: I would change signature of set_objective to take is_max and decide whether to add equation.
// Otherwise, the difference logic backends will not work.
s.toggle_objective(true);
opt_solver::toggle_objective _t(s, true);
for (unsigned i = 0; i < objectives.size(); ++i) {
s.add_objective(objectives[i]);
}
is_sat = s.check_sat(0, 0);
while (is_sat == l_true) {
// Extract values for objectives
inf_eps_rational<inf_rational> val;
val = ismax ? s.get_objective_value() : -s.get_objective_value();
// Check whether objective is unbounded
values.reset();
values.push_back(val);
values.append(s.get_objective_values());
IF_VERBOSE(1,
for (unsigned i = 0; i < values.size(); ++i) {
verbose_stream() << values[i] << " ";
}
verbose_stream() << "\n";);
expr_ref_vector disj(m);
expr_ref constraint(m), num(m);
for (unsigned i = 0; i < objectives.size(); ++i) {
if (!val.get_infinity().is_zero()) {
break;
if (!values[i].get_infinity().is_zero()) {
continue;
}
num = autil.mk_numeral(values[i].get_rational(), m.get_sort(objectives[i]));
SASSERT(values[i].get_infinitesimal().is_nonpos());
if (values[i].get_infinitesimal().is_neg()) {
disj.push_back(autil.mk_ge(objectives[i], num));
}
else {
disj.push_back(autil.mk_gt(objectives[i], num));
}
}
expr_ref constraint(m);
constraint = autil.mk_gt(objective_term, autil.mk_numeral(val.get_rational(), srt));
constraint = m.mk_or(disj.size(), disj.c_ptr());
s.assert_expr(constraint);
is_sat = s.check_sat(0, 0);
}
@ -86,7 +110,6 @@ namespace opt {
if (is_sat == l_undef) {
return is_sat;
}
//SASSERT(is_sat == l_false); // NSB review: not really water-tight with cancellation and with infinitesimal solutions.
return l_true;
}
@ -96,9 +119,9 @@ namespace opt {
*/
lbool optimize_objectives(opt_solver& s,
app_ref_vector& objectives, svector<bool> const& is_max,
app_ref_vector& objectives,
vector<inf_eps_rational<inf_rational> >& values) {
return mathsat_style_opt(s, objectives, is_max, values);
return mathsat_style_opt(s, objectives, values);
}
}

2
src/opt/optimize_objectives.h
View file

@ -28,7 +28,7 @@ namespace opt {
*/
lbool optimize_objectives(opt_solver& s,
app_ref_vector& objectives, svector<bool> const& is_max,
app_ref_vector& objectives,
vector<inf_eps_rational<inf_rational> >& values);
};