diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp index cb579b9ef..7e5ac38f8 100644 --- a/src/opt/bcd2.cpp +++ b/src/opt/bcd2.cpp @@ -99,9 +99,9 @@ namespace opt { } public: - bcd2(opt_solver* s, ast_manager& m, params_ref& p, + bcd2(context& c, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), + maxsmt_solver_base(c, ws, soft), pb(m), m_soft_aux(m), m_trail(m), @@ -116,7 +116,6 @@ namespace opt { expr_ref fml(m), r(m); lbool is_sat = l_undef; expr_ref_vector asms(m); - enable_sls(); solver::scoped_push _scope1(s()); init(); init_bcd(); @@ -400,9 +399,9 @@ namespace opt { } }; - maxsmt_solver_base* opt::mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* opt::mk_bcd2(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(bcd2, s, m, p, ws, soft); + return alloc(bcd2, c, ws, soft); } } diff --git a/src/opt/bcd2.h b/src/opt/bcd2.h index db08b15ef..6528c2807 100644 --- a/src/opt/bcd2.h +++ b/src/opt/bcd2.h @@ -23,7 +23,6 @@ Notes: #include "maxsmt.h" namespace opt { - maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_bcd2(context& c, vector const& ws, expr_ref_vector const& soft); } #endif diff --git a/src/opt/bvsls_opt_solver.cpp b/src/opt/bvsls_opt_solver.cpp deleted file mode 100644 index 9bb858856..000000000 --- a/src/opt/bvsls_opt_solver.cpp +++ /dev/null @@ -1,123 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - bvsls_opt_solver.cpp - -Abstract: - - Uses the bvsls engine for optimization - -Author: - - Christoph (cwinter) 2014-3-28 - -Notes: - ---*/ - -#include "bvsls_opt_solver.h" - -namespace opt { - - bvsls_opt_solver::bvsls_opt_solver(ast_manager & m, params_ref const & p) : - opt_solver(m, p, symbol("QF_BV")), - m_manager(m), - m_params(p), - m_engine(m, p) - { - } - - bvsls_opt_solver::~bvsls_opt_solver() - { - } - - void bvsls_opt_solver::updt_params(params_ref & p) - { - opt_solver::updt_params(p); - m_engine.updt_params(p); - } - - void bvsls_opt_solver::collect_param_descrs(param_descrs & r) - { - opt_solver::collect_param_descrs(r); - } - - void bvsls_opt_solver::collect_statistics(statistics & st) const - { - opt_solver::collect_statistics(st); - } - - void bvsls_opt_solver::assert_expr(expr * t) { - m_engine.assert_expr(t); - } - - void bvsls_opt_solver::push_core() - { - opt_solver::push_core(); - } - - void bvsls_opt_solver::pop_core(unsigned n) - { - opt_solver::pop_core(n); - } - - lbool bvsls_opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) - { - SASSERT(num_assumptions == 0); - SASSERT(assumptions == 0); - return m_engine(); - } - - void bvsls_opt_solver::get_unsat_core(ptr_vector & r) - { - NOT_IMPLEMENTED_YET(); - } - - void bvsls_opt_solver::get_model(model_ref & m) - { - NOT_IMPLEMENTED_YET(); - } - - proof * bvsls_opt_solver::get_proof() - { - NOT_IMPLEMENTED_YET(); - } - - std::string bvsls_opt_solver::reason_unknown() const - { - NOT_IMPLEMENTED_YET(); - } - - void bvsls_opt_solver::get_labels(svector & r) - { - opt_solver::get_labels(r); - } - - void bvsls_opt_solver::set_cancel(bool f) - { - opt_solver::set_cancel(f); - m_engine.set_cancel(f); - } - - void bvsls_opt_solver::set_progress_callback(progress_callback * callback) - { - opt_solver::set_progress_callback(callback); - } - - unsigned bvsls_opt_solver::get_num_assertions() const - { - NOT_IMPLEMENTED_YET(); - } - - expr * bvsls_opt_solver::get_assertion(unsigned idx) const - { - NOT_IMPLEMENTED_YET(); - } - - void bvsls_opt_solver::display(std::ostream & out) const - { - NOT_IMPLEMENTED_YET(); - } -} \ No newline at end of file diff --git a/src/opt/bvsls_opt_solver.h b/src/opt/bvsls_opt_solver.h deleted file mode 100644 index eac1d0403..000000000 --- a/src/opt/bvsls_opt_solver.h +++ /dev/null @@ -1,57 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - bvsls_opt_solver.h - -Abstract: - - Uses the bvsls engine for optimization - -Author: - - Christoph (cwinter) 2014-3-28 - -Notes: - ---*/ -#ifndef _BVSLS_OPT_SOLVER_H_ -#define _BVSLS_OPT_SOLVER_H_ - -#include "bvsls_opt_engine.h" -#include "opt_solver.h" - -namespace opt { - - class bvsls_opt_solver : public opt_solver { - ast_manager & m_manager; - params_ref const & m_params; - bvsls_opt_engine m_engine; - - public: - bvsls_opt_solver(ast_manager & m, params_ref const & p); - virtual ~bvsls_opt_solver(); - - virtual void updt_params(params_ref & p); - virtual void collect_param_descrs(param_descrs & r); - virtual void collect_statistics(statistics & st) const; - virtual void assert_expr(expr * t); - virtual void push_core(); - virtual void pop_core(unsigned n); - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); - virtual void get_unsat_core(ptr_vector & r); - virtual void get_model(model_ref & m); - virtual proof * get_proof(); - virtual std::string reason_unknown() const; - virtual void get_labels(svector & r); - virtual void set_cancel(bool f); - virtual void set_progress_callback(progress_callback * callback); - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; - virtual void display(std::ostream & out) const; - }; - -} - -#endif \ No newline at end of file diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp index 053f4dc5a..0663f9abc 100644 --- a/src/opt/core_maxsat.cpp +++ b/src/opt/core_maxsat.cpp @@ -19,11 +19,13 @@ Notes: #include "core_maxsat.h" #include "pb_decl_plugin.h" #include "ast_pp.h" +#include "opt_context.h" namespace opt { - core_maxsat::core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints): - m(m), s(s), m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) { + core_maxsat::core_maxsat(context& c, expr_ref_vector& soft_constraints): + m(c.get_manager()), s(c.get_solver()), + m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) { m_answer.resize(m_soft.size(), false); } diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h index f5a1a9bb3..bbb173a3f 100644 --- a/src/opt/core_maxsat.h +++ b/src/opt/core_maxsat.h @@ -34,7 +34,7 @@ namespace opt { unsigned m_lower; model_ref m_model; public: - core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints); + core_maxsat(context& c, expr_ref_vector& soft_constraints); virtual ~core_maxsat(); virtual lbool operator()(); virtual rational get_lower() const; diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 75b8f86d0..b410a102e 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -23,9 +23,9 @@ Notes: #include "goal.h" #include "probe.h" #include "tactic.h" -#include "smt_context.h" #include "ast_pp.h" #include "model_smt2_pp.h" +#include "opt_context.h" /** \brief Fu & Malik procedure for MaxSAT. This procedure is based on @@ -44,9 +44,9 @@ Notes: namespace opt { struct fu_malik::imp { - ast_manager& m; - opt_solver & m_opt_solver; - ref m_s; + ast_manager& m; + solver& m_s; + filter_model_converter& m_fm; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; @@ -55,10 +55,10 @@ namespace opt { unsigned m_lower; model_ref m_model; - imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft): - m(m), - m_opt_solver(s), - m_s(&s), + imp(context& c, expr_ref_vector const& soft): + m(c.get_manager()), + m_s(c.get_solver()), + m_fm(c.fm()), m_soft(soft), m_orig_soft(soft), m_aux(m), @@ -69,7 +69,7 @@ namespace opt { m_assignment.resize(m_soft.size(), false); } - solver& s() { return *m_s; } + solver& s() { return m_s; } /** \brief One step of the Fu&Malik algorithm. @@ -96,10 +96,8 @@ namespace opt { } } + void collect_statistics(statistics& st) const { - if (m_s != &m_opt_solver) { - m_s->collect_statistics(st); - } st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper); } @@ -145,8 +143,8 @@ namespace opt { app_ref block_var(m), tmp(m); block_var = m.mk_fresh_const("block_var", m.mk_bool_sort()); m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); - m_opt_solver.mc().insert(block_var->get_decl()); - m_opt_solver.mc().insert(to_app(m_aux[i].get())->get_decl()); + m_fm.insert(block_var->get_decl()); + m_fm.insert(to_app(m_aux[i].get())->get_decl()); m_soft[i] = m.mk_or(m_soft[i].get(), block_var); block_vars.push_back(block_var); tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); @@ -181,17 +179,6 @@ namespace opt { } } - void set_solver() { - if (m_opt_solver.dump_benchmarks()) - return; - - solver& current_solver = s(); - goal g(m, true, false); - unsigned num_assertions = current_solver.get_num_assertions(); - for (unsigned i = 0; i < num_assertions; ++i) { - g.assert_expr(current_solver.get_assertion(i)); - } - } // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef lbool operator()() { @@ -199,7 +186,6 @@ namespace opt { if (m_soft.empty()) { return is_sat; } - set_solver(); solver::scoped_push _sp(s()); expr_ref tmp(m); @@ -211,7 +197,7 @@ namespace opt { for (unsigned i = 0; i < m_soft.size(); ++i) { m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); - m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl()); + m_fm.insert(to_app(m_aux.back())->get_decl()); tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); s().assert_expr(tmp); } @@ -247,8 +233,8 @@ namespace opt { }; - fu_malik::fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints) { - m_imp = alloc(imp, m, s, soft_constraints); + fu_malik::fu_malik(context& c, expr_ref_vector& soft_constraints) { + m_imp = alloc(imp, c, soft_constraints); } fu_malik::~fu_malik() { dealloc(m_imp); @@ -281,49 +267,3 @@ namespace opt { } }; -#if 0 - void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) { - if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { - core.reset(); - return; - } - - SASSERT(!literals.empty()); - if (literals.size() == 1) { - core.reset(); - core.insert(literals[0].get()); - return; - } - - unsigned mid = literals.size()/2; - expr_ref_vector ls1(m), ls2(m); - ls1.append(mid, literals.c_ptr()); - ls2.append(literals.size()-mid, literals.c_ptr() + mid); -#if Z3DEBUG - expr_ref_vector ls(m); - ls.append(ls1); - ls.append(ls2); - SASSERT(ls.size() == literals.size()); - for (unsigned i = 0; i < literals.size(); ++i) { - SASSERT(ls[i].get() == literals[i].get()); - } -#endif - expr_ref_vector as1(m); - as1.append(assumptions); - as1.append(ls1); - expr_set core2; - quick_explain(as1, ls2, !ls1.empty(), core2); - - expr_ref_vector as2(m), cs2(m); - as2.append(assumptions); - set2vector(core2, cs2); - as2.append(cs2); - expr_set core1; - quick_explain(as2, ls1, !core2.empty(), core1); - - set_union(core1, core2, core); - } - -#endif - - diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h index e9c994faf..8eb363cb6 100644 --- a/src/opt/fu_malik.h +++ b/src/opt/fu_malik.h @@ -33,7 +33,7 @@ namespace opt { struct imp; imp* m_imp; public: - fu_malik(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints); + fu_malik(context& c, expr_ref_vector& soft_constraints); virtual ~fu_malik(); virtual lbool operator()(); virtual rational get_lower() const; diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 73638f44c..89f9e79fd 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -40,18 +40,19 @@ class inc_sat_solver : public solver { expr_ref_vector m_fmls; expr_ref_vector m_current_fmls; unsigned_vector m_fmls_lim; - expr_ref_vector m_core; - atom2bool_var m_map; - model_ref m_model; + expr_ref_vector m_core; + atom2bool_var m_map; + model_ref m_model; model_converter_ref m_mc; - tactic_ref m_preprocess; - unsigned m_num_scopes; + tactic_ref m_preprocess; + unsigned m_num_scopes; sat::literal_vector m_asms; goal_ref_buffer m_subgoals; proof_converter_ref m_pc; model_converter_ref m_mc2; expr_dependency_ref m_dep_core; - + expr_ref_vector m_soft; + vector m_weights; typedef obj_map dep2asm_t; public: @@ -59,7 +60,8 @@ public: m(m), m_solver(p,0), m_params(p), m_fmls(m), m_current_fmls(m), m_core(m), m_map(m), m_num_scopes(0), - m_dep_core(m) { + m_dep_core(m), + m_soft(m) { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); params_ref simp2_p = p; @@ -78,29 +80,32 @@ public: mk_max_bv_sharing_tactic(m), mk_bit_blaster_tactic(m), mk_aig_tactic(), - using_params(mk_simplify_tactic(m), simp2_p)); - - + using_params(mk_simplify_tactic(m), simp2_p)); } virtual ~inc_sat_solver() {} - virtual void set_progress_callback(progress_callback * callback) { - } + virtual void set_progress_callback(progress_callback * callback) {} + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { m_solver.pop_to_base_level(); dep2asm_t dep2asm; - m_model = 0; lbool r = internalize_formulas(); if (r != l_true) return r; r = internalize_assumptions(num_assumptions, assumptions, dep2asm); if (r != l_true) return r; extract_assumptions(dep2asm, m_asms); + + r = initialize_soft_constraints(); + if (r != l_true) return r; + r = m_solver.check(m_asms.size(), m_asms.c_ptr()); switch (r) { case l_true: - check_assumptions(dep2asm); + if (num_assumptions > 0) { + check_assumptions(dep2asm); + } break; case l_false: // TBD: expr_dependency core is not accounted for. @@ -160,8 +165,7 @@ public: m_params = p; m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); - } - + } virtual void collect_statistics(statistics & st) const { m_preprocess->collect_statistics(st); m_solver.collect_statistics(st); @@ -186,18 +190,57 @@ public: virtual void get_labels(svector & r) { UNREACHABLE(); } - virtual unsigned get_num_assertions() const { return m_fmls.size(); } - virtual expr * get_assertion(unsigned idx) const { return m_fmls[idx]; } - + void set_soft(unsigned sz, expr*const* soft, rational const* weights) { + m_soft.reset(); + m_weights.reset(); + m_soft.append(sz, soft); + m_weights.append(sz, weights); + } private: + lbool initialize_soft_constraints() { + dep2asm_t dep2asm; + if (m_soft.empty()) { + return l_true; + } + expr_ref_vector soft(m_soft); + for (unsigned i = 0; i < soft.size(); ++i) { + expr* e = soft[i].get(), *e1; + if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) { + continue; + } + expr_ref asum(m), fml(m); + asum = m.mk_fresh_const("soft", m.mk_bool_sort()); + fml = m.mk_iff(asum, e); + m_fmls.push_back(fml); + soft[i] = asum; + } + m_soft.reset(); + lbool r = internalize_formulas(); + if (r != l_true) return r; + r = internalize_assumptions(soft.size(), soft.c_ptr(), dep2asm); + sat::literal_vector lits; + svector weights; + + if (r == l_true) { + for (unsigned i = 0; i < soft.size(); ++i) { + weights.push_back(m_weights[i].get_double()); + lits.push_back(dep2asm.find(soft[i].get())); + } + m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr()); + m_params.set_bool("optimize_model", true); + m_solver.updt_params(m_params); + } + return r; + } + lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) { m_mc2.reset(); m_pc.reset(); @@ -295,10 +338,8 @@ private: dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); for (; it != end; ++it) { sat::literal lit = it->m_value; - lbool polarity = lit.sign()?l_false:l_true; - lbool value = sat::value_at(lit.var(), ll_m); - if (value != polarity) { - IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " evaluates to " << value << "\n"; + if (sat::value_at(lit, ll_m) != l_true) { + IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " does not evaluate to true\n"; verbose_stream() << m_asms << "\n"; m_solver.display_assignment(verbose_stream()); m_solver.display(verbose_stream());); @@ -343,6 +384,12 @@ private: } }; + solver* mk_inc_sat_solver(ast_manager& m, params_ref& p) { return alloc(inc_sat_solver, m, p); } + +void set_soft_inc_sat(solver* _s, unsigned sz, expr*const* soft, rational const* weights) { + inc_sat_solver* s = dynamic_cast(_s); + s->set_soft(sz, soft, weights); +} diff --git a/src/opt/inc_sat_solver.h b/src/opt/inc_sat_solver.h index 903d27ebc..8bb4c288a 100644 --- a/src/opt/inc_sat_solver.h +++ b/src/opt/inc_sat_solver.h @@ -24,4 +24,6 @@ Notes: solver* mk_inc_sat_solver(ast_manager& m, params_ref& p); +void set_soft_inc_sat(solver* s, unsigned sz, expr*const* soft, rational const* weights); + #endif diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp index 35ca630d9..76645ee7e 100644 --- a/src/opt/maxhs.cpp +++ b/src/opt/maxhs.cpp @@ -23,6 +23,7 @@ Notes: #include "model_smt2_pp.h" #include "uint_set.h" #include "maxhs.h" +#include "opt_context.h" namespace opt { @@ -74,8 +75,8 @@ namespace opt { public: - maxhs(opt_solver* s, ast_manager& m, params_ref& p, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), + maxhs(context& c, vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(c, ws, soft), m_aux(m), m_at_lower_bound(false) { } @@ -528,7 +529,7 @@ namespace opt { app_ref mk_fresh(sort* s) { app_ref r(m); r = m.mk_fresh_const("r", s); - m_mc->insert(r->get_decl()); + m_c.fm().insert(r->get_decl()); return r; } @@ -553,9 +554,9 @@ namespace opt { }; - maxsmt_solver_base* opt::mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* opt::mk_maxhs(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(maxhs, s, m, p, ws, soft); + return alloc(maxhs, c, ws, soft); } } diff --git a/src/opt/maxhs.h b/src/opt/maxhs.h index e08a550bd..6bb7a2696 100644 --- a/src/opt/maxhs.h +++ b/src/opt/maxhs.h @@ -23,7 +23,7 @@ Notes: #include "maxsmt.h" namespace opt { - maxsmt_solver_base* mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* mk_maxhs(context& c, vector const& ws, expr_ref_vector const& soft); } #endif diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index f879ff99a..a4ccf567f 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -60,6 +60,7 @@ Notes: #include "mus.h" #include "mss.h" #include "inc_sat_solver.h" +#include "opt_context.h" using namespace opt; @@ -83,10 +84,10 @@ private: rational m_max_upper; public: - maxres(ast_manager& m, opt_solver* s, params_ref& p, + maxres(context& c, vector const& ws, expr_ref_vector const& soft, strategy_t st): - maxsmt_solver_base(s, m, p, ws, soft), + maxsmt_solver_base(c, ws, soft), m_B(m), m_asms(m), m_mus(m_s, m), m_mss(m_s, m), @@ -133,10 +134,9 @@ public: } lbool mus_solver() { - solver::scoped_push _sc(*m_s.get()); + solver::scoped_push _sc(m_s); init(); init_local(); - enable_bvsat(); while (true) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); @@ -159,7 +159,6 @@ public: }); for (unsigned i = 0; i < m_soft.size(); ++i) { VERIFY(m_model->eval(m_soft[i].get(), tmp)); - std::cout << mk_pp(m_soft[i].get(), m) << " -> " << tmp << "\n"; m_assignment[i] = m.is_true(tmp); } m_upper = m_lower; @@ -179,11 +178,10 @@ public: } lbool mus_mss_solver() { - solver::scoped_push _sc(*m_s.get()); + solver::scoped_push _sc(s()); init(); init_local(); - enable_bvsat(); - enable_sls(); + enable_sls(m_asms); ptr_vector mcs; vector > cores; while (m_lower < m_upper) { @@ -222,11 +220,32 @@ public: return l_true; } - - lbool mss_solver() { NOT_IMPLEMENTED_YET(); - return l_undef; + solver::scoped_push _sc(s()); + init(); + init_local(); + ptr_vector mcs; + while (m_lower < m_upper) { + lbool is_sat = s().check_sat(0, 0); + // is_sat = get_mcs(mcs); + switch (is_sat) { + case l_undef: + return l_undef; + case l_false: + m_lower = m_upper; + break; + case l_true: + // + is_sat = process_sat(mcs); + if (is_sat != l_true) { + return is_sat; + } + break; + } + } + m_lower = m_upper; + return l_true; } lbool operator()() { @@ -322,7 +341,7 @@ public: } lbool minimize_core(ptr_vector& core) { - if (m_sat_enabled) { + if (m_c.sat_enabled()) { return l_true; } m_mus.reset(); @@ -592,9 +611,9 @@ public: void verify_assignment() { IF_VERBOSE(0, verbose_stream() << "verify assignment\n";); - ref sat_solver = mk_inc_sat_solver(m, m_params); - for (unsigned i = 0; i < m_assertions.size(); ++i) { - sat_solver->assert_expr(m_assertions[i].get()); + ref sat_solver = mk_inc_sat_solver(m, m_params); + for (unsigned i = 0; i < s().get_num_assertions(); ++i) { + sat_solver->assert_expr(s().get_assertion(i)); } expr_ref n(m); for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -612,18 +631,18 @@ public: }; -opt::maxsmt_solver_base* opt::mk_maxres(ast_manager& m, opt_solver* s, params_ref& p, +opt::maxsmt_solver_base* opt::mk_maxres(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(maxres, m, s, p, ws, soft, maxres::s_mus); + return alloc(maxres, c, ws, soft, maxres::s_mus); } -opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(ast_manager& m, opt_solver* s, params_ref& p, +opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(maxres, m, s, p, ws, soft, maxres::s_mus_mss); + return alloc(maxres, c, ws, soft, maxres::s_mus_mss); } -opt::maxsmt_solver_base* opt::mk_mss_maxres(ast_manager& m, opt_solver* s, params_ref& p, +opt::maxsmt_solver_base* opt::mk_mss_maxres(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(maxres, m, s, p, ws, soft, maxres::s_mss); + return alloc(maxres, c, ws, soft, maxres::s_mss); } diff --git a/src/opt/maxres.h b/src/opt/maxres.h index efa8886f7..5f4ea8db3 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -23,15 +23,15 @@ Notes: namespace opt { maxsmt_solver_base* mk_maxres( - ast_manager& m, opt_solver* s, params_ref& p, + context& c, vector const& ws, expr_ref_vector const& soft); maxsmt_solver_base* mk_mus_mss_maxres( - ast_manager& m, opt_solver* s, params_ref& p, + context& c, vector const& ws, expr_ref_vector const& soft); maxsmt_solver_base* mk_mss_maxres( - ast_manager& m, opt_solver* s, params_ref& p, + context& c, vector const& ws, expr_ref_vector const& soft); }; diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp index c64e0f3fc..be8e99c3a 100644 --- a/src/opt/maxsls.cpp +++ b/src/opt/maxsls.cpp @@ -26,16 +26,14 @@ namespace opt { class sls : public maxsmt_solver_base { public: - sls(opt_solver* s, ast_manager& m, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft) { + sls(context& c, vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(c, ws, soft) { } virtual ~sls() {} lbool operator()() { IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";); - enable_bvsat(); - enable_sls(); init(); + enable_sls(m_soft); lbool is_sat = s().check_sat(0, 0); if (is_sat == l_true) { s().get_model(m_model); @@ -54,9 +52,9 @@ namespace opt { }; - maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* opt::mk_sls(context& c, vector const& ws, expr_ref_vector const& soft) { - return alloc(sls, s, m, p, ws, soft); + return alloc(sls, c, ws, soft); } diff --git a/src/opt/maxsls.h b/src/opt/maxsls.h index 111d6a3b2..0ba94d6e8 100644 --- a/src/opt/maxsls.h +++ b/src/opt/maxsls.h @@ -27,7 +27,7 @@ Notes: namespace opt { - maxsmt_solver_base* mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* mk_sls(context& c, vector const& ws, expr_ref_vector const& soft); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 572c6e66c..d7cbbc910 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -24,12 +24,10 @@ Notes: #include "maxres.h" #include "maxhs.h" #include "bcd2.h" -#include "wpm2.h" #include "pbmax.h" #include "wmax.h" #include "maxsls.h" #include "ast_pp.h" -#include "opt_params.hpp" #include "pb_decl_plugin.h" #include "pb_sls.h" #include "tactical.h" @@ -38,19 +36,27 @@ Notes: #include "qfbv_tactic.h" #include "card2bv_tactic.h" #include "uint_set.h" -#include "opt_sls_solver.h" #include "pb_preprocess_tactic.h" -#include "inc_sat_solver.h" +#include "opt_context.h" namespace opt { + maxsmt_solver_base::maxsmt_solver_base( + context& c, vector const& ws, expr_ref_vector const& soft): + m_s(c.get_solver()), + m(c.get_manager()), + m_c(c), + m_cancel(false), m_soft(m), + m_assertions(m) { + m_s.get_model(m_model); + SASSERT(m_model); + updt_params(c.params()); + init_soft(ws, soft); + } + void maxsmt_solver_base::updt_params(params_ref& p) { m_params.copy(p); - s().updt_params(p); - opt_params _p(p); - m_enable_sat = _p.enable_sat(); - m_enable_sls = _p.enable_sls(); } void maxsmt_solver_base::init_soft(vector const& weights, expr_ref_vector const& soft) { @@ -90,132 +96,68 @@ namespace opt { } } - struct maxsmt_solver_base::is_bv { - struct found {}; - ast_manager& m; - pb_util pb; - bv_util bv; - is_bv(ast_manager& m): m(m), pb(m), bv(m) {} - void operator()(var *) { throw found(); } - void operator()(quantifier *) { throw found(); } - void operator()(app *n) { - family_id fid = n->get_family_id(); - if (fid != m.get_basic_family_id() && - fid != pb.get_family_id() && - fid != bv.get_family_id() && - !is_uninterp_const(n)) { - throw found(); - } - } - }; - - bool maxsmt_solver_base::probe_bv() { - expr_fast_mark1 visited; - is_bv proc(m); - try { - unsigned sz = s().get_num_assertions(); - for (unsigned i = 0; i < sz; i++) { - quick_for_each_expr(proc, visited, s().get_assertion(i)); - } - sz = m_soft.size(); - for (unsigned i = 0; i < sz; ++i) { - quick_for_each_expr(proc, visited, m_soft[i].get()); - } - } - catch (is_bv::found) { - return false; - } - return true; - } - - void maxsmt_solver_base::enable_inc_bvsat() { - m_params.set_bool("minimize_core", true); - solver* sat_solver = mk_inc_sat_solver(m, m_params); - unsigned sz = s().get_num_assertions(); - for (unsigned i = 0; i < sz; ++i) { - sat_solver->assert_expr(s().get_assertion(i)); - m_assertions.push_back(s().get_assertion(i)); - } - m_s = sat_solver; - } - - void maxsmt_solver_base::enable_bvsat() { - if (m_enable_sat && !m_sat_enabled && probe_bv()) { - enable_inc_bvsat(); - m_sat_enabled = true; - } - } - - void maxsmt_solver_base::enable_sls() { - if (m_enable_sls && !m_sls_enabled && probe_bv()) { - m_params.set_uint("restarts", 20); - unsigned lvl = m_s->get_scope_level(); - sls_solver* sls = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params); - m_s = sls; - while (lvl > 0) { m_s->push(); --lvl; } - m_sls_enabled = true; - sls->opt(m_model); - } - } - void maxsmt_solver_base::set_mus(bool f) { params_ref p; p.set_bool("minimize_core", f); - m_s->updt_params(p); + m_s.updt_params(p); + } + + void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft) { + m_c.enable_sls(soft, m_weights); } app* maxsmt_solver_base::mk_fresh_bool(char const* name) { app* result = m.mk_fresh_const(name, m.mk_bool_sort()); - m_mc->insert(result->get_decl()); + m_c.fm().insert(result->get_decl()); return result; } + maxsmt::maxsmt(context& c): + m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false), + m_soft_constraints(m), m_answer(m) {} - lbool maxsmt::operator()(opt_solver* s) { + lbool maxsmt::operator()(solver* s) { lbool is_sat; m_msolver = 0; - m_s = s; + symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt", tout << "maxsmt\n";); if (m_soft_constraints.empty()) { TRACE("opt", tout << "no constraints\n";); m_msolver = 0; - is_sat = m_s->check_sat(0, 0); + is_sat = m_s.check_sat(0, 0); } - else if (m_maxsat_engine == symbol("maxres")) { - m_msolver = mk_maxres(m, s, m_params, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("maxres")) { + m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("mus-mss-maxres")) { - m_msolver = mk_mus_mss_maxres(m, s, m_params, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("mus-mss-maxres")) { + m_msolver = mk_mus_mss_maxres(m_c, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("pbmax")) { - m_msolver = mk_pbmax(m, s, m_params, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("pbmax")) { + m_msolver = mk_pbmax(m_c, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("wpm2")) { - m_msolver = mk_wpm2(m, s, m_params, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("bcd2")) { + m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("bcd2")) { - m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("maxhs")) { + m_msolver = mk_maxhs(m_c, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("maxhs")) { - m_msolver = mk_maxhs(m, s, m_params, m_weights, m_soft_constraints); - } - else if (m_maxsat_engine == symbol("sls")) { + else if (maxsat_engine == symbol("sls")) { // NB: this is experimental one-round version of SLS - m_msolver = mk_sls(m, s, m_params, m_weights, m_soft_constraints); + m_msolver = mk_sls(m_c, m_weights, m_soft_constraints); } - else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("core_maxsat")) { - m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints); + else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("core_maxsat")) { + m_msolver = alloc(core_maxsat, m_c, m_soft_constraints); } - else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("fu_malik")) { - m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); + else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) { + m_msolver = alloc(fu_malik, m_c, m_soft_constraints); } else { - if (m_maxsat_engine != symbol::null && m_maxsat_engine != symbol("wmax")) { + if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) { warning_msg("solver %s is not recognized, using default 'wmax'", - m_maxsat_engine.str().c_str()); + maxsat_engine.str().c_str()); } - m_msolver = mk_wmax(m, m_s.get(), m_params, m_weights, m_soft_constraints); + m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); } if (m_msolver) { @@ -242,13 +184,12 @@ namespace opt { } void maxsmt::verify_assignment() { - m_s->push(); + solver::scoped_push _sp(m_s); commit_assignment(); - if (l_true != m_s->check_sat(0,0)) { + if (l_true != m_s.check_sat(0,0)) { IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";); UNREACHABLE(); } - m_s->pop(1); } bool maxsmt::get_assignment(unsigned idx) const { @@ -292,7 +233,6 @@ namespace opt { } void maxsmt::commit_assignment() { - SASSERT(m_s); for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { expr_ref tmp(m); tmp = m_soft_constraints[i].get(); @@ -300,7 +240,7 @@ namespace opt { tmp = m.mk_not(tmp); } TRACE("opt", tout << "committing: " << tmp << "\n";); - m_s->assert_expr(tmp); + m_s.assert_expr(tmp); } } @@ -337,9 +277,7 @@ namespace opt { } void maxsmt::updt_params(params_ref& p) { - opt_params _p(p); - m_maxsat_engine = _p.maxsat_engine(); - m_params = p; + m_params.append(p); if (m_msolver) { m_msolver->updt_params(p); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index a36269447..0110132f2 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -19,11 +19,16 @@ Notes: #ifndef _OPT_MAXSMT_H_ #define _OPT_MAXSMT_H_ -#include "opt_solver.h" -#include "statistics.h" +#include"ast.h" +#include"params.h" +#include"solver.h" +#include"filter_model_converter.h" +#include"statistics.h" namespace opt { + class context; + class maxsmt_solver { public: virtual ~maxsmt_solver() {} @@ -44,8 +49,9 @@ namespace opt { // class maxsmt_solver_base : public maxsmt_solver { protected: - ref m_s; + solver& m_s; ast_manager& m; + context& m_c; volatile bool m_cancel; expr_ref_vector m_soft; expr_ref_vector m_assertions; @@ -53,55 +59,30 @@ namespace opt { rational m_lower; rational m_upper; model_ref m_model; - ref m_mc; // model converter to remove fresh variables svector m_assignment; // truth assignment to soft constraints params_ref m_params; // config - bool m_enable_sls; // config - bool m_enable_sat; // config - bool m_sls_enabled; - bool m_sat_enabled; - struct is_bv; public: - maxsmt_solver_base(opt_solver* s, ast_manager& m, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - m_s(s), m(m), m_cancel(false), m_soft(m), - m_assertions(m), - m_enable_sls(false), m_enable_sat(false), - m_sls_enabled(false), m_sat_enabled(false) { - m_s->get_model(m_model); - SASSERT(m_model); - updt_params(p); - set_converter(s->mc_ref().get()); - init_soft(ws, soft); - } + maxsmt_solver_base(context& c, vector const& ws, expr_ref_vector const& soft); virtual ~maxsmt_solver_base() {} virtual rational get_lower() const { return m_lower; } virtual rational get_upper() const { return m_upper; } virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } - virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } - virtual void collect_statistics(statistics& st) const { - if (m_sls_enabled || m_sat_enabled) { - m_s->collect_statistics(st); - } - } + virtual void set_cancel(bool f) { m_cancel = f; s().set_cancel(f); } + virtual void collect_statistics(statistics& st) const { } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } void set_model() { s().get_model(m_model); } virtual void updt_params(params_ref& p); virtual void init_soft(vector const& weights, expr_ref_vector const& soft); void add_hard(expr* e){ s().assert_expr(e); } - solver& s() { return *m_s; } - void set_converter(filter_model_converter* mc) { m_mc = mc; } + solver& s() { return m_s; } void init(); expr* mk_not(expr* e); - bool probe_bv(); void set_mus(bool f); - void enable_bvsat(); - void enable_sls(); app* mk_fresh_bool(char const* name); - private: - void enable_inc_bvsat(); + protected: + void enable_sls(expr_ref_vector const& soft); }; /** @@ -110,32 +91,27 @@ namespace opt { */ class maxsmt { - ast_manager& m; - ref m_s; + ast_manager& m; + solver& m_s; + context& m_c; + scoped_ptr m_msolver; volatile bool m_cancel; expr_ref_vector m_soft_constraints; expr_ref_vector m_answer; vector m_weights; rational m_lower; rational m_upper; - scoped_ptr m_msolver; - symbol m_maxsat_engine; model_ref m_model; params_ref m_params; public: - maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {} - - lbool operator()(opt_solver* s); - + maxsmt(context& c); + lbool operator()(solver* s); void set_cancel(bool f); - void updt_params(params_ref& p); - void add(expr* f, rational const& w); unsigned size() const { return m_soft_constraints.size(); } expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; } rational weight(unsigned idx) const { return m_weights[idx]; } - void commit_assignment(); rational get_value() const; rational get_lower() const; @@ -146,13 +122,9 @@ namespace opt { bool get_assignment(unsigned index) const; void display_answer(std::ostream& out) const; void collect_statistics(statistics& st) const; - private: - bool is_maxsat_problem(vector const& ws) const; - void verify_assignment(); - }; }; diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index d796a2b92..63a7a72bf 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -26,21 +26,21 @@ Notes: namespace opt { - mss::mss(ref& s, ast_manager& m): m_s(s), m(m), m_cancel(false) { + mss::mss(solver& s, ast_manager& m): m_s(s), m(m), m_cancel(false) { } mss::~mss() { } bool mss::check_result() { - lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); + lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr()); if (is_sat == l_undef) return true; SASSERT(is_sat == l_true); if (is_sat == l_false) return false; expr_set::iterator it = m_mcs.begin(), end = m_mcs.end(); for (; it != end; ++it) { m_mss.push_back(*it); - is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); + is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr()); m_mss.pop_back(); if (is_sat == l_undef) return true; SASSERT(is_sat == l_false); @@ -147,7 +147,7 @@ namespace opt { lbool mss::operator()(vector const& _cores, exprs& literals, exprs& mcs) { m_mss.reset(); m_todo.reset(); - m_s->get_model(m_model); + m_s.get_model(m_model); SASSERT(m_model); vector cores(_cores); TRACE("opt", @@ -207,12 +207,12 @@ namespace opt { TRACE("opt", display_vec(tout << "process (total " << core.size() << ") :", sz, core.c_ptr());); unsigned sz_save = m_mss.size(); m_mss.append(sz, core.c_ptr()); - lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); - IF_VERBOSE(1, display_vec(verbose_stream(), sz, core.c_ptr());); + lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr()); + IF_VERBOSE(2, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr());); m_mss.resize(sz_save); switch (is_sat) { case l_true: - m_s->get_model(m_model); + m_s.get_model(m_model); update_mss(); DEBUG_CODE( for (unsigned i = 0; i < sz; ++i) { diff --git a/src/opt/mss.h b/src/opt/mss.h index 9f14f66c3..cf69c14f9 100644 --- a/src/opt/mss.h +++ b/src/opt/mss.h @@ -21,7 +21,7 @@ Notes: namespace opt { class mss { - ref& m_s; + solver& m_s; ast_manager& m; volatile bool m_cancel; typedef ptr_vector exprs; @@ -32,7 +32,7 @@ namespace opt { exprs m_todo; model_ref m_model; public: - mss(ref& s, ast_manager& m); + mss(solver& s, ast_manager& m); ~mss(); lbool operator()(vector const& cores, exprs& literals, exprs& mcs); diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index a8126e699..545aba2cc 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -29,13 +29,13 @@ using namespace opt; // struct mus::imp { - ref& m_s; - ast_manager& m; - expr_ref_vector m_cls2expr; - obj_map m_expr2cls; - volatile bool m_cancel; + solver& m_s; + ast_manager& m; + expr_ref_vector m_cls2expr; + obj_map m_expr2cls; + volatile bool m_cancel; - imp(ref& s, ast_manager& m): + imp(solver& s, ast_manager& m): m_s(s), m(m), m_cls2expr(m), m_cancel(false) {} @@ -92,7 +92,7 @@ struct mus::imp { unsigned sz = assumptions.size(); assumptions.push_back(not_cls); add_core(core, assumptions); - lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); + lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr()); assumptions.resize(sz); switch (is_sat) { case l_undef: @@ -103,7 +103,7 @@ struct mus::imp { break; default: core_exprs.reset(); - m_s->get_unsat_core(core_exprs); + m_s.get_unsat_core(core_exprs); if (!core_exprs.contains(not_cls)) { // core := core_exprs \ mus core.reset(); @@ -124,7 +124,7 @@ struct mus::imp { for (unsigned i = 0; i < mus.size(); ++i) { assumptions.push_back(m_cls2expr[mus[i]].get()); } - lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); + lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr()); SASSERT(is_sat == l_false); ); #endif @@ -147,7 +147,7 @@ struct mus::imp { }; -mus::mus(ref& s, ast_manager& m) { +mus::mus(solver& s, ast_manager& m) { m_imp = alloc(imp, s, m); } diff --git a/src/opt/mus.h b/src/opt/mus.h index 3a96b4842..94eb42cc6 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -24,7 +24,7 @@ namespace opt { struct imp; imp * m_imp; public: - mus(ref& s, ast_manager& m); + mus(solver& s, ast_manager& m); ~mus(); /** Add soft constraint. diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 58c5c2017..d2de3ae80 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -34,8 +34,10 @@ Notes: #include "tactical.h" #include "model_smt2_pp.h" #include "card2bv_tactic.h" -#include "bvsls_opt_solver.h" #include "nnf_tactic.h" +#include "inc_sat_solver.h" +#include "bv_decl_plugin.h" +#include "pb_decl_plugin.h" namespace opt { @@ -114,13 +116,18 @@ namespace opt { m_arith(m), m_bv(m), m_hard_constraints(m), + m_solver(0), m_optsmt(m), m_scoped_state(m), - m_objective_refs(m) + m_fm(m), + m_objective_refs(m), + m_enable_sat(false), + m_enable_sls(false) { - m_params.set_bool("model", true); - m_params.set_bool("unsat_core", true); - m_solver = alloc(opt_solver, m, m_params, symbol()); + params_ref p; + p.set_bool("model", true); + p.set_bool("unsat_core", true); + updt_params(p); } context::~context() { @@ -172,9 +179,7 @@ namespace opt { objective& obj = s.m_objectives[i]; m_objectives.push_back(obj); if (obj.m_type == O_MAXSMT) { - maxsmt* ms = alloc(maxsmt, m); - ms->updt_params(m_params); - m_maxsmts.insert(obj.m_id, ms); + add_maxsmt(obj.m_id); } } m_hard_constraints.append(s.m_hard); @@ -184,18 +189,19 @@ namespace opt { if (m_pareto) { return execute_pareto(); } - import_scoped_state(); + init_solver(); + import_scoped_state(); normalize(); internalize(); - opt_solver& s = get_solver(); - solver::scoped_push _sp(s); + update_solver(); + solver& s = get_solver(); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;); s.assert_expr(m_hard_constraints[i].get()); } IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); - lbool is_sat = s.check_sat_core(0,0); + lbool is_sat = s.check_sat(0,0); TRACE("opt", tout << "initial search result: " << is_sat << "\n";); if (is_sat != l_true) { m_model = 0; @@ -203,7 +209,7 @@ namespace opt { } IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";); s.get_model(m_model); - m_optsmt.setup(s); + m_optsmt.setup(*m_opt_solver.get()); update_lower(true); switch (m_objectives.size()) { case 0: @@ -214,7 +220,6 @@ namespace opt { opt_params optp(m_params); symbol pri = optp.priority(); if (pri == symbol("pareto")) { - _sp.disable_pop(); return execute_pareto(); } else if (pri == symbol("box")) { @@ -233,7 +238,7 @@ namespace opt { if (m_model_converter) { (*m_model_converter)(mdl, 0); } - get_solver().mc()(mdl, 0); + m_fm(mdl, 0); } } @@ -243,7 +248,7 @@ namespace opt { if (result == l_true) m_optsmt.get_model(m_model); return result; } - + lbool context::execute_maxsat(symbol const& id, bool committed) { model_ref tmp; maxsmt& ms = *m_maxsmts.find(id); @@ -265,7 +270,10 @@ namespace opt { lbool context::execute_lex() { lbool r = l_true; for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { + bool is_last = i + 1 == m_objectives.size(); + if (!is_last) get_solver().push(); r = execute(m_objectives[i], i + 1 < m_objectives.size()); + if (!is_last) get_solver().pop(1); if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } @@ -282,9 +290,8 @@ namespace opt { for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; if (obj.m_type == O_MAXSMT) { - get_solver().push(); + solver::scoped_push _sp(get_solver()); r = execute(obj, false); - get_solver().pop(1); } } return r; @@ -381,12 +388,13 @@ namespace opt { } lbool context::execute_pareto() { + if (!m_pareto) { - m_pareto = alloc(gia_pareto, m, *this, m_solver.get(), m_params); + set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params)); } lbool is_sat = (*(m_pareto.get()))(); if (is_sat != l_true) { - m_pareto = 0; + set_pareto(0); } if (is_sat == l_true) { yield(); @@ -395,7 +403,6 @@ namespace opt { m_solver->pop(1); } return is_sat; - // NB. fix race condition for set_cancel } void context::display_bounds(std::ostream& out, bounds_t const& b) const { @@ -411,10 +418,98 @@ namespace opt { } } - opt_solver& context::get_solver() { + solver& context::get_solver() { return *m_solver.get(); } + void context::init_solver() { + #pragma omp critical (opt_context) + { + m_opt_solver = alloc(opt_solver, m, m_params, m_fm, symbol()); + m_solver = m_opt_solver.get(); + } + } + + void context::update_solver() { + if (!m_enable_sat || !probe_bv()) { + return; + } + if (m_maxsat_engine != symbol("maxres") && + m_maxsat_engine != symbol("mus-mss-maxres") && + m_maxsat_engine != symbol("bcd2") && + m_maxsat_engine != symbol("sls")) { + return; + } + m_params.set_bool("minimize_core", true); + m_sat_solver = mk_inc_sat_solver(m, m_params); + unsigned sz = get_solver().get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + m_sat_solver->assert_expr(get_solver().get_assertion(i)); + } + #pragma omp critical (opt_context) + { + m_solver = m_sat_solver.get(); + } + } + + void context::enable_sls(expr_ref_vector const& soft, vector const& weights) { + SASSERT(soft.size() == weights.size()); + if (m_enable_sls && m_sat_solver.get()) { + set_soft_inc_sat(m_sat_solver.get(), soft.size(), soft.c_ptr(), weights.c_ptr()); + } + } + + struct context::is_bv { + struct found {}; + ast_manager& m; + pb_util pb; + bv_util bv; + is_bv(ast_manager& m): m(m), pb(m), bv(m) {} + void operator()(var *) { throw found(); } + void operator()(quantifier *) { throw found(); } + void operator()(app *n) { + family_id fid = n->get_family_id(); + if (fid != m.get_basic_family_id() && + fid != pb.get_family_id() && + fid != bv.get_family_id() && + !is_uninterp_const(n)) { + throw found(); + } + } + }; + + bool context::probe_bv() { + expr_fast_mark1 visited; + is_bv proc(m); + try { + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective & obj = m_objectives[i]; + if (obj.m_type != O_MAXSMT) return false; + maxsmt& ms = *m_maxsmts.find(obj.m_id); + for (unsigned j = 0; j < ms.size(); ++j) { + quick_for_each_expr(proc, visited, ms[j]); + } + } + unsigned sz = get_solver().get_num_assertions(); + for (unsigned i = 0; i < sz; i++) { + quick_for_each_expr(proc, visited, get_solver().get_assertion(i)); + } + } + catch (is_bv::found) { + return false; + } + return true; + } + + void context::add_maxsmt(symbol const& id) { + maxsmt* ms = alloc(maxsmt, *this); + ms->updt_params(m_params); + #pragma omp critical (opt_context) + { + m_maxsmts.insert(id, ms); + } + } + bool context::is_numeral(expr* e, rational & n) const { unsigned sz; return m_arith.is_numeral(e, n) || m_bv.is_numeral(e, n, sz); @@ -440,28 +535,16 @@ namespace opt { mk_simplify_tactic(m)); opt_params optp(m_params); tactic_ref tac2, tac3; - if (optp.engine() == "bvsls") { + if (optp.elim_01()) { tac2 = mk_elim01_tactic(m); tac3 = mk_lia2card_tactic(m); params_ref lia_p; lia_p.set_bool("compile_equality", optp.pb_compile_equality()); tac3->updt_params(lia_p); - m_simplify = and_then(tac0.get(), tac2.get(), tac3.get(), - mk_card2bv_tactic(m), - mk_simplify_tactic(m), - mk_nnf_tactic(m)); - m_solver = alloc(bvsls_opt_solver, m, m_params); - } - else if (optp.elim_01()) { - tac2 = mk_elim01_tactic(m); - tac3 = mk_lia2card_tactic(m); - params_ref lia_p; - lia_p.set_bool("compile_equality", optp.pb_compile_equality()); - tac3->updt_params(lia_p); - m_simplify = and_then(tac0.get(), tac2.get(), tac3.get()); + set_simplify(and_then(tac0.get(), tac2.get(), tac3.get())); } else { - m_simplify = tac0.get(); + set_simplify(tac0.get()); } proof_converter_ref pc; expr_dependency_ref core(m); @@ -657,9 +740,7 @@ namespace opt { obj.m_type = O_MAXSMT; obj.m_weights.append(weights); SASSERT(!m_maxsmts.contains(id)); - maxsmt* ms = alloc(maxsmt, m); - ms->updt_params(m_params); - m_maxsmts.insert(id, ms); + add_maxsmt(id); } SASSERT(obj.m_id == id); obj.m_terms.reset(); @@ -899,22 +980,39 @@ namespace opt { default: return expr_ref(m_arith.mk_add(args.size(), args.c_ptr()), m); } } - + + void context::set_simplify(tactic* tac) { + #pragma omp critical (opt_context) + { + m_simplify = tac; + } + } + + void context::set_pareto(pareto_base* p) { + #pragma omp critical (opt_context) + { + m_pareto = p; + } + } + void context::set_cancel(bool f) { - if (m_solver) { - m_solver->set_cancel(f); - } - if (m_simplify) { - m_simplify->set_cancel(f); - } - if (m_pareto) { - m_pareto->set_cancel(f); + #pragma omp critical (opt_context) + { + if (m_solver) { + m_solver->set_cancel(f); + } + if (m_pareto) { + m_pareto->set_cancel(f); + } + if (m_simplify) { + m_simplify->set_cancel(f); + } + map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); + for (; it != end; ++it) { + it->m_value->set_cancel(f); + } } m_optsmt.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) const { @@ -944,6 +1042,10 @@ namespace opt { for (; it != end; ++it) { it->m_value->updt_params(m_params); } + opt_params _p(p); + m_enable_sat = _p.enable_sat(); + m_enable_sls = _p.enable_sls(); + m_maxsat_engine = _p.maxsat_engine(); } typedef obj_hashtable func_decl_set; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 1f7eb55af..33af6c912 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -108,7 +108,9 @@ namespace opt { arith_util m_arith; bv_util m_bv; expr_ref_vector m_hard_constraints; - ref m_solver; + ref m_opt_solver; + ref m_solver; + ref m_sat_solver; scoped_ptr m_pareto; params_ref m_params; optsmt m_optsmt; @@ -116,11 +118,15 @@ namespace opt { scoped_state m_scoped_state; vector m_objectives; model_ref m_model; - model_converter_ref m_model_converter; + model_converter_ref m_model_converter; + filter_model_converter m_fm; obj_map m_objective_fns; obj_map m_objective_orig; func_decl_ref_vector m_objective_refs; tactic_ref m_simplify; + bool m_enable_sat; + bool m_enable_sls; + symbol m_maxsat_engine; public: context(ast_manager& m); virtual ~context(); @@ -163,6 +169,15 @@ namespace opt { virtual expr_ref mk_ge(unsigned i, model_ref& model); virtual expr_ref mk_le(unsigned i, model_ref& model); + smt::context& smt_context() { return m_opt_solver->get_context(); } + filter_model_converter& fm() { return m_fm; } + bool sat_enabled() const { return 0 != m_sat_solver.get(); } + solver& get_solver(); + ast_manager& get_manager() { return this->m; } + params_ref& params() { return m_params; } + void enable_sls(expr_ref_vector const& soft, vector const& weights); + symbol const& maxsat_engine() const { return m_maxsat_engine; } + private: void validate_feasibility(maxsmt& ms); @@ -199,7 +214,14 @@ namespace opt { inf_eps get_upper_as_num(unsigned idx); - opt_solver& get_solver(); + struct is_bv; + bool probe_bv(); + + void init_solver(); + void update_solver(); + void add_maxsmt(symbol const& id); + void set_simplify(tactic *simplify); + void set_pareto(pareto_base* p); bool is_numeral(expr* e, rational& n) const; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 21667e5f8..186a63105 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -35,13 +35,14 @@ Notes: namespace opt { - opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, symbol const & l): + opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, + filter_model_converter& fm, symbol const & l): solver_na2as(mgr), m_params(p), m_context(mgr, m_params), m(mgr), m_dump_benchmarks(false), - m_fm(alloc(filter_model_converter, m)) { + m_fm(fm) { m_logic = l; if (m_logic != symbol::null) { m_context.set_logic(m_logic); @@ -233,20 +234,20 @@ namespace opt { if (typeid(smt::theory_inf_arith) == typeid(opt)) { smt::theory_inf_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(mc(), v, val), m); + return expr_ref(th.mk_ge(m_fm, v, val), m); } if (typeid(smt::theory_mi_arith) == typeid(opt)) { smt::theory_mi_arith& th = dynamic_cast(opt); SASSERT(val.is_finite()); - return expr_ref(th.mk_ge(mc(), v, val.get_numeral()), m); + return expr_ref(th.mk_ge(m_fm, v, val.get_numeral()), m); } if (typeid(smt::theory_i_arith) == typeid(opt)) { SASSERT(val.is_finite()); SASSERT(val.get_infinitesimal().is_zero()); smt::theory_i_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(mc(), v, val.get_rational()), m); + return expr_ref(th.mk_ge(m_fm, v, val.get_rational()), m); } // difference logic? diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 5ac794ab4..128e12798 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -42,6 +42,7 @@ namespace opt { smt_params m_params; smt::kernel m_context; ast_manager& m; + filter_model_converter& m_fm; progress_callback * m_callback; symbol m_logic; bool m_objective_enabled; @@ -50,9 +51,8 @@ namespace opt { bool m_dump_benchmarks; static unsigned m_dump_count; statistics m_stats; - ref m_fm; public: - opt_solver(ast_manager & m, params_ref const & p, symbol const & l); + opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm, symbol const & l); virtual ~opt_solver(); virtual void updt_params(params_ref & p); @@ -82,9 +82,6 @@ namespace opt { inf_eps const & get_objective_value(unsigned obj_index); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); - filter_model_converter& mc() { return *(m_fm.get()); } - ref& mc_ref() { return m_fm; } - static opt_solver& to_opt(solver& s); bool dump_benchmarks(); diff --git a/src/opt/pbmax.cpp b/src/opt/pbmax.cpp index fe1d7b70d..a2191686e 100644 --- a/src/opt/pbmax.cpp +++ b/src/opt/pbmax.cpp @@ -31,16 +31,14 @@ namespace opt { class pbmax : public maxsmt_solver_base { public: - pbmax(opt_solver* s, ast_manager& m, params_ref& p, + pbmax(context& c, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft) { + maxsmt_solver_base(c, ws, soft) { } virtual ~pbmax() {} lbool operator()() { - enable_bvsat(); - enable_sls(); TRACE("opt", s().display(tout); tout << "\n"; for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -90,9 +88,9 @@ namespace opt { } }; - maxsmt_solver_base* opt::mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* opt::mk_pbmax(context & c, vector const& ws, expr_ref_vector const& soft) { - return alloc(pbmax, s, m, p, ws, soft); + return alloc(pbmax, c, ws, soft); } } diff --git a/src/opt/pbmax.h b/src/opt/pbmax.h index 8dcb43715..50a989abd 100644 --- a/src/opt/pbmax.h +++ b/src/opt/pbmax.h @@ -23,7 +23,7 @@ Notes: #include "maxsmt.h" namespace opt { - maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* mk_pbmax(context& c, vector const& ws, expr_ref_vector const& soft); } diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 8c76b06ba..84a1a4e52 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -23,15 +23,15 @@ Notes: #include "smt_theory.h" #include "smt_context.h" #include "theory_wmaxsat.h" - +#include "opt_context.h" namespace opt { class maxsmt_solver_wbase : public maxsmt_solver_base { smt::context& ctx; public: - maxsmt_solver_wbase(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + maxsmt_solver_wbase(context& c, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), ctx(ctx) {} + maxsmt_solver_base(c, ws, soft), ctx(c.smt_context()) {} ~maxsmt_solver_wbase() {} class scoped_ensure_theory { @@ -52,7 +52,7 @@ namespace opt { wth->reset(); } else { - wth = alloc(smt::theory_wmaxsat, m, m_mc); + wth = alloc(smt::theory_wmaxsat, m, m_c.fm()); ctx.register_plugin(wth); } return wth; @@ -76,9 +76,9 @@ namespace opt { class wmax : public maxsmt_solver_wbase { public: - wmax(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + wmax(context& c, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_wbase(s, m, ctx, p, ws, soft) {} + maxsmt_solver_wbase(c, ws, soft) {} virtual ~wmax() {} lbool operator()() { @@ -122,9 +122,9 @@ namespace opt { } }; - maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(wmax, s, m, s->get_context(), p, ws, soft); + maxsmt_solver_base* opt::mk_wmax(context& c, + vector const& ws, expr_ref_vector const& soft) { + return alloc(wmax, c, ws, soft); } } diff --git a/src/opt/wmax.h b/src/opt/wmax.h index bc33eee4a..77be62f92 100644 --- a/src/opt/wmax.h +++ b/src/opt/wmax.h @@ -23,7 +23,7 @@ Notes: #include "maxsmt.h" namespace opt { - maxsmt_solver_base* mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, + maxsmt_solver_base* mk_wmax(context& c, vector const& ws, expr_ref_vector const& soft); } diff --git a/src/opt/wpm2.cpp b/src/opt/wpm2.cpp deleted file mode 100644 index 63418861a..000000000 --- a/src/opt/wpm2.cpp +++ /dev/null @@ -1,251 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - wpm2.cpp - -Abstract: - - wpn2 based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ -#include "wpm2.h" -#include "pbmax.h" -#include "pb_decl_plugin.h" -#include "uint_set.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" - - -namespace opt { - - // ------------------------------------------------------ - // AAAI 2010 - class wpm2 : public maxsmt_solver_base { - scoped_ptr maxs; - public: - wpm2(opt_solver* s, ast_manager& m, maxsmt_solver_base* _maxs, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), maxs(_maxs) { - } - - virtual ~wpm2() {} - - lbool operator()() { - enable_sls(); - IF_VERBOSE(1, verbose_stream() << "(opt.wpm2)\n";); - solver::scoped_push _s(s()); - pb_util u(m); - app_ref fml(m), a(m), b(m), c(m); - expr_ref val(m); - expr_ref_vector block(m), ans(m), al(m), am(m); - obj_map ans_index; - vector amk; - vector sc; - init(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - rational w = m_weights[i]; - - b = mk_fresh_bool("b"); - block.push_back(b); - expr* bb = b; - - a = mk_fresh_bool("a"); - ans.push_back(a); - ans_index.insert(a, i); - fml = m.mk_or(m_soft[i].get(), b, m.mk_not(a)); - s().assert_expr(fml); - - c = mk_fresh_bool("c"); - fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0))); - s().assert_expr(fml); - - sc.push_back(uint_set()); - sc.back().insert(i); - am.push_back(c); - amk.push_back(rational(0)); - } - - while (true) { - expr_ref_vector asms(m); - ptr_vector core; - asms.append(ans); - asms.append(am); - lbool is_sat = s().check_sat(asms.size(), asms.c_ptr()); - TRACE("opt", - tout << "\nassumptions: "; - for (unsigned i = 0; i < asms.size(); ++i) { - tout << mk_pp(asms[i].get(), m) << " "; - } - tout << "\n" << is_sat << "\n"; - tout << "upper: " << m_upper << "\n"; - tout << "lower: " << m_lower << "\n"; - if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - model_smt2_pp(tout, m, *(mdl.get()), 0); - }); - - if (m_cancel && is_sat != l_false) { - is_sat = l_undef; - } - if (is_sat == l_true) { - m_upper = m_lower; - s().get_model(m_model); - for (unsigned i = 0; i < block.size(); ++i) { - VERIFY(m_model->eval(m_soft[i].get(), val)); - TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";); - m_assignment[i] = m.is_true(val); - } - } - if (is_sat != l_false) { - return is_sat; - } - s().get_unsat_core(core); - if (core.empty()) { - return l_false; - } - TRACE("opt", - tout << "core: "; - for (unsigned i = 0; i < core.size(); ++i) { - tout << mk_pp(core[i],m) << " "; - } - tout << "\n";); - uint_set A; - for (unsigned i = 0; i < core.size(); ++i) { - unsigned j; - if (ans_index.find(core[i], j)) { - A.insert(j); - } - } - if (A.empty()) { - return l_false; - } - uint_set B; - rational k(0); - rational old_lower(m_lower); - for (unsigned i = 0; i < sc.size(); ++i) { - uint_set t(sc[i]); - t &= A; - if (!t.empty()) { - B |= sc[i]; - k += amk[i]; - m_lower -= amk[i]; - sc[i] = sc.back(); - sc.pop_back(); - am[i] = am.back(); - am.pop_back(); - amk[i] = amk.back(); - amk.pop_back(); - --i; - } - } - vector ws; - expr_ref_vector bs(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (B.contains(i)) { - ws.push_back(m_weights[i]); - bs.push_back(block[i].get()); - } - } - TRACE("opt", tout << "at most bound: " << k << "\n";); - is_sat = new_bound(al, ws, bs, k); - if (is_sat != l_true) { - return is_sat; - } - m_lower += k; - SASSERT(m_lower > old_lower); - TRACE("opt", tout << "new bound: " << m_lower << "\n";); - expr_ref B_le_k(m), B_ge_k(m); - B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k); - B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k); - s().assert_expr(B_ge_k); - al.push_back(B_ge_k); - IF_VERBOSE(1, verbose_stream() << "(opt.wpm2 [" << m_lower << ":" << m_upper << "])\n";); - IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";); - - c = mk_fresh_bool("c"); - fml = m.mk_implies(c, B_le_k); - s().assert_expr(fml); - sc.push_back(B); - am.push_back(c); - amk.push_back(k); - } - } - - virtual void set_cancel(bool f) { - maxsmt_solver_base::set_cancel(f); - maxs->set_cancel(f); - } - - virtual void collect_statistics(statistics& st) const { - maxsmt_solver_base::collect_statistics(st); - maxs->collect_statistics(st); - } - - private: - lbool new_bound(expr_ref_vector const& al, - vector const& ws, - expr_ref_vector const& bs, - rational& k) { - pb_util u(m); - expr_ref_vector al2(m); - al2.append(al); - // w_j*b_j > k - al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k))); - return bound(al2, ws, bs, k); - } - - // - // minimal k, such that al & w_j*b_j >= k is sat - // minimal k, such that al & 3*x + 4*y >= k is sat - // minimal k, such that al & (or (not x) w3) & (or (not y) w4) - // - lbool bound(expr_ref_vector const& al, - vector const& ws, - expr_ref_vector const& bs, - rational& k) { - expr_ref_vector nbs(m); - opt_solver::scoped_push _sc(maxs->s()); - for (unsigned i = 0; i < al.size(); ++i) { - maxs->add_hard(al[i]); - } - for (unsigned i = 0; i < bs.size(); ++i) { - nbs.push_back(mk_not(bs[i])); - } - TRACE("opt", - maxs->s().display(tout); - tout << "\n"; - for (unsigned i = 0; i < bs.size(); ++i) { - tout << mk_pp(bs[i], m) << " " << ws[i] << "\n"; - }); - maxs->init_soft(ws, nbs); - lbool is_sat = maxs->s().check_sat(0,0); - if (is_sat == l_true) { - maxs->set_model(); - is_sat = (*maxs)(); - } - SASSERT(maxs->get_lower() > k); - k = maxs->get_lower(); - return is_sat; - } - }; - - maxsmt_solver_base* opt::mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - - ref s0 = alloc(opt_solver, m, p, symbol()); - // initialize model. - s0->check_sat(0,0); - maxsmt_solver_base* s2 = mk_pbmax(m, s0.get(), p, ws, soft); - return alloc(wpm2, s, m, s2, p, ws, soft); - } - -} diff --git a/src/opt/wpm2.h b/src/opt/wpm2.h deleted file mode 100644 index efaddc602..000000000 --- a/src/opt/wpm2.h +++ /dev/null @@ -1,29 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - wpm2.h - -Abstract: - - Wpm2 based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ - -#ifndef _WPM2_H_ -#define _WPM2_H_ - -#include "maxsmt.h" - -namespace opt { - maxsmt_solver_base* mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); -} -#endif diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 94ac37de5..f142100ad 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -105,6 +105,7 @@ namespace sat { } m_minimize_lemmas = p.minimize_lemmas(); m_minimize_core = p.minimize_core(); + m_optimize_model = p.optimize_model(); m_dyn_sub_res = p.dyn_sub_res(); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 47804793d..df11629ab 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -69,6 +69,7 @@ namespace sat { bool m_minimize_lemmas; bool m_dyn_sub_res; bool m_minimize_core; + bool m_optimize_model; symbol m_always_true; diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index db1e90b39..11d0fc15d 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -41,6 +41,7 @@ namespace sat { lbool mus::operator()() { flet _disable_min(s.m_config.m_minimize_core, false); + flet _disable_opt(s.m_config.m_optimize_model, false); TRACE("sat", tout << "old core: " << s.get_core() << "\n";); IF_VERBOSE(2, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); reset(); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index fd35e5d64..fb4a7fe6d 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -19,4 +19,5 @@ def_module_params('sat', ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('minimize_core', BOOL, False, 'minimize computed core'), + ('optimize_model', BOOL, False, 'enable optimization of soft constraints'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index 78d9b66e5..fdb9bd5e2 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -50,8 +50,8 @@ namespace sat { return m_elems[rnd(num_elems())]; } - sls::sls(solver& s): s(s) { - m_max_tries = 10000; + sls::sls(solver& s): s(s), m_cancel(false) { + m_max_tries = 1000000; m_prob_choose_min_var = 43; m_clause_generation = 0; } @@ -180,6 +180,7 @@ namespace sat { m_use_list[c[j].index()].push_back(i); } } + DEBUG_CODE(check_use_list();); } unsigned_vector const& sls::get_use(literal lit) { @@ -242,7 +243,7 @@ namespace sat { } void sls::flip(literal lit) { - // IF_VERBOSE(0, verbose_stream() << lit << " ";); + //IF_VERBOSE(0, verbose_stream() << lit << " ";); SASSERT(value_at(lit, m_model) == l_false); SASSERT(!m_tabu[lit.var()]); m_model[lit.var()] = lit.sign()?l_false:l_true; @@ -266,9 +267,70 @@ namespace sat { } void sls::check_invariant() { - + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause const& c = *m_clauses[i]; + bool is_sat = c.satisfied_by(m_model); + SASSERT(is_sat != m_false.contains(i)); + SASSERT(is_sat == m_num_true[i] > 0); + } } + void sls::check_use_list() { + + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause const& c = *m_clauses[i]; + for (unsigned j = 0; j < c.size(); ++j) { + unsigned idx = c[j].index(); + SASSERT(m_use_list[idx].contains(i)); + } + } + + for (unsigned i = 0; i < m_use_list.size(); ++i) { + literal lit = to_literal(i); + for (unsigned j = 0; j < m_use_list[i].size(); ++j) { + clause const& c = *m_clauses[m_use_list[i][j]]; + bool found = false; + for (unsigned k = 0; !found && k < c.size(); ++k) { + found = c[k] == lit; + } + SASSERT(found); + } + } + } + + void sls::display(std::ostream& out) const { + out << "Model\n"; + for (bool_var v = 0; v < m_model.size(); ++v) { + out << v << ": " << m_model[v] << "\n"; + } + out << "Clauses\n"; + unsigned sz = m_false.num_elems(); + for (unsigned i = 0; i < sz; ++i) { + out << *m_clauses[m_false[i]] << "\n"; + } + for (unsigned i = 0; i < m_clauses.size(); ++i) { + if (m_false.contains(i)) continue; + clause const& c = *m_clauses[i]; + out << c << " " << m_num_true[i] << "\n"; + } + bool has_tabu = false; + for (unsigned i = 0; !has_tabu && i < m_tabu.size(); ++i) { + has_tabu = m_tabu[i]; + } + if (has_tabu) { + out << "Tabu: "; + for (unsigned i = 0; i < m_tabu.size(); ++i) { + if (m_tabu[i]) { + literal lit(i, false); + if (value_at(lit, m_model) == l_false) lit.neg(); + out << lit << " "; + } + } + out << "\n"; + } + } + + wsls::wsls(solver& s): sls(s) { @@ -277,7 +339,7 @@ namespace sat { wsls::~wsls() {} - void wsls::set_soft(unsigned sz, double const* weights, literal const* lits) { + void wsls::set_soft(unsigned sz, literal const* lits, double const* weights) { m_soft.reset(); m_weights.reset(); m_soft.append(sz, lits); @@ -291,14 +353,17 @@ namespace sat { // Initialize m_clause_weights, m_hscore, m_sscore. // m_best_value = m_false.empty()?evaluate_model():-1.0; + m_best_model.reset(); m_clause_weights.reset(); m_hscore.reset(); m_sscore.reset(); m_H.reset(); m_S.reset(); + m_best_model.append(s.get_model()); m_clause_weights.resize(m_clauses.size(), 1); m_sscore.resize(s.num_vars(), 0.0); m_hscore.resize(s.num_vars(), 0); + unsigned num_violated = 0; for (unsigned i = 0; i < m_soft.size(); ++i) { literal lit = m_soft[i]; m_sscore[lit.var()] = m_weights[i]; @@ -310,16 +375,19 @@ namespace sat { m_hscore[i] = compute_hscore(i); refresh_scores(i); } + DEBUG_CODE(check_invariant();); unsigned i = 0; - for (; !m_cancel && i < m_max_tries; ++i) { + for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) { wflip(); } - IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";); + TRACE("sat", display(tout);); + IF_VERBOSE(0, verbose_stream() << "tries " << i << "\n";); } void wsls::wflip() { literal lit; if (pick_wflip(lit)) { + // IF_VERBOSE(0, verbose_stream() << lit << " ";); wflip(lit); } } @@ -328,8 +396,10 @@ namespace sat { if (m_false.empty()) { double val = evaluate_model(); if (val < m_best_value || m_best_value < 0.0) { + m_best_value = val; m_best_model.reset(); m_best_model.append(m_model); + IF_VERBOSE(0, verbose_stream() << "new value:" << val << "\n";); } } unsigned idx; @@ -337,6 +407,8 @@ namespace sat { idx = m_H.choose(m_rand); lit = literal(idx, false); if (value_at(lit, m_model) == l_true) lit.neg(); + SASSERT(value_at(lit, m_model) == l_false); + TRACE("sat", tout << "flip H(" << m_H.num_elems() << ") " << lit << "\n";); } else if (!m_S.empty()) { double score = 0.0; @@ -353,16 +425,38 @@ namespace sat { m_min_vars.push_back(literal(v, false)); } } - idx = m_min_vars[m_rand(m_min_vars.size())].var(); // pick with largest sscore. + lit = m_min_vars[m_rand(m_min_vars.size())]; // pick with largest sscore. + SASSERT(value_at(lit, m_model) == l_false); + TRACE("sat", tout << "flip S(" << m_min_vars.size() << "," << score << ") " << lit << "\n";); } else { update_hard_weights(); if (!m_false.empty()) { unsigned cls_idx = m_false.choose(m_rand); + clause const& c = *m_clauses[cls_idx]; + lit = c[m_rand(c.size())]; + TRACE("sat", tout << "flip hard(" << m_false.num_elems() << "," << c.size() << ") " << lit << "\n";); } else { - lit = m_soft[m_rand(m_soft.size())]; + m_min_vars.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + lit = m_soft[i]; + if (value_at(lit, m_model) == l_false) { + m_min_vars.push_back(lit); + } + } + if (m_min_vars.empty()) { + SASSERT(m_best_value == 0.0); + UNREACHABLE(); // we should have exited the main loop before. + return false; + } + else { + lit = m_min_vars[m_rand(m_min_vars.size())]; + } + TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ") " << lit << "\n";); + } + SASSERT(value_at(lit, m_model) == l_false); } return !m_tabu[lit.var()]; } @@ -408,7 +502,6 @@ namespace sat { } } } - DEBUG_CODE(check_invariant();); } @@ -488,9 +581,29 @@ namespace sat { // The score(v) is the reward on soft clauses for flipping v. for (unsigned j = 0; j < m_soft.size(); ++j) { unsigned v = m_soft[j].var(); - double ss = value_at(m_soft[j], m_model)?(-m_weights[j]):m_weights[j]; + double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j]; SASSERT(m_sscore[v] == ss); } + + // m_H are values such that m_hscore >= 0. + for (bool_var v = 0; v < m_hscore.size(); ++v) { + SASSERT(m_hscore[v] > 0 == m_H.contains(v)); + } + + // m_S are values such that hscore = 0, sscore > 0 + for (bool_var v = 0; v < m_sscore.size(); ++v) { + SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0) == m_S.contains(v)); + } + } + + void wsls::display(std::ostream& out) const { + sls::display(out); + out << "Best model\n"; + for (bool_var v = 0; v < m_best_model.size(); ++v) { + out << v << ": " << m_best_model[v] << " h: " << m_hscore[v]; + if (m_sscore[v] != 0.0) out << " s: " << m_sscore[v]; + out << "\n"; + } } }; diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h index 5546b90ac..57b883994 100644 --- a/src/sat/sat_sls.h +++ b/src/sat/sat_sls.h @@ -60,6 +60,8 @@ namespace sat { virtual ~sls(); lbool operator()(unsigned sz, literal const* tabu, bool reuse_model); void set_cancel(bool f) { m_cancel = f; } + void set_max_tries(unsigned mx) { m_max_tries = mx; } + virtual void display(std::ostream& out) const; protected: void init(unsigned sz, literal const* tabu, bool reuse_model); void init_tabu(unsigned sz, literal const* tabu); @@ -69,6 +71,7 @@ namespace sat { unsigned_vector const& get_use(literal lit); void flip(literal lit); virtual void check_invariant(); + void check_use_list(); private: bool pick_flip(literal& lit); void flip(); @@ -91,9 +94,11 @@ namespace sat { public: wsls(solver& s); virtual ~wsls(); - void set_soft(unsigned sz, double const* weights, literal const* lits); + void set_soft(unsigned sz, literal const* lits, double const* weights); + bool has_soft() const { return !m_soft.empty(); } void opt(unsigned sz, literal const* tabu, bool reuse_model); model const& get_model() { return m_best_model; } + virtual void display(std::ostream& out) const; private: void wflip(); void wflip(literal lit); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c100f15b1..e4e34b8a3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -40,6 +40,7 @@ namespace sat { m_asymm_branch(*this, p), m_probing(*this, p), m_mus(*this), + m_wsls(*this), m_inconsistent(false), m_num_frozen(0), m_activity_inc(128), @@ -528,6 +529,10 @@ namespace sat { return found_undef ? l_undef : l_false; } + void solver::initialize_soft(unsigned sz, literal const* lits, double const* weights) { + m_wsls.set_soft(sz, lits, weights); + } + // ----------------------- // // Propagation @@ -1003,6 +1008,11 @@ namespace sat { m_model[v] = value(v); } TRACE("sat_mc_bug", m_mc.display(tout);); + if (m_config.m_optimize_model) { + m_wsls.opt(0, 0, false); + m_model.reset(); + m_model.append(m_wsls.get_model()); + } m_mc(m_model); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); @@ -2305,6 +2315,7 @@ namespace sat { void solver::set_cancel(bool f) { m_cancel = f; + m_wsls.set_cancel(f); } void solver::collect_statistics(statistics & st) const { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 869330e06..5f45ab424 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -33,6 +33,7 @@ Revision History: #include"sat_iff3_finder.h" #include"sat_probing.h" #include"sat_mus.h" +#include"sat_sls.h" #include"params.h" #include"statistics.h" #include"stopwatch.h" @@ -82,6 +83,7 @@ namespace sat { asymm_branch m_asymm_branch; probing m_probing; mus m_mus; + wsls m_wsls; bool m_inconsistent; // A conflict is usually a single justification. That is, a justification // for false. If m_not_l is not null_literal, then m_conflict is a @@ -224,13 +226,14 @@ namespace sat { void assign_core(literal l, justification jst); void set_conflict(justification c, literal not_l); void set_conflict(justification c) { set_conflict(c, null_literal); } - lbool status(clause const & c) const; + lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } void checkpoint() { if (m_cancel) throw solver_exception(Z3_CANCELED_MSG); if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } typedef std::pair bin_clause; + void initialize_soft(unsigned sz, literal const* lits, double const* weights); protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; } watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 5d9753a82..38a22095a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -36,6 +36,7 @@ Notes: #include"model_v2_pp.h" #include"tactic.h" #include"ast_pp.h" +#include struct goal2sat::imp { struct frame { @@ -78,8 +79,9 @@ struct goal2sat::imp { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } - void throw_op_not_handled() { - throw tactic_exception("operator not supported, apply simplifier before invoking translator"); + void throw_op_not_handled(std::string const& s) { + std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator"; + throw tactic_exception(s0.c_str()); } void mk_clause(sat::literal l) { @@ -183,9 +185,12 @@ struct goal2sat::imp { case OP_AND: case OP_XOR: case OP_IMPLIES: - case OP_DISTINCT: + case OP_DISTINCT: { TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";); - throw_op_not_handled(); + std::ostringstream strm; + strm << mk_ismt2_pp(t, m); + throw_op_not_handled(strm.str()); + } default: convert_atom(t, root, sign); return true; diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 353ff38a3..e6f410442 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -24,7 +24,7 @@ Notes: namespace smt { -theory_wmaxsat::theory_wmaxsat(ast_manager& m, ref& mc): +theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc): theory(m.mk_family_id("weighted_maxsat")), m_mc(mc), m_vars(m), @@ -91,7 +91,7 @@ bool_var theory_wmaxsat::assert_weighted(expr* fml, rational const& w) { ast_manager& m = get_manager(); app_ref var(m), wfml(m); var = m.mk_fresh_const("w", m.mk_bool_sort()); - m_mc->insert(var->get_decl()); + m_mc.insert(var->get_decl()); wfml = m.mk_or(var, fml); ctx.assert_expr(wfml); m_rweights.push_back(w); diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index b6974957c..feac6c04e 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -28,7 +28,7 @@ namespace smt { void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; - ref m_mc; + filter_model_converter& m_mc; mutable unsynch_mpz_manager m_mpz; app_ref_vector m_vars; // Auxiliary variables per soft clause expr_ref_vector m_fmls; // Formulas per soft clause @@ -50,7 +50,7 @@ namespace smt { svector m_assigned; stats m_stats; public: - theory_wmaxsat(ast_manager& m, ref& mc); + theory_wmaxsat(ast_manager& m, filter_model_converter& mc); virtual ~theory_wmaxsat(); void get_assignment(svector& result); virtual void init_search_eh();