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

working on supporting multiple max-sat objectives

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-08 16:54:34 -08:00
parent f350efffc7
commit 9f53a4aa18
7 changed files with 65 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/opt/opt_cmds.cpp
View file

@ -50,6 +50,7 @@ class assert_weighted_cmd : public cmd {
unsigned m_idx;
expr* m_formula;
rational m_weight;
symbol m_id;
public:
assert_weighted_cmd(cmd_context& ctx, opt_context& opt_ctx):
@ -70,15 +71,22 @@ public:
}
m_idx = 0;
m_formula = 0;
m_id = symbol::null;
}
virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
virtual unsigned get_arity() const { return 2; }
virtual unsigned get_arity() const { return VAR_ARITY; }
// command invocation
virtual void prepare(cmd_context & ctx) {}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_idx == 0) return CPK_EXPR; return CPK_NUMERAL; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
switch(m_idx) {
case 0: return CPK_EXPR;
case 1: return CPK_NUMERAL;
default: return CPK_SYMBOL;
}
}
virtual void set_next_arg(cmd_context & ctx, rational const & val) {
SASSERT(m_idx == 1);
if (!val.is_pos()) {
@ -98,12 +106,18 @@ public:
++m_idx;
}
virtual void set_next_arg(cmd_context & ctx, symbol const& s) {
SASSERT(m_idx > 1);
m_id = s;
++m_idx;
}
virtual void failure_cleanup(cmd_context & ctx) {
reset(ctx);
}
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, m_id);
reset(ctx);
}

38
src/opt/opt_context.cpp
View file

@ -32,14 +32,29 @@ namespace opt {
context::context(ast_manager& m):
m(m),
m_hard_constraints(m),
m_optsmt(m),
m_maxsmt(m)
m_optsmt(m)
{
m_params.set_bool("model", true);
m_params.set_bool("unsat_core", true);
m_solver = alloc(opt_solver, m, m_params, symbol());
}
context::~context() {
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
}
void context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
maxsmt* ms;
if (!m_maxsmts.find(id, ms)) {
ms = alloc(maxsmt, m);
m_maxsmts.insert(id, ms);
}
ms->add(f, w);
}
void context::optimize() {
opt_solver& s = *m_solver.get();
@ -48,8 +63,13 @@ namespace opt {
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
s.assert_expr(m_hard_constraints[i].get());
}
lbool is_sat = m_maxsmt(s);
lbool is_sat = l_true;
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; is_sat == l_true && it != end; ++it) {
maxsmt* ms = it->m_value;
is_sat = (*ms)(s);
}
if (is_sat == l_true) {
is_sat = m_optsmt(s);
}
@ -60,7 +80,10 @@ namespace opt {
m_solver->set_cancel(f);
}
m_optsmt.set_cancel(f);
m_maxsmt.set_cancel(f);
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
it->m_value->set_cancel(f);
}
}
void context::collect_statistics(statistics& stats) {
@ -79,7 +102,10 @@ namespace opt {
m_solver->updt_params(m_params);
}
m_optsmt.updt_params(m_params);
m_maxsmt.updt_params(m_params);
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
it->m_value->updt_params(m_params);
}
}

7
src/opt/opt_context.h
View file

@ -35,16 +35,17 @@ namespace opt {
class opt_solver;
class context {
typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
ast_manager& m;
expr_ref_vector m_hard_constraints;
ref<opt_solver> m_solver;
params_ref m_params;
optsmt m_optsmt;
maxsmt m_maxsmt;
map_t m_maxsmts;
public:
context(ast_manager& m);
void add_soft_constraint(expr* f, rational const& w) { m_maxsmt.add(f, w); }
~context();
void add_soft_constraint(expr* f, rational const& w, symbol const& id);
void add_objective(app* t, bool is_max) { m_optsmt.add(t, is_max); }
void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); }
void optimize();

10
src/opt/opt_solver.cpp
View file

@ -168,7 +168,15 @@ namespace opt {
vector<inf_eps> const& opt_solver::get_objective_values() {
return m_objective_values;
}
expr_ref opt_solver::block_upper_bound(unsigned var, inf_eps const& val) {
smt::theory_opt& opt = get_optimizer();
SASSERT(typeid(smt::theory_inf_arith) == typeid(opt));
smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt);
smt::theory_var v = m_objective_vars[var];
return expr_ref(th.block_upper_bound(v, val), m);
}
expr_ref opt_solver::block_lower_bound(unsigned var, inf_eps const& val) {
if (val.get_infinity().is_pos()) {
return expr_ref(m.mk_false(), m);

1
src/opt/opt_solver.h
View file

@ -73,6 +73,7 @@ namespace opt {
vector<inf_eps> const& get_objective_values();
expr_ref block_lower_bound(unsigned obj_index, inf_eps const& val);
expr_ref block_upper_bound(unsigned obj_index, inf_eps const& val);
static opt_solver& to_opt(solver& s);

8
src/opt/optsmt.cpp
View file

@ -259,13 +259,7 @@ namespace opt {
// force lower_bound(i) <= objective_value(i)
void optsmt::commit_assignment(unsigned i) {
smt::theory_var v = m_vars[i];
// TBD: this should be a method on all optimization solvers.
smt::theory_opt& opt = s->get_optimizer();
SASSERT(typeid(smt::theory_inf_arith) == typeid(opt));
smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt);
s->assert_expr(th.block_upper_bound(v, get_lower(i)));
s->assert_expr(s->block_upper_bound(i, get_lower(i)));
}
void optsmt::display(std::ostream& out) const {

4
src/opt/weighted_maxsat.cpp
View file

@ -226,9 +226,7 @@ namespace smt {
m_cost_save.append(m_costs);
}
return !lits.empty();
}
}
};
}