From 3bbc09c1d2c800ea4ac646c66a886d25a87c4938 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Fri, 16 Feb 2018 14:44:22 +0000 Subject: [PATCH 01/10] MSS based MaxSMT solver --- src/opt/maxsmt.cpp | 4 ++ src/opt/mss_solver.cpp | 156 +++++++++++++++++++++++++++++++++++++++++ src/opt/mss_solver.h | 12 ++++ src/opt/opt_params.pyg | 8 +-- 4 files changed, 176 insertions(+), 4 deletions(-) create mode 100755 src/opt/mss_solver.cpp create mode 100755 src/opt/mss_solver.h diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 91e843ca0..9bc4f4f14 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -21,6 +21,7 @@ Notes: #include "opt/maxsmt.h" #include "opt/maxres.h" #include "opt/wmax.h" +#include "opt/mss_solver.h" #include "ast/ast_pp.h" #include "util/uint_set.h" #include "opt/opt_context.h" @@ -240,6 +241,9 @@ namespace opt { else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } + else if (maxsat_engine == symbol("mss")) { + m_msolver = mk_mss_solver(m_c, m_index, m_weights, m_soft_constraints); + } else if (maxsat_engine == symbol("wmax")) { m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp new file mode 100755 index 000000000..501b43ee4 --- /dev/null +++ b/src/opt/mss_solver.cpp @@ -0,0 +1,156 @@ +#include "solver/solver.h" +#include "opt/maxsmt.h" +#include "opt/mss_solver.h" +#include "opt/mss.h" +#include "opt/opt_context.h" +#include "opt/opt_params.hpp" + +using namespace opt; + +class mss_solver: public maxsmt_solver_base { + +private: + typedef ptr_vector exprs; + mss m_mss; + unsigned m_index; + expr_ref_vector m_asms; + unsigned m_max_mss; + +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_asms(m), + m_max_mss(UINT_MAX) { + } + + virtual ~mss_solver() {} + + virtual lbool operator()() { + if (!init()) return l_undef; + 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 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(); + } + +private: + void init_asms() { + m_asms.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr* e = m_soft[i]; + m_asms.push_back(relax_and_assert(e)); + } + } + + expr_ref relax_and_assert(expr* e) { + expr_ref asum(m); + if (is_literal(e)) { + asum = e; + } + else { + asum = mk_fresh_bool("r"); + e = m.mk_iff(asum, e); + s().assert_expr(e); + } + return asum; + } + + bool is_literal(expr* l) { + return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); + } + + 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()))); + } + return l_true; + } + + 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 = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(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; + } + + void push_exprs(exprs& dst, expr_ref_vector const& src) { + for (unsigned i = 0; i < src.size(); ++i) { + dst.push_back(src[i]); + } + } + + lbool check_sat() { + expr_ref_vector dummy(m); + return check_sat(dummy); + } + + lbool check_sat(expr_ref_vector const& asms) { + return s().check_sat(asms); + } + + void update_assignment(model* mdl) { + rational upper(0); + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (!is_true(mdl, m_soft[i])) { + upper += m_weights[i]; + } + } + if (upper > m_upper) return; + if (!m_c.verify_model(m_index, mdl, upper)) return; + m_model = mdl; + m_c.model_updated(mdl); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment[i] = is_true(m_soft[i]); + } + // TODO: DEBUG verify assignment + m_upper = upper; + trace_bounds("mss-solver"); + } + + bool is_true(model* mdl, expr* e) { + expr_ref tmp(m); + return mdl->eval(e, tmp, true) && m.is_true(tmp); + } + + bool is_true(expr* e) { + return is_true(m_model.get(), e); + } +}; + +maxsmt_solver_base* opt::mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { + return alloc(mss_solver, c, id, ws, soft); +} diff --git a/src/opt/mss_solver.h b/src/opt/mss_solver.h new file mode 100755 index 000000000..5c274cd4c --- /dev/null +++ b/src/opt/mss_solver.h @@ -0,0 +1,12 @@ +#ifndef MSS_SOLVER_H_ +#define MSS_SOLVER_H_ + +#include "opt/maxsmt.h" + +namespace opt { + + maxsmt_solver_base* mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft); + +} + +#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 1d6d7ee6a..4cb22389d 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,13 +2,13 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), + ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), @@ -20,8 +20,8 @@ def_module_params('opt', ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), ('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') - + ('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') )) From 3a7efb91ae073c346716b4213c06d32fc39510a6 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Fri, 16 Feb 2018 19:48:29 +0000 Subject: [PATCH 02/10] implemented CLD --- src/opt/mss.cpp | 12 ++++---- src/opt/mss_solver.cpp | 62 ++++++++++++++++++++++++++++++++++++++---- 2 files changed, 62 insertions(+), 12 deletions(-) diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index cc0fa8d7d..47f4b6e02 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -155,10 +155,10 @@ namespace opt { lbool is_sat = l_true; for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) { bool has_mcs = false; - bool is_last = i + 1 < m_cores.size(); + bool not_last = i + 1 < m_cores.size(); SASSERT(check_invariant()); update_core(m_cores[i]); // remove members of mss - is_sat = process_core(1, m_cores[i], has_mcs, is_last); + is_sat = process_core(1, m_cores[i], has_mcs, not_last); } if (is_sat == l_true) { SASSERT(check_invariant()); @@ -183,7 +183,7 @@ namespace opt { // at least one literal in core is false in current model. // pick literals in core that are not yet in mss. // - lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) { + lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) { SASSERT(sz > 0); if (core.empty()) { return l_true; @@ -191,7 +191,7 @@ namespace opt { if (m.canceled()) { return l_undef; } - if (sz == 1 && core.size() == 1 && is_last && !has_mcs) { + if (sz == 1 && core.size() == 1 && not_last && !has_mcs) { // there has to be at least one false // literal in the core. TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";); @@ -214,7 +214,7 @@ namespace opt { SASSERT(m_mss_set.contains(core[i])); }); update_core(core); - return process_core(2*sz, core, has_mcs, is_last); + return process_core(2*sz, core, has_mcs, not_last); case l_false: if (sz == 1) { has_mcs = true; @@ -232,7 +232,7 @@ namespace opt { } update_core(core); } - return process_core(1, core, has_mcs, is_last); + return process_core(1, core, has_mcs, not_last); case l_undef: return l_undef; } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index 501b43ee4..d27b6300c 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -98,15 +98,61 @@ private: vector dummy; push_exprs(mss, m_asms); push_exprs(mss, asms); - is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(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";); + 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";); + } + /*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; } + lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) { + exprs sat, undef; + undef.append(mss); + update_sat(initial_model, sat, undef); + lbool is_sat = l_true; + while (is_sat == l_true) { + expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); + sat.push_back(asum); + is_sat = check_sat(sat); + sat.pop_back(); + if (is_sat == l_true) { + model_ref mdl; + s().get_model(mdl); + update_sat(mdl, sat, undef); + update_assignment(mdl.get()); + } + } + if (is_sat == l_false) { + mss.reset(); + mcs.reset(); + mss.append(sat); + mcs.append(undef); + is_sat = l_true; + } + return is_sat; + } + + void update_sat(model_ref mdl, exprs& sat, exprs& undef) { + for (unsigned i = 0; i < undef.size();) { + if (is_true(mdl.get(), undef[i])) { + sat.push_back(undef[i]); + undef[i] = undef.back(); + undef.pop_back(); + } + else { + ++i; + } + } + } + void push_exprs(exprs& dst, expr_ref_vector const& src) { for (unsigned i = 0; i < src.size(); ++i) { dst.push_back(src[i]); @@ -122,6 +168,10 @@ private: return s().check_sat(asms); } + lbool check_sat(exprs const& asms) { + return s().check_sat(asms.size(), asms.c_ptr()); + } + void update_assignment(model* mdl) { rational upper(0); for (unsigned i = 0; i < m_soft.size(); ++i) { From e5aa79ba6a1f1e5e5ba38716c71247ccb70c0391 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Mon, 19 Feb 2018 13:29:15 +0000 Subject: [PATCH 03/10] disjoint cores --- src/opt/mss_solver.cpp | 221 +++++++++++++++++++++++++++++------------ src/opt/opt_params.pyg | 3 +- 2 files changed, 161 insertions(+), 63 deletions(-) diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index d27b6300c..1ac351855 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -11,45 +11,85 @@ class mss_solver: public maxsmt_solver_base { private: typedef ptr_vector exprs; + typedef obj_hashtable expr_set; mss m_mss; unsigned m_index; - expr_ref_vector m_asms; + 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; 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_asms(m), - m_max_mss(UINT_MAX) { + m_mss_found(0), + m_core_idx(0), + m_max_mss(UINT_MAX), + m_disjoint_cores(false) { } virtual ~mss_solver() {} virtual lbool operator()() { if (!init()) return l_undef; - 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; + 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; + } } - return enumerate_mss(); + return l_true; } 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_asms() { + 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(); m_asms.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* e = m_soft[i]; @@ -74,42 +114,84 @@ private: return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); } - 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 disjoint_cores(exprs const& asms) { + expr_set asm_lits, core_lits; + for (unsigned i = 0; i < asms.size(); ++i) { + asm_lits.insert(asms[i]); } - return l_true; + 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; } - 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";); + 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(); + } } - /*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";); - }*/ + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";); return is_sat; } @@ -118,19 +200,19 @@ private: undef.append(mss); update_sat(initial_model, sat, undef); lbool is_sat = l_true; - while (is_sat == l_true) { + while (is_sat == l_true && !undef.empty()) { expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - sat.push_back(asum); - is_sat = check_sat(sat); - sat.pop_back(); + exprs asms; + asms.append(sat); + get_trail_asms(asms); + asms.push_back(asum); + is_sat = check_sat(asms); if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - update_sat(mdl, sat, undef); - update_assignment(mdl.get()); + update_model(); + update_sat(m_last_model, sat, undef); } } - if (is_sat == l_false) { + if (is_sat == l_false || undef.empty()) { mss.reset(); mcs.reset(); mss.append(sat); @@ -140,6 +222,26 @@ 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])) { @@ -160,12 +262,7 @@ private: } lbool check_sat() { - expr_ref_vector dummy(m); - return check_sat(dummy); - } - - lbool check_sat(expr_ref_vector const& asms) { - return s().check_sat(asms); + return check_sat(exprs()); } lbool check_sat(exprs const& asms) { @@ -186,7 +283,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 4cb22389d..41548452a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -21,7 +21,8 @@ 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.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'), + ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores') )) From ab8d3cdc447e278465563294d44c73ea29d098af Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Tue, 24 Apr 2018 17:59:21 +0100 Subject: [PATCH 04/10] WMax conflict budget bug fix --- src/opt/opt_context.cpp | 4 ++-- src/opt/opt_params.pyg | 2 +- src/opt/wmax.cpp | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2f6bad9e8..4bbbc3865 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -398,10 +398,10 @@ namespace opt { /** \brief there is no need to use push/pop when all objectives are maxsat and engine - is maxres. + is maxres or mss. */ bool context::scoped_lex() { - if (m_maxsat_engine == symbol("maxres")) { + if (m_maxsat_engine == symbol("maxres") || m_maxsat_engine == symbol("mss")) { for (unsigned i = 0; i < m_objectives.size(); ++i) { if (m_objectives[i].m_type != O_MAXSMT) return true; } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 41548452a..e06836f61 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), - ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), + ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 52b87e536..513c68d6e 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,6 +84,9 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_undef) { + break; + } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -97,9 +100,6 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } - else { - //DEBUG_CODE(verify_cores(cores);); - } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); From 047f6c558c156ebe5e116c7d9f26e70026007336 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 26 Apr 2018 16:36:14 -0400 Subject: [PATCH 05/10] fix memory leak related to #1575 --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0f9d42b3d..126594b06 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8096,7 +8096,7 @@ namespace smt { rational nn1Len, nn2Len; bool nn1Len_exists = get_len_value(lhs, nn1Len); bool nn2Len_exists = get_len_value(rhs, nn2Len); - expr * emptyStr = mk_string(""); + expr_ref emptyStr(mk_string(""), m); if (nn1Len_exists && nn1Len.is_zero()) { if (!in_same_eqc(lhs, emptyStr) && rhs != emptyStr) { From 37852807b0fa0fb0ee1799dbc2c46df46b89ac47 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:45 +0100 Subject: [PATCH 06/10] Revert "WMax conflict budget bug fix" This reverts commit ab8d3cdc447e278465563294d44c73ea29d098af. --- src/opt/opt_context.cpp | 4 ++-- src/opt/opt_params.pyg | 2 +- src/opt/wmax.cpp | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 4bbbc3865..2f6bad9e8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -398,10 +398,10 @@ namespace opt { /** \brief there is no need to use push/pop when all objectives are maxsat and engine - is maxres or mss. + is maxres. */ bool context::scoped_lex() { - if (m_maxsat_engine == symbol("maxres") || m_maxsat_engine == symbol("mss")) { + if (m_maxsat_engine == symbol("maxres")) { for (unsigned i = 0; i < m_objectives.size(); ++i) { if (m_objectives[i].m_type != O_MAXSMT) return true; } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index e06836f61..41548452a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), - ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), + ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 513c68d6e..52b87e536 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,9 +84,6 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } - if (is_sat == l_undef) { - break; - } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -100,6 +97,9 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } + else { + //DEBUG_CODE(verify_cores(cores);); + } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); From bf2a031f7bb728aaabbc2103df75f684c516c0f6 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:55 +0100 Subject: [PATCH 07/10] 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') )) From 7e8ed0762d29bbfc80716937183772e388802f1c Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:58 +0100 Subject: [PATCH 08/10] Revert "implemented CLD" This reverts commit 3a7efb91ae073c346716b4213c06d32fc39510a6. --- src/opt/mss.cpp | 12 ++++---- src/opt/mss_solver.cpp | 62 ++++-------------------------------------- 2 files changed, 12 insertions(+), 62 deletions(-) diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index 47f4b6e02..cc0fa8d7d 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -155,10 +155,10 @@ namespace opt { lbool is_sat = l_true; for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) { bool has_mcs = false; - bool not_last = i + 1 < m_cores.size(); + bool is_last = i + 1 < m_cores.size(); SASSERT(check_invariant()); update_core(m_cores[i]); // remove members of mss - is_sat = process_core(1, m_cores[i], has_mcs, not_last); + is_sat = process_core(1, m_cores[i], has_mcs, is_last); } if (is_sat == l_true) { SASSERT(check_invariant()); @@ -183,7 +183,7 @@ namespace opt { // at least one literal in core is false in current model. // pick literals in core that are not yet in mss. // - lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) { + lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) { SASSERT(sz > 0); if (core.empty()) { return l_true; @@ -191,7 +191,7 @@ namespace opt { if (m.canceled()) { return l_undef; } - if (sz == 1 && core.size() == 1 && not_last && !has_mcs) { + if (sz == 1 && core.size() == 1 && is_last && !has_mcs) { // there has to be at least one false // literal in the core. TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";); @@ -214,7 +214,7 @@ namespace opt { SASSERT(m_mss_set.contains(core[i])); }); update_core(core); - return process_core(2*sz, core, has_mcs, not_last); + return process_core(2*sz, core, has_mcs, is_last); case l_false: if (sz == 1) { has_mcs = true; @@ -232,7 +232,7 @@ namespace opt { } update_core(core); } - return process_core(1, core, has_mcs, not_last); + return process_core(1, core, has_mcs, is_last); case l_undef: return l_undef; } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index d27b6300c..501b43ee4 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -98,61 +98,15 @@ private: 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";); - } - /*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";); - }*/ + is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(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; } - lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) { - exprs sat, undef; - undef.append(mss); - update_sat(initial_model, sat, undef); - lbool is_sat = l_true; - while (is_sat == l_true) { - expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - sat.push_back(asum); - is_sat = check_sat(sat); - sat.pop_back(); - if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - update_sat(mdl, sat, undef); - update_assignment(mdl.get()); - } - } - if (is_sat == l_false) { - mss.reset(); - mcs.reset(); - mss.append(sat); - mcs.append(undef); - is_sat = l_true; - } - return is_sat; - } - - void update_sat(model_ref mdl, exprs& sat, exprs& undef) { - for (unsigned i = 0; i < undef.size();) { - if (is_true(mdl.get(), undef[i])) { - sat.push_back(undef[i]); - undef[i] = undef.back(); - undef.pop_back(); - } - else { - ++i; - } - } - } - void push_exprs(exprs& dst, expr_ref_vector const& src) { for (unsigned i = 0; i < src.size(); ++i) { dst.push_back(src[i]); @@ -168,10 +122,6 @@ private: return s().check_sat(asms); } - lbool check_sat(exprs const& asms) { - return s().check_sat(asms.size(), asms.c_ptr()); - } - void update_assignment(model* mdl) { rational upper(0); for (unsigned i = 0; i < m_soft.size(); ++i) { From e1d7f5deba5398e8471ae53d63fce59c690c731e Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:40:00 +0100 Subject: [PATCH 09/10] Revert "MSS based MaxSMT solver" This reverts commit 3bbc09c1d2c800ea4ac646c66a886d25a87c4938. --- src/opt/maxsmt.cpp | 4 -- src/opt/mss_solver.cpp | 156 ----------------------------------------- src/opt/mss_solver.h | 12 ---- src/opt/opt_params.pyg | 8 +-- 4 files changed, 4 insertions(+), 176 deletions(-) delete mode 100755 src/opt/mss_solver.cpp delete mode 100755 src/opt/mss_solver.h diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9bc4f4f14..91e843ca0 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -21,7 +21,6 @@ Notes: #include "opt/maxsmt.h" #include "opt/maxres.h" #include "opt/wmax.h" -#include "opt/mss_solver.h" #include "ast/ast_pp.h" #include "util/uint_set.h" #include "opt/opt_context.h" @@ -241,9 +240,6 @@ namespace opt { else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } - else if (maxsat_engine == symbol("mss")) { - m_msolver = mk_mss_solver(m_c, m_index, m_weights, m_soft_constraints); - } else if (maxsat_engine == symbol("wmax")) { m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp deleted file mode 100755 index 501b43ee4..000000000 --- a/src/opt/mss_solver.cpp +++ /dev/null @@ -1,156 +0,0 @@ -#include "solver/solver.h" -#include "opt/maxsmt.h" -#include "opt/mss_solver.h" -#include "opt/mss.h" -#include "opt/opt_context.h" -#include "opt/opt_params.hpp" - -using namespace opt; - -class mss_solver: public maxsmt_solver_base { - -private: - typedef ptr_vector exprs; - mss m_mss; - unsigned m_index; - expr_ref_vector m_asms; - unsigned m_max_mss; - -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_asms(m), - m_max_mss(UINT_MAX) { - } - - virtual ~mss_solver() {} - - virtual lbool operator()() { - if (!init()) return l_undef; - 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 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(); - } - -private: - void init_asms() { - m_asms.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - expr* e = m_soft[i]; - m_asms.push_back(relax_and_assert(e)); - } - } - - expr_ref relax_and_assert(expr* e) { - expr_ref asum(m); - if (is_literal(e)) { - asum = e; - } - else { - asum = mk_fresh_bool("r"); - e = m.mk_iff(asum, e); - s().assert_expr(e); - } - return asum; - } - - bool is_literal(expr* l) { - return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); - } - - 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()))); - } - return l_true; - } - - 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 = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(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; - } - - void push_exprs(exprs& dst, expr_ref_vector const& src) { - for (unsigned i = 0; i < src.size(); ++i) { - dst.push_back(src[i]); - } - } - - lbool check_sat() { - expr_ref_vector dummy(m); - return check_sat(dummy); - } - - lbool check_sat(expr_ref_vector const& asms) { - return s().check_sat(asms); - } - - void update_assignment(model* mdl) { - rational upper(0); - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (!is_true(mdl, m_soft[i])) { - upper += m_weights[i]; - } - } - if (upper > m_upper) return; - if (!m_c.verify_model(m_index, mdl, upper)) return; - m_model = mdl; - m_c.model_updated(mdl); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_assignment[i] = is_true(m_soft[i]); - } - // TODO: DEBUG verify assignment - m_upper = upper; - trace_bounds("mss-solver"); - } - - bool is_true(model* mdl, expr* e) { - expr_ref tmp(m); - return mdl->eval(e, tmp, true) && m.is_true(tmp); - } - - bool is_true(expr* e) { - return is_true(m_model.get(), e); - } -}; - -maxsmt_solver_base* opt::mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { - return alloc(mss_solver, c, id, ws, soft); -} diff --git a/src/opt/mss_solver.h b/src/opt/mss_solver.h deleted file mode 100755 index 5c274cd4c..000000000 --- a/src/opt/mss_solver.h +++ /dev/null @@ -1,12 +0,0 @@ -#ifndef MSS_SOLVER_H_ -#define MSS_SOLVER_H_ - -#include "opt/maxsmt.h" - -namespace opt { - - maxsmt_solver_base* mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft); - -} - -#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 4cb22389d..1d6d7ee6a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,13 +2,13 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'), + ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), @@ -20,8 +20,8 @@ def_module_params('opt', ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), ('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') + ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core') + )) From 24b35fb9256f2bf799cadae819334d8d52a3e686 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:42:55 +0100 Subject: [PATCH 10/10] WMax conflict budget bug fix --- src/opt/wmax.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 52b87e536..513c68d6e 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,6 +84,9 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_undef) { + break; + } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -97,9 +100,6 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } - else { - //DEBUG_CODE(verify_cores(cores);); - } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax");