From 9f53a4aa18d7b4c2c51b17f427a3c547ce09f636 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Nov 2013 16:54:34 -0800 Subject: [PATCH] working on supporting multiple max-sat objectives Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 20 ++++++++++++++++--- src/opt/opt_context.cpp | 38 +++++++++++++++++++++++++++++++------ src/opt/opt_context.h | 7 ++++--- src/opt/opt_solver.cpp | 10 +++++++++- src/opt/opt_solver.h | 1 + src/opt/optsmt.cpp | 8 +------- src/opt/weighted_maxsat.cpp | 4 +--- 7 files changed, 65 insertions(+), 23 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index e08b9652f..ad5985d1c 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -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 " "; } 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); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 69ec91d85..ede93b34a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -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); + } } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 22fd5fd7a..c9388a56a 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -35,16 +35,17 @@ namespace opt { class opt_solver; class context { + typedef map map_t; ast_manager& m; expr_ref_vector m_hard_constraints; ref 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(); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index cd31e870c..750b8d700 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -168,7 +168,15 @@ namespace opt { vector 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(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); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 2c96e65ec..fa9a5e031 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -73,6 +73,7 @@ namespace opt { vector 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); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index a6dbd30ab..28dd95f67 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -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(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 { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 204e6d656..b74bb1ab8 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -226,9 +226,7 @@ namespace smt { m_cost_save.append(m_costs); } return !lits.empty(); - } - - + } }; }