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') + ))