mirror of
https://github.com/Z3Prover/z3
synced 2025-08-19 17:50:23 +00:00
A rudimentary version of MathSAT optimization
Remarks: (1) The core procedure accepts maximization only (2) Add lazy initialization to min_maximize_cmd (3) The procedure isn't working with composite objective yet.
This commit is contained in:
Anh-Dung Phan
parent
898609a3ef
commit
a44044fb15
8 changed files with 114 additions and 33 deletions
|
|
@ -22,18 +22,32 @@ Notes:
|
|||
#include "opt_context.h"
|
||||
|
||||
|
||||
class opt_context {
|
||||
cmd_context& ctx;
|
||||
scoped_ptr<opt::context> m_opt;
|
||||
public:
|
||||
opt_context(cmd_context& ctx): ctx(ctx) {}
|
||||
opt::context& operator()() {
|
||||
if (!m_opt) {
|
||||
m_opt = alloc(opt::context, ctx.m());
|
||||
}
|
||||
return *m_opt;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
class assert_weighted_cmd : public cmd {
|
||||
opt::context* m_opt_ctx;
|
||||
opt_context* m_opt_ctx;
|
||||
unsigned m_idx;
|
||||
expr_ref m_formula;
|
||||
expr* m_formula;
|
||||
rational m_weight;
|
||||
|
||||
public:
|
||||
assert_weighted_cmd(cmd_context& ctx, opt::context* opt_ctx):
|
||||
assert_weighted_cmd(cmd_context& ctx, opt_context* opt_ctx):
|
||||
cmd("assert-weighted"),
|
||||
m_opt_ctx(opt_ctx),
|
||||
m_idx(0),
|
||||
m_formula(ctx.m()),
|
||||
m_formula(0),
|
||||
m_weight(0)
|
||||
{}
|
||||
|
||||
|
|
@ -42,6 +56,9 @@ public:
|
|||
}
|
||||
|
||||
virtual void reset(cmd_context & ctx) {
|
||||
if (m_formula) {
|
||||
ctx.m().dec_ref(m_formula);
|
||||
}
|
||||
m_idx = 0;
|
||||
m_formula = 0;
|
||||
}
|
||||
|
|
@ -68,6 +85,7 @@ public:
|
|||
throw cmd_exception("Invalid type for expression. Expected Boolean type.");
|
||||
}
|
||||
m_formula = t;
|
||||
ctx.m().inc_ref(t);
|
||||
++m_idx;
|
||||
}
|
||||
|
||||
|
|
@ -76,7 +94,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
m_opt_ctx->add_soft_constraint(m_formula, m_weight);
|
||||
(*m_opt_ctx)().add_soft_constraint(m_formula, m_weight);
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
|
|
@ -91,10 +109,10 @@ public:
|
|||
// to do the feasibility check.
|
||||
class min_maximize_cmd : public cmd {
|
||||
bool m_is_max;
|
||||
opt::context* m_opt_ctx;
|
||||
opt_context* m_opt_ctx;
|
||||
|
||||
public:
|
||||
min_maximize_cmd(cmd_context& ctx, opt::context* opt_ctx, bool is_max):
|
||||
min_maximize_cmd(cmd_context& ctx, opt_context* opt_ctx, bool is_max):
|
||||
cmd(is_max?"maximize":"minimize"),
|
||||
m_is_max(is_max),
|
||||
m_opt_ctx(opt_ctx)
|
||||
|
|
@ -113,7 +131,7 @@ public:
|
|||
virtual void set_next_arg(cmd_context & ctx, expr * t) {
|
||||
// TODO: type check objective term. It should pass basic sanity being
|
||||
// integer, real (, bit-vector) or other supported objective function type.
|
||||
m_opt_ctx->add_objective(t, m_is_max);
|
||||
(*m_opt_ctx)().add_objective(t, m_is_max);
|
||||
}
|
||||
|
||||
virtual void failure_cleanup(cmd_context & ctx) {
|
||||
|
|
@ -127,9 +145,9 @@ public:
|
|||
};
|
||||
|
||||
class optimize_cmd : public cmd {
|
||||
opt::context* m_opt_ctx;
|
||||
opt_context* m_opt_ctx;
|
||||
public:
|
||||
optimize_cmd(opt::context* opt_ctx):
|
||||
optimize_cmd(opt_context* opt_ctx):
|
||||
cmd("optimize"),
|
||||
m_opt_ctx(opt_ctx)
|
||||
{}
|
||||
|
|
@ -145,9 +163,9 @@ public:
|
|||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
for (; it != end; ++it) {
|
||||
m_opt_ctx->add_hard_constraint(*it);
|
||||
(*m_opt_ctx)().add_hard_constraint(*it);
|
||||
}
|
||||
m_opt_ctx->optimize();
|
||||
(*m_opt_ctx)().optimize();
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -157,7 +175,7 @@ private:
|
|||
};
|
||||
|
||||
void install_opt_cmds(cmd_context & ctx) {
|
||||
opt::context* opt_ctx = alloc(opt::context, ctx.m());
|
||||
opt_context* opt_ctx = alloc(opt_context, ctx);
|
||||
ctx.insert(alloc(assert_weighted_cmd, ctx, opt_ctx));
|
||||
ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, true));
|
||||
ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, false));
|
||||
|
|
|
|||
|
|
@ -73,8 +73,13 @@ namespace opt {
|
|||
if (is_sat != l_true) {
|
||||
return;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < values.size(); ++i) {
|
||||
// display
|
||||
if (values[i]) {
|
||||
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << *values[i] << "\n";
|
||||
} else {
|
||||
std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> unbounded\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ namespace opt {
|
|||
|
||||
opt_solver::opt_solver(ast_manager & m, params_ref const & p, symbol const & l):
|
||||
solver_na2as(m),
|
||||
m_manager(m),
|
||||
m_params(p),
|
||||
m_context(m, m_params),
|
||||
m_objective_enabled(false) {
|
||||
|
|
@ -48,6 +49,7 @@ namespace opt {
|
|||
smt::context& ctx = m_context.get_context();
|
||||
smt::theory_id arith_id = m_context.m().get_family_id("arith");
|
||||
smt::theory* arith_theory = ctx.get_theory(arith_id);
|
||||
|
||||
if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) {
|
||||
return dynamic_cast<smt::theory_mi_arith&>(*arith_theory);
|
||||
}
|
||||
|
|
@ -64,8 +66,14 @@ namespace opt {
|
|||
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
|
||||
TRACE("opt_solver_na2as", tout << "smt_opt_solver::check_sat_core: " << num_assumptions << "\n";);
|
||||
lbool r = m_context.check(num_assumptions, assumptions);
|
||||
if (r == l_true &&& m_objective_enabled) {
|
||||
VERIFY(get_optimizer().max_min(m_objective_var, false));
|
||||
if (r == l_true && m_objective_enabled) {
|
||||
bool is_bounded = get_optimizer().max(m_objective_var);
|
||||
if (is_bounded) {
|
||||
m_objective_value = get_optimizer().get_objective_value(m_objective_var);
|
||||
} else {
|
||||
optional<rational> r;
|
||||
m_objective_value = r;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -123,4 +131,9 @@ namespace opt {
|
|||
void opt_solver::toggle_objective(bool enable) {
|
||||
m_objective_enabled = enable;
|
||||
}
|
||||
|
||||
optional<rational> opt_solver::get_objective_value() {
|
||||
return m_objective_value;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -37,6 +37,8 @@ namespace opt {
|
|||
symbol m_logic;
|
||||
bool m_objective_enabled;
|
||||
smt::theory_var m_objective_var;
|
||||
ast_manager& m_manager;
|
||||
optional<rational> m_objective_value;
|
||||
public:
|
||||
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
|
||||
virtual ~opt_solver();
|
||||
|
|
@ -61,6 +63,8 @@ namespace opt {
|
|||
|
||||
void set_objective(app* term);
|
||||
void toggle_objective(bool enable);
|
||||
|
||||
optional<rational> get_objective_value();
|
||||
private:
|
||||
smt::theory_opt& get_optimizer();
|
||||
};
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
|
||||
#include "optimize_objectives.h"
|
||||
#include "opt_solver.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
|
|
@ -31,23 +32,47 @@ namespace opt {
|
|||
lbool mathsat_style_opt(opt_solver& s,
|
||||
expr_ref_vector& objectives, svector<bool> const& is_max,
|
||||
vector<optional<rational> >& values) {
|
||||
lbool is_sat;
|
||||
is_sat = s.check_sat(0,0);
|
||||
if (is_sat != l_true) {
|
||||
return is_sat;
|
||||
enable_trace("maximize");
|
||||
// First check_sat call for initialize theories
|
||||
lbool is_sat = s.check_sat(0, 0);
|
||||
if (is_sat == l_false) {
|
||||
return l_false;
|
||||
}
|
||||
// assume that s is instrumented to produce locally optimal assignments.
|
||||
|
||||
// Assume there is only one objective function
|
||||
ast_manager& m = objectives.get_manager();
|
||||
arith_util autil(m);
|
||||
app* objective = is_max[0] ? (app*) objectives[0].get() : autil.mk_uminus(objectives[0].get());
|
||||
s.set_objective(objective);
|
||||
s.toggle_objective(true);
|
||||
is_sat = s.check_sat(0, 0);
|
||||
|
||||
while (is_sat != l_false) {
|
||||
model_ref model;
|
||||
s.get_model(model);
|
||||
// extract values for objectives.
|
||||
// store them in values.
|
||||
// assert there must be something better.
|
||||
is_sat = s.check_sat(0,0);
|
||||
}
|
||||
return l_true;
|
||||
// Extract values for objectives.
|
||||
optional<rational> rat;
|
||||
rat = s.get_objective_value();
|
||||
|
||||
// Unbounded objective
|
||||
if (!rat) {
|
||||
values.reset();
|
||||
values.push_back(rat);
|
||||
return l_true;
|
||||
}
|
||||
|
||||
// If values have initial data, they will be dropped.
|
||||
values.reset();
|
||||
values.push_back(rat);
|
||||
|
||||
// Assert there must be something better.
|
||||
expr_ref_vector assumptions(m);
|
||||
expr* bound = m.mk_fresh_const("bound", m.mk_bool_sort());
|
||||
assumptions.push_back(bound);
|
||||
expr* r = autil.mk_numeral(*rat, false);
|
||||
s.assert_expr(m.mk_eq(bound, is_max[0] ? autil.mk_gt(objectives[0].get(), r) : autil.mk_lt(objectives[0].get(), r)));
|
||||
is_sat = s.check_sat(1, assumptions.c_ptr());
|
||||
}
|
||||
|
||||
return l_true;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue