From e3cb0e2d8b1cbdedc47fb56fe4a0a3b9e8f7a9b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Aug 2015 12:06:27 -0700 Subject: [PATCH] reworking pd-maxres Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 51 +++++---- src/opt/maxsls.cpp | 3 +- src/opt/maxsmt.cpp | 8 +- src/opt/maxsmt.h | 3 +- src/opt/opt_context.cpp | 14 +-- src/opt/opt_context.h | 6 +- src/sat/sat_config.cpp | 1 - src/sat/sat_config.h | 1 - src/sat/sat_params.pyg | 1 - src/sat/sat_solver.cpp | 108 +++++++++++------- src/sat/sat_solver.h | 10 +- src/sat/sat_solver/inc_sat_solver.cpp | 154 +++++++++++++------------- src/sat/sat_solver/inc_sat_solver.h | 2 +- 13 files changed, 192 insertions(+), 170 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index ddd238156..bf98e80ed 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -206,16 +206,10 @@ public: init_local(); set_soft_assumptions(); lbool is_sat = l_true; - trace_bounds("max_res"); + trace_bounds("maxres"); exprs cs; while (m_lower < m_upper) { -#if 0 - expr_ref_vector asms(m_asms); - sort_assumptions(asms); - is_sat = s().check_sat(asms.size(), asms.c_ptr()); -#else is_sat = check_sat_hill_climb(m_asms); -#endif if (m_cancel) { return l_undef; } @@ -268,33 +262,45 @@ public: first = false; IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";); m_last_index = index; - is_sat = s().check_sat(index, asms.c_ptr()); + is_sat = check_sat(index, asms.c_ptr()); } } else { - is_sat = s().check_sat(asms.size(), asms.c_ptr()); + is_sat = check_sat(asms.size(), asms.c_ptr()); } return is_sat; } + lbool check_sat(unsigned sz, expr* const* asms) { + if (m_st == s_primal_dual && m_c.sat_enabled()) { + rational max_weight = m_upper; + vector weights; + for (unsigned i = 0; i < sz; ++i) { + weights.push_back(get_weight(asms[i])); + } + return inc_sat_check_sat(s(), sz, asms, weights.c_ptr(), max_weight); + } + else { + return s().check_sat(sz, asms); + } + } + void found_optimum() { IF_VERBOSE(1, verbose_stream() << "found optimum\n";); s().get_model(m_model); - DEBUG_CODE( - for (unsigned i = 0; i < m_asms.size(); ++i) { - SASSERT(is_true(m_asms[i].get())); - }); + SASSERT(is_true(m_asms)); rational upper(0); for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); - if (!m_assignment[i]) upper += m_weights[i]; + if (!m_assignment[i]) { + upper += m_weights[i]; + } } SASSERT(upper == m_lower); m_upper = m_lower; m_found_feasible_optimum = true; } - virtual lbool operator()() { m_defs.reset(); switch(m_st) { @@ -496,14 +502,6 @@ public: return m_asm2weight.find(e); } - void sls() { - vector ws; - for (unsigned i = 0; i < m_asms.size(); ++i) { - ws.push_back(get_weight(m_asms[i].get())); - } - enable_sls(m_asms, ws); - } - rational split_core(exprs const& core) { if (core.empty()) return rational(0); // find the minimal weight: @@ -687,6 +685,13 @@ public: return is_true(m_model.get(), e); } + bool is_true(expr_ref_vector const& es) { + for (unsigned i = 0; i < es.size(); ++i) { + if (!is_true(es[i])) return false; + } + return true; + } + void remove_soft(exprs const& core, expr_ref_vector& asms) { for (unsigned i = 0; i < asms.size(); ++i) { if (core.contains(asms[i].get())) { diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp index d5ddb6623..e1cf90fb1 100644 --- a/src/opt/maxsls.cpp +++ b/src/opt/maxsls.cpp @@ -33,8 +33,7 @@ namespace opt { lbool operator()() { IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";); init(); - set_enable_sls(true); - enable_sls(m_soft, m_weights); + enable_sls(true); lbool is_sat = s().check_sat(0, 0); if (is_sat == l_true) { s().get_model(m_model); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 92dac9474..0267b8bb7 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -97,12 +97,8 @@ namespace opt { s().updt_params(p); } - void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft, vector const& ws) { - m_c.enable_sls(soft, ws); - } - - void maxsmt_solver_base::set_enable_sls(bool f) { - m_c.set_enable_sls(f); + void maxsmt_solver_base::enable_sls(bool force) { + m_c.enable_sls(force); } void maxsmt_solver_base::set_soft_assumptions() { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index a15d191e4..ef85b9de8 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -100,8 +100,7 @@ namespace opt { protected: - void enable_sls(expr_ref_vector const& soft, weights_t& ws); - void set_enable_sls(bool f); + void enable_sls(bool force); void set_soft_assumptions(); void trace_bounds(char const* solver); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 86c5447a9..2936ee3c0 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -130,7 +130,6 @@ namespace opt { m_fm(m), m_objective_refs(m), m_enable_sat(false), - m_enable_sls(false), m_is_clausal(false), m_pp_neat(false) { @@ -532,18 +531,11 @@ namespace opt { } void context::set_soft_assumptions() { - if (m_sat_solver.get()) { - m_params.set_bool("soft_assumptions", true); - m_sat_solver->updt_params(m_params); - } + // TBD no-op } - void context::enable_sls(expr_ref_vector const& soft, vector const& weights) { - SASSERT(soft.size() == weights.size()); - if (m_sat_solver.get()) { - set_soft_inc_sat(m_sat_solver.get(), soft.size(), soft.c_ptr(), weights.c_ptr()); - } - if (m_enable_sls && m_sat_solver.get()) { + void context::enable_sls(bool force) { + if ((force || m_enable_sls) && m_sat_solver.get()) { m_params.set_bool("optimize_model", true); m_sat_solver->updt_params(m_params); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 4b14a0115..194c08495 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -50,8 +50,7 @@ namespace opt { virtual solver& get_solver() = 0; // retrieve solver object (SAT or SMT solver) virtual ast_manager& get_manager() = 0; virtual params_ref& params() = 0; - virtual void enable_sls(expr_ref_vector const& soft, weights_t& weights) = 0; // stochastic local search - virtual void set_enable_sls(bool f) = 0; // overwrite whether SLS is enabled. + virtual void enable_sls(bool force) = 0; // stochastic local search virtual void set_soft_assumptions() = 0; // configure SAT solver to skip assumptions assigned by unit-propagation virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter. virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call. @@ -216,8 +215,7 @@ namespace opt { virtual solver& get_solver(); virtual ast_manager& get_manager() { return this->m; } virtual params_ref& params() { return m_params; } - virtual void enable_sls(expr_ref_vector const& soft, weights_t& weights); - virtual void set_enable_sls(bool f) { m_enable_sls = f; } + virtual void enable_sls(bool force); virtual void set_soft_assumptions(); virtual symbol const& maxsat_engine() const { return m_maxsat_engine; } virtual void get_base_model(model_ref& _m); diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 0c100aff2..aff023b22 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -110,7 +110,6 @@ namespace sat { m_minimize_core = p.minimize_core(); m_minimize_core_partial = p.minimize_core_partial(); m_optimize_model = p.optimize_model(); - m_soft_assumptions = p.soft_assumptions(); m_bcd = p.bcd(); m_dyn_sub_res = p.dyn_sub_res(); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 1b336ccb6..2eff402ad 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -72,7 +72,6 @@ namespace sat { bool m_minimize_core; bool m_minimize_core_partial; bool m_optimize_model; - bool m_soft_assumptions; bool m_bcd; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index ed4f4910a..c5ac97b4e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -22,6 +22,5 @@ def_module_params('sat', ('minimize_core', BOOL, False, 'minimize computed core'), ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('optimize_model', BOOL, False, 'enable optimization of soft constraints'), - ('soft_assumptions', BOOL, False, 'disable assumptions that are forced during unit propagation'), ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 40d02ebbb..dc258817b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -534,10 +534,6 @@ 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 @@ -714,7 +710,7 @@ namespace sat { // Search // // ----------------------- - lbool solver::check(unsigned num_lits, literal const* lits) { + lbool solver::check(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); @@ -729,7 +725,7 @@ namespace sat { init_search(); propagate(false); if (inconsistent()) return l_false; - init_assumptions(num_lits, lits); + init_assumptions(num_lits, lits, weights, max_weight); propagate(false); if (check_inconsistent()) return l_false; cleanup(); @@ -892,10 +888,12 @@ namespace sat { } } - void solver::init_assumptions(unsigned num_lits, literal const* lits) { + void solver::init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { if (num_lits == 0 && m_user_scope_literals.empty()) { return; } + + retry_init_assumptions: m_assumptions.reset(); m_assumption_set.reset(); push(); @@ -920,45 +918,75 @@ namespace sat { assign(nlit, justification()); } - for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { - literal lit = lits[i]; - SASSERT(is_external((lit).var())); - m_assumption_set.insert(lit); - - if (m_config.m_soft_assumptions) { - switch(value(lit)) { - case l_undef: - m_assumptions.push_back(lit); - assign(lit, justification()); - break; - case l_false: { - set_conflict(lit); - flet _min1(m_config.m_minimize_core, false); - flet _min2(m_config.m_minimize_core_partial, false); - resolve_conflict_for_unsat_core(); - SASSERT(m_core.size() <= m_assumptions.size()); - if (m_core.size() <= 3 || - m_core.size() <= i - m_assumptions.size() + 1) { - return; - } - else { - m_inconsistent = false; - } - break; - } - case l_true: - break; - } - propagate(false); + if (weights) { + if (m_config.m_optimize_model) { + m_wsls.set_soft(num_lits, lits, weights); } else { - m_assumptions.push_back(lit); - assign(lit, justification()); - // propagate(false); + svector blocker; + if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) { + pop_to_base_level(); + mk_clause(blocker.size(), blocker.c_ptr()); + goto retry_init_assumptions; + } } + return; + } + + for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { + literal lit = lits[i]; + SASSERT(is_external(lit.var())); + m_assumption_set.insert(lit); + m_assumptions.push_back(lit); + assign(lit, justification()); + // propagate(false); } } + bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, + svector& blocker) { + double weight = 0; + blocker.reset(); + for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { + literal lit = lits[i]; + SASSERT(is_external(lit.var())); + m_assumption_set.insert(lit); + + switch(value(lit)) { + case l_undef: + m_assumptions.push_back(lit); + assign(lit, justification()); + break; + case l_false: { + set_conflict(lit); + flet _min1(m_config.m_minimize_core, false); + flet _min2(m_config.m_minimize_core_partial, false); + resolve_conflict_for_unsat_core(); + weight += weights[i]; + blocker.push_back(~lit); + SASSERT(m_core.size() <= m_assumptions.size()); + SASSERT(m_assumptions.size() <= i); + if (m_core.size() <= 3 || m_core.size() < blocker.size()) { + TRACE("opt", tout << "found small core: " << m_core.size() << "\n";); + return true; + } + m_inconsistent = false; + if (weight >= max_weight) { + TRACE("opt", tout << "blocking soft correction set: " << blocker.size() << "\n";); + // block the current correction set candidate. + return false; + } + break; + } + case l_true: + break; + } + propagate(false); + } + return true; + } + + void solver::reinit_assumptions() { if (tracking_assumptions() && scope_lvl() == 0) { TRACE("sat", tout << m_assumptions << "\n";); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f8948e3b6..76a42829d 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -239,7 +239,6 @@ namespace sat { 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()]; } @@ -271,7 +270,11 @@ namespace sat { // // ----------------------- public: - lbool check(unsigned num_lits = 0, literal const* lits = 0); + lbool check(unsigned num_lits = 0, literal const* lits = 0) { + return check(num_lits, lits, 0, 0); + } + lbool check(unsigned num_lits, literal const* lits, double const* weights, double max_weight); + model const & get_model() const { return m_model; } bool model_is_current() const { return m_model_is_current; } literal_vector const& get_core() const { return m_core; } @@ -291,7 +294,8 @@ namespace sat { bool_var next_var(); lbool bounded_search(); void init_search(); - void init_assumptions(unsigned num_lits, literal const* lits); + void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); + bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight, svector& blocker); void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e06267208..aa519971b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -30,6 +30,7 @@ Notes: #include "goal2sat.h" #include "ast_pp.h" #include "model_smt2_pp.h" +#include "filter_model_converter.h" // incremental SAT solver. class inc_sat_solver : public solver { @@ -55,9 +56,6 @@ class inc_sat_solver : public solver { proof_converter_ref m_pc; model_converter_ref m_mc2; expr_dependency_ref m_dep_core; - expr_ref_vector m_soft; - vector m_weights; - bool m_soft_assumptions; typedef obj_map dep2asm_t; @@ -71,9 +69,7 @@ public: m_core(m), m_map(m), m_num_scopes(0), - m_dep_core(m), - m_soft(m), - m_soft_assumptions(false) { + m_dep_core(m) { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); params_ref simp2_p = p; @@ -99,25 +95,25 @@ public: virtual void set_progress_callback(progress_callback * callback) {} - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + return check_sat(num_assumptions, assumptions, 0, 0); + } + + lbool check_sat(unsigned num_assumptions, expr * const * assumptions, double const* weights, double max_weight) { 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(); + r = internalize_assumptions(num_assumptions, assumptions, weights, dep2asm); if (r != l_true) return r; //m_solver.display_dimacs(std::cout); - r = m_solver.check(m_asms.size(), m_asms.c_ptr()); + r = m_solver.check(m_asms.size(), m_asms.c_ptr(), weights, max_weight); switch (r) { case l_true: - if (num_assumptions > 0) { + if (num_assumptions > 0 && !weights) { check_assumptions(dep2asm); } break; @@ -187,7 +183,6 @@ public: m_params = p; m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); - m_soft_assumptions = m_params.get_bool("soft_assumptions", false); m_optimize_model = m_params.get_bool("optimize_model", false); } virtual void collect_statistics(statistics & st) const { @@ -226,58 +221,9 @@ public: virtual expr * get_assumption(unsigned idx) const { return m_asmsf[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); - if (r != l_true) return r; - sat::literal_vector lits; - svector weights; - sat::literal lit; - for (unsigned i = 0; i < soft.size(); ++i) { - weights.push_back(m_weights[i].get_double()); - expr* s = soft[i].get(); - if (!dep2asm.find(s, lit)) { - IF_VERBOSE(0, - verbose_stream() << "not found: " << mk_pp(s, m) << "\n"; - dep2asm_t::iterator it = dep2asm.begin(); - dep2asm_t::iterator end = dep2asm.end(); - for (; it != end; ++it) { - verbose_stream() << mk_pp(it->m_key, m) << " " << it->m_value << "\n"; - } - UNREACHABLE();); - } - lits.push_back(lit); - } - m_solver.initialize_soft(lits.size(), lits.c_ptr(), weights.c_ptr()); - return r; - } lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) { m_mc2.reset(); @@ -305,15 +251,54 @@ private: return l_true; } - lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { + lbool internalize_assumptions(unsigned sz, expr* const* asms, double const* weights, dep2asm_t& dep2asm) { if (sz == 0) { return l_true; } + if (weights) { + return internalize_weighted(sz, asms, weights, dep2asm); + } + return internalize_unweighted(sz, asms, dep2asm); + } + + lbool internalize_unweighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. + lbool res = l_undef; for (unsigned i = 0; i < sz; ++i) { g->assert_expr(asms[i], m.mk_leaf(asms[i])); } - return internalize_goal(g, dep2asm); + res = internalize_goal(g, dep2asm); + if (res == l_true) { + extract_assumptions(dep2asm); + } + return res; + } + + /* + \brief extract weighted assumption literals in the same order as the weights. + For this purpose we enforce tha assumptions are literals. + */ + lbool internalize_weighted(unsigned sz, expr* const* asms, double const* weights, dep2asm_t& dep2asm) { + goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. + lbool res = l_undef; + m_asms.reset(); + expr_ref_vector lits(m); + filter_model_converter_ref fmc = alloc(filter_model_converter, m); + for (unsigned i = 0; i < sz; ++i) { + expr_ref lit = ensure_literal(g, asms[i], fmc.get()); + lits.push_back(lit); + g->assert_expr(lit, m.mk_leaf(lit)); + } + m_mc = concat(m_mc.get(), fmc.get()); + res = internalize_goal(g, dep2asm); + if (res == l_true) { + for (unsigned i = 0; i < lits.size(); ++i) { + sat::literal l; + VERIFY (dep2asm.find(lits[i].get(), l)); + m_asms.push_back(l); + } + } + return res; } lbool internalize_formulas() { @@ -328,11 +313,27 @@ private: return internalize_goal(g, dep2asm); } - void extract_assumptions(dep2asm_t& dep2asm, sat::literal_vector& asms) { - asms.reset(); + expr_ref ensure_literal(goal_ref& g, expr* e, filter_model_converter* fmc) { + expr_ref result(m), fml(m); + expr* e1; + if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) { + result = e; + } + else { + // TBD: need a filter_model_converter to remove + result = m.mk_fresh_const("soft", m.mk_bool_sort()); + fmc->insert(to_app(result)->get_decl()); + fml = m.mk_implies(result, e); + g->assert_expr(fml); + } + return result; + } + + void extract_assumptions(dep2asm_t& dep2asm) { + m_asms.reset(); dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); for (; it != end; ++it) { - asms.push_back(it->m_value); + m_asms.push_back(it->m_value); } //IF_VERBOSE(0, verbose_stream() << asms << "\n";); } @@ -363,8 +364,6 @@ private: VERIFY(asm2dep.find(core[i].index(), e)); m_core.push_back(e); } - - } void check_assumptions(dep2asm_t& dep2asm) { @@ -372,7 +371,7 @@ private: dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); for (; it != end; ++it) { sat::literal lit = it->m_value; - if (!m_soft_assumptions && sat::value_at(lit, ll_m) != l_true) { + 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()); @@ -433,7 +432,12 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& 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); + +lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational const* _weights, rational const& max_weight) { + inc_sat_solver& s = dynamic_cast(_s); + vector weights; + for (unsigned i = 0; _weights && i < sz; ++i) { + weights.push_back(_weights[i].get_double()); + } + return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double()); } diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 58b582617..b13f24552 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -24,6 +24,6 @@ Notes: solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p); -void set_soft_inc_sat(solver* s, unsigned sz, expr*const* soft, rational const* weights); +lbool inc_sat_check_sat(solver& s, unsigned sz, expr*const* soft, rational const* weights, rational const& max_weight); #endif