From c928f776da3a5893dd430bbbf0ac1e68e62ec17b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Aug 2014 08:39:31 -0700 Subject: [PATCH] working on mss/mus v2 Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 44 ++++++++++++++++++++++++++-------------- src/opt/mus.cpp | 50 ++++++++++++++++++++++++++++++++++++++++++++-- src/opt/mus.h | 10 ++++++++++ 3 files changed, 87 insertions(+), 17 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index c0bb1cd8f..4d64cbab9 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -61,6 +61,7 @@ Notes: #include "mss.h" #include "inc_sat_solver.h" #include "opt_context.h" +#include "pb_decl_plugin.h" using namespace opt; @@ -85,6 +86,7 @@ private: rational m_max_upper; bool m_hill_climb; bool m_all_cores; + bool m_add_upper_bound_block; public: maxres(context& c, @@ -97,7 +99,8 @@ public: m_trail(m), m_st(st), m_hill_climb(true), - m_all_cores(false) + m_all_cores(false), + m_add_upper_bound_block(false) { } @@ -281,13 +284,12 @@ public: */ lbool mus_mss2_solver() { + m_all_cores = true; + m_add_upper_bound_block = true; init(); init_local(); sls(); - m_all_cores = true; - NOT_IMPLEMENTED_YET(); vector > cores; - return l_undef; lbool is_sat = l_true; while (m_lower < m_upper && is_sat == l_true) { TRACE("opt", @@ -318,15 +320,21 @@ public: break; } SASSERT(is_sat == l_true); - // there is some best model, + + // TBD: there is some best model, + // retrieve it from the get_cores calls. // extend it to a maximal assignment // extracting the mss and mcs. + set_mus(false); ptr_vector mss, mcs; is_sat = m_mss(cores, mss, mcs); set_mus(true); if (is_sat != l_true) return is_sat; - // + model_ref mdl; + m_mss.get_model(mdl); // last model is best way to reduce search space. + update_assignment(mdl.get()); + is_sat = process_sat(mcs); } m_lower = m_upper; return l_true; @@ -446,14 +454,9 @@ public: lbool process_sat(ptr_vector const& corr_set) { expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); - if (corr_set.empty()) { - return l_true; - } - remove_core(corr_set); rational w = split_core(corr_set); - TRACE("opt", display_vec(tout << " corr_set: ", corr_set.size(), corr_set.c_ptr());); - cs_max_resolve(corr_set, w); + cs_max_resolve(corr_set, w); return l_true; } @@ -479,6 +482,7 @@ public: lbool process_unsat(ptr_vector const& core) { expr_ref fml(m); remove_core(core); + SASSERT(!core.empty()); rational w = split_core(core); TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); max_resolve(core, w); @@ -524,9 +528,8 @@ public: } rational split_core(ptr_vector const& core) { - + if (core.empty()) return rational(0); // find the minimal weight: - SASSERT(!core.empty()); rational w = get_weight(core[0]); for (unsigned i = 1; i < core.size(); ++i) { rational w2 = get_weight(core[i]); @@ -602,8 +605,8 @@ public: // cs is a correction set (a complement of a (maximal) satisfying assignment). void cs_max_resolve(ptr_vector const& cs, rational const& w) { + if (cs.empty()) return; TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr());); - SASSERT(!cs.empty()); expr_ref fml(m), asum(m); app_ref cls(m), d(m), dd(m); m_B.reset(); @@ -737,6 +740,17 @@ public: // verify_assignment(); IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";); + + if (m_add_upper_bound_block) { + pb_util u(m); + expr_ref_vector nsoft(m); + expr_ref fml(m); + for (unsigned i = 0; i < m_soft.size(); ++i) { + nsoft.push_back(m.mk_not(m_soft[i].get())); + } + fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); + s().assert_expr(fml); + } } void remove_soft(ptr_vector const& core, expr_ref_vector& asms) { diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 545aba2cc..932d9ccf7 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -22,7 +22,6 @@ Notes: #include "smt_literal.h" #include "mus.h" #include "ast_pp.h" -#include "model_smt2_pp.h" using namespace opt; @@ -34,9 +33,13 @@ struct mus::imp { expr_ref_vector m_cls2expr; obj_map m_expr2cls; volatile bool m_cancel; + model_ref m_model; + expr_ref_vector m_soft; + vector m_weights; + rational m_weight; imp(solver& s, ast_manager& m): - m_s(s), m(m), m_cls2expr(m), m_cancel(false) + m_s(s), m(m), m_cls2expr(m), m_cancel(false), m_soft(m) {} void reset() { @@ -100,6 +103,7 @@ struct mus::imp { case l_true: assumptions.push_back(cls); mus.push_back(cls_id); + update_model(); break; default: core_exprs.reset(); @@ -145,6 +149,40 @@ struct mus::imp { out << "\n"; } + void set_soft(unsigned sz, expr* const* soft, rational const* weights) { + m_model.reset(); + m_weight.reset(); + m_soft.append(sz, soft); + m_weights.append(sz, weights); + for (unsigned i = 0; i < sz; ++i) { + m_weight += weights[i]; + } + } + + void update_model() { + if (m_soft.empty()) return; + model_ref mdl; + expr_ref tmp(m); + m_s.get_model(mdl); + rational w; + for (unsigned i = 0; i < m_soft.size(); ++i) { + mdl->eval(m_soft[i].get(), tmp); + if (!m.is_true(tmp)) { + w += m_weights[i]; + } + } + if (w < m_weight || !m_model.get()) { + m_model = mdl; + m_weight = w; + } + } + + rational get_best_model(model_ref& mdl) { + mdl = m_model; + return m_weight; + } + + }; mus::mus(solver& s, ast_manager& m) { @@ -170,3 +208,11 @@ void mus::set_cancel(bool f) { void mus::reset() { m_imp->reset(); } + +void mus::set_soft(unsigned sz, expr* const* soft, rational const* weights) { + m_imp->set_soft(sz, soft, weights); +} + +rational mus::get_best_model(model_ref& mdl) { + return m_imp->get_best_model(mdl); +} diff --git a/src/opt/mus.h b/src/opt/mus.h index 94eb42cc6..12cd8b0b2 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -40,6 +40,16 @@ namespace opt { void reset(); void set_cancel(bool f); + + /** + Instrument MUS extraction to also provide the minimal + penalty model, if any is found. + The minimal penalty model has the least weight for the + supplied soft constraints. + */ + void set_soft(unsigned sz, expr* const* soft, rational const* weights); + rational get_best_model(model_ref& mdl); + }; };