From bf2a031f7bb728aaabbc2103df75f684c516c0f6 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:55 +0100 Subject: [PATCH] Revert "disjoint cores" This reverts commit e5aa79ba6a1f1e5e5ba38716c71247ccb70c0391. --- src/opt/mss_solver.cpp | 221 ++++++++++++----------------------------- src/opt/opt_params.pyg | 3 +- 2 files changed, 63 insertions(+), 161 deletions(-) diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index 1ac351855..d27b6300c 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -11,85 +11,45 @@ class mss_solver: public maxsmt_solver_base { private: typedef ptr_vector exprs; - typedef obj_hashtable expr_set; mss m_mss; unsigned m_index; - exprs m_asms; - unsigned m_mss_found; - vector m_cores; - unsigned m_core_idx; - model_ref m_last_model; - exprs m_mss_trail; - exprs m_mcs_trail; - unsigned_vector m_mss_trail_lim; - unsigned_vector m_mcs_trail_lim; + expr_ref_vector m_asms; unsigned m_max_mss; - bool m_disjoint_cores; public: mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_mss(c.get_solver(), m), m_index(id), - m_mss_found(0), - m_core_idx(0), - m_max_mss(UINT_MAX), - m_disjoint_cores(false) { + m_asms(m), + m_max_mss(UINT_MAX) { } virtual ~mss_solver() {} virtual lbool operator()() { if (!init()) return l_undef; - init_local(); - lbool is_sat = disjoint_cores(); - if (is_sat != l_true) return is_sat; - if (m_cores.size() == 0) return l_true; - update_model(); - exprs asms; - while (true) { - exprs mss, mcs; - mss.append(m_cores[m_core_idx]); - is_sat = cld(m_last_model, mss, mcs); - if (is_sat == l_undef || m.canceled()) return l_undef; - SASSERT(is_sat == l_true); - update_trails(mss, mcs); - if (m_core_idx < m_cores.size()-1) { - m_core_idx++; - } - else { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";); - if (++m_mss_found >= m_max_mss) return l_true; - asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr()))); - is_sat = backtrack(asms); - if (is_sat == l_false) { - SASSERT(m_core_idx == 0); - is_sat = disjoint_cores(asms); - } - if (is_sat == l_undef) return l_undef; - if (is_sat == l_false) return l_true; - } + init_asms(); + lbool is_sat = check_sat(m_asms); + if (is_sat == l_undef) return l_undef; + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + return l_true; } - return l_true; + return enumerate_mss(); } virtual void updt_params(params_ref& p) { maxsmt_solver_base::updt_params(p); opt_params _p(p); m_max_mss = _p.mss_max(); - m_disjoint_cores = _p.mss_disjoint_cores(); } private: - void init_local() { - m_cores.reset(); - m_core_idx = 0; - m_mss_found = 0; - m_last_model.reset(); - m_mss_trail.reset(); - m_mcs_trail.reset(); - m_mss_trail_lim.reset(); - m_mcs_trail_lim.reset(); + void init_asms() { m_asms.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* e = m_soft[i]; @@ -114,84 +74,42 @@ private: return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); } - lbool disjoint_cores(exprs const& asms) { - expr_set asm_lits, core_lits; - for (unsigned i = 0; i < asms.size(); ++i) { - asm_lits.insert(asms[i]); + lbool enumerate_mss() { + expr_ref_vector asms(m); + for (unsigned i = 0; i < m_max_mss; ++i) { + exprs mss, mcs; + lbool is_sat = next_mss(asms, mss, mcs); + if (is_sat == l_false && i == 0) return l_false; + if (is_sat == l_undef && i == 0) return l_undef; + if (is_sat == l_false || is_sat == l_undef) return l_true; + asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); } - lbool is_sat = l_false; - exprs core; - while (is_sat == l_false) { - exprs tmp_asms; - tmp_asms.append(asms); - tmp_asms.append(m_asms); - is_sat = check_sat(tmp_asms); - if (is_sat == l_true) { - update_model(); - } - else if (is_sat == l_false) { - core.reset(); - s().get_unsat_core(core); - for (unsigned i = 0; i < core.size();) { - if (asm_lits.contains(core[i])) { - core[i] = core.back(); - core.pop_back(); - } - else { - core_lits.insert(core[i]); - ++i; - } - } - if (core.empty()) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";); - return l_false; - } - if (m_disjoint_cores) { - m_cores.push_back(core); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";); - for (unsigned i = 0; i < m_asms.size();) { - if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) { - m_asms[i] = m_asms.back(); - m_asms.pop_back(); - } - else { - ++i; - } - } - } - else { - m_cores.push_back(m_asms); - m_asms.reset(); - } - } - } - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";); - // TODO: update m_lower? - return is_sat; + return l_true; } - lbool disjoint_cores() { - return disjoint_cores(exprs()); - } - - lbool backtrack(exprs& asms) { - SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size()); - lbool is_sat = l_false; - while (is_sat == l_false && m_core_idx > 0) { - m_core_idx--; - m_mss_trail.resize(m_mss_trail_lim.back()); - m_mss_trail_lim.pop_back(); - m_mcs_trail.resize(m_mcs_trail_lim.back()); - m_mcs_trail_lim.pop_back(); - exprs tmp_asms; - tmp_asms.append(asms); - get_trail_asms(tmp_asms); - is_sat = check_sat(tmp_asms); - if (is_sat == l_true) { - update_model(); - } + lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { + mss.reset(); + mcs.reset(); + lbool is_sat = check_sat(asms); + if (is_sat != l_true) return is_sat; + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + vector dummy; + push_exprs(mss, m_asms); + push_exprs(mss, asms); + is_sat = cld(mdl.get(), mss, mcs); + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); } - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";); + /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(is_sat != l_false); + if (is_sat == l_true) { + mdl.reset(); + m_mss.get_model(mdl); + update_assignment(mdl.get()); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + }*/ return is_sat; } @@ -200,19 +118,19 @@ private: undef.append(mss); update_sat(initial_model, sat, undef); lbool is_sat = l_true; - while (is_sat == l_true && !undef.empty()) { + while (is_sat == l_true) { expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - exprs asms; - asms.append(sat); - get_trail_asms(asms); - asms.push_back(asum); - is_sat = check_sat(asms); + sat.push_back(asum); + is_sat = check_sat(sat); + sat.pop_back(); if (is_sat == l_true) { - update_model(); - update_sat(m_last_model, sat, undef); + model_ref mdl; + s().get_model(mdl); + update_sat(mdl, sat, undef); + update_assignment(mdl.get()); } } - if (is_sat == l_false || undef.empty()) { + if (is_sat == l_false) { mss.reset(); mcs.reset(); mss.append(sat); @@ -222,26 +140,6 @@ private: return is_sat; } - void get_trail_asms(exprs& asms) { - asms.append(m_mss_trail); - for (unsigned i = 0; i < m_mcs_trail.size(); ++i) { - asms.push_back(m.mk_not(m_mcs_trail[i])); - } - } - - void update_trails(exprs const& mss, exprs const& mcs) { - m_mss_trail_lim.push_back(m_mss_trail.size()); - m_mcs_trail_lim.push_back(m_mcs_trail.size()); - m_mss_trail.append(mss); - m_mcs_trail.append(mcs); - } - - void update_model() { - m_last_model.reset(); - s().get_model(m_last_model); - update_assignment(m_last_model.get()); - } - void update_sat(model_ref mdl, exprs& sat, exprs& undef) { for (unsigned i = 0; i < undef.size();) { if (is_true(mdl.get(), undef[i])) { @@ -262,7 +160,12 @@ private: } lbool check_sat() { - return check_sat(exprs()); + expr_ref_vector dummy(m); + return check_sat(dummy); + } + + lbool check_sat(expr_ref_vector const& asms) { + return s().check_sat(asms); } lbool check_sat(exprs const& asms) { @@ -283,7 +186,7 @@ private: for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } - // TODO: DEBUG verify assignment? + // TODO: DEBUG verify assignment m_upper = upper; trace_bounds("mss-solver"); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 41548452a..4cb22389d 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -21,8 +21,7 @@ def_module_params('opt', ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), - ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'), - ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores') + ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') ))