From 024082a45f11505b5d6992472f8a50a409920606 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Nov 2016 09:52:05 -0800 Subject: [PATCH] adding preferred sat, currently disabled, to wmax. Fixing issue #815 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 4 + src/opt/opt_solver.h | 1 + src/opt/wmax.cpp | 256 ++++++++++++++-- src/smt/smt_consequences.cpp | 200 ++++++++++-- src/smt/smt_context.cpp | 162 +++++----- src/smt/smt_context.h | 27 +- src/smt/smt_context_inv.cpp | 3 + src/smt/smt_kernel.cpp | 9 + src/smt/smt_kernel.h | 7 +- src/smt/theory_wmaxsat.cpp | 577 +++++++++++++++++++---------------- src/smt/theory_wmaxsat.h | 30 +- src/solver/solver.cpp | 4 + src/solver/solver.h | 12 +- 13 files changed, 887 insertions(+), 405 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 0d0283232..868303660 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -198,6 +198,10 @@ namespace opt { return m_context.find_mutexes(vars, mutexes); } + lbool opt_solver::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_context.preferred_sat(asms, cores); + } + /** diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 16c2061c7..094023ba2 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -107,6 +107,7 @@ namespace opt { virtual std::ostream& display(std::ostream & out) const; virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index d8ffe9f66..228e14cd6 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -32,64 +32,286 @@ namespace opt { class wmax : public maxsmt_solver_base { + obj_map m_weights; + obj_map m_keys; + expr_ref_vector m_trail, m_defs; + + void reset() { + m_weights.reset(); + m_keys.reset(); + m_trail.reset(); + m_defs.reset(); + } + public: wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft) {} + maxsmt_solver_base(c, ws, soft), + m_trail(m), + m_defs(m) {} + virtual ~wmax() {} lbool operator()() { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); obj_map soft; + reset(); lbool is_sat = find_mutexes(soft); if (is_sat != l_true) { return is_sat; } - rational offset = m_lower; - m_upper = offset; + m_upper = m_lower; bool was_sat = false; - expr_ref_vector disj(m); + expr_ref_vector disj(m), asms(m); + vector cores; obj_map::iterator it = soft.begin(), end = soft.end(); for (; it != end; ++it) { - expr_ref tmp(m); - bool is_true = m_model->eval(it->m_key, tmp) && m.is_true(tmp); - expr* c = wth().assert_weighted(it->m_key, it->m_value, is_true); - if (!is_true) { + expr* c = assert_weighted(wth(), it->m_key, it->m_value); + if (!is_true(it->m_key)) { + disj.push_back(m.mk_not(c)); m_upper += it->m_value; - disj.push_back(c); } } + wth().init_min_cost(m_upper - m_lower); s().assert_expr(mk_or(disj)); trace_bounds("wmax"); - while (l_true == is_sat && m_lower < m_upper) { + + while (!m.canceled() && m_lower < m_upper) { + //mk_assumptions(asms); + //is_sat = s().preferred_sat(asms, cores); is_sat = s().check_sat(0, 0); if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_false) { + break; + } if (is_sat == l_true) { if (wth().is_optimal()) { - m_upper = offset + wth().get_min_cost(); + m_upper = m_lower + wth().get_cost(); s().get_model(m_model); } expr_ref fml = wth().mk_block(); + //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); was_sat = true; } + else { + //DEBUG_CODE(verify_cores(cores);); + } + update_cores(wth(), cores); + wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); + SASSERT(m_lower <= m_upper); } - if (was_sat) { - wth().get_assignment(m_assignment); - m_upper = offset + wth().get_min_cost(); - } - if (is_sat == l_false && was_sat) { + + update_assignment(); + + if (!m.canceled() && is_sat == l_undef && m_lower == m_upper) { is_sat = l_true; } - if (is_sat == l_true) { + if (is_sat == l_false) { + is_sat = l_true; m_lower = m_upper; } TRACE("opt", tout << "min cost: " << m_upper << "\n";); return is_sat; } + + bool is_true(expr* e) { + expr_ref tmp(m); + return m_model->eval(e, tmp) && m.is_true(tmp); + } + + void update_assignment() { + m_assignment.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment.push_back(is_true(m_soft[i])); + } + } + + struct compare_asm { + wmax& max; + compare_asm(wmax& max):max(max) {} + bool operator()(expr* a, expr* b) const { + return max.m_weights[a] > max.m_weights[b]; + } + }; + + void mk_assumptions(expr_ref_vector& asms) { + ptr_vector _asms; + obj_map::iterator it = m_weights.begin(), end = m_weights.end(); + for (; it != end; ++it) { + _asms.push_back(it->m_key); + } + compare_asm comp(*this); + std::sort(_asms.begin(),_asms.end(), comp); + asms.reset(); + for (unsigned i = 0; i < _asms.size(); ++i) { + asms.push_back(m.mk_not(_asms[i])); + } + } + + void verify_cores(vector const& cores) { + for (unsigned i = 0; i < cores.size(); ++i) { + verify_core(cores[i]); + } + } + + void verify_core(expr_ref_vector const& core) { + s().push(); + s().assert_expr(core); + VERIFY(l_false == s().check_sat(0, 0)); + s().pop(1); + } + + void update_cores(smt::theory_wmaxsat& th, vector const& cores) { + obj_hashtable seen; + bool updated = false; + unsigned min_core_size = UINT_MAX; + for (unsigned i = 0; i < cores.size(); ++i) { + expr_ref_vector const& core = cores[i]; + if (core.size() <= 20) { + s().assert_expr(m.mk_not(mk_and(core))); + } + min_core_size = std::min(core.size(), min_core_size); + if (core.size() >= 11) { + continue; + } + bool found = false; + for (unsigned j = 0; !found && j < core.size(); ++j) { + found = seen.contains(core[j]); + } + if (found) { + continue; + } + for (unsigned j = 0; j < core.size(); ++j) { + seen.insert(core[j]); + } + update_core(th, core); + updated = true; + } + // if no core was selected, then take the smallest cores. + for (unsigned i = 0; !updated && i < cores.size(); ++i) { + expr_ref_vector const& core = cores[i]; + if (core.size() > min_core_size + 2) { + continue; + } + bool found = false; + for (unsigned j = 0; !found && j < core.size(); ++j) { + found = seen.contains(core[j]); + } + if (found) { + continue; + } + for (unsigned j = 0; j < core.size(); ++j) { + seen.insert(core[j]); + } + update_core(th, core); + } + } + + + rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector& keys, vector& weights) { + rational min_weight(-1); + for (unsigned i = 0; i < core.size(); ++i) { + expr* e; + VERIFY(m.is_not(core[i], e)); + keys.push_back(m_keys[e]); + rational weight = m_weights[e]; + if (i == 0 || weight < min_weight) { + min_weight = weight; + } + weights.push_back(weight); + m_weights.erase(e); + m_keys.erase(e); + th.disable_var(e); + } + for (unsigned i = 0; i < core.size(); ++i) { + rational weight = weights[i]; + if (weight > min_weight) { + weight -= min_weight; + assert_weighted(th, keys[i], weight); + } + } + return min_weight; + } + + // assert maxres clauses + // assert new core members with value of current model. + // update lower bound + // bounds get re-normalized when solver is invoked. + // each element of core is negated literal from theory_wmaxsat + // disable those literals from th + + void update_core(smt::theory_wmaxsat& th, expr_ref_vector const& core) { + ptr_vector keys; + vector weights; + rational min_weight = remove_negations(th, core, keys, weights); + max_resolve(th, keys, min_weight); + m_lower += min_weight; + // std::cout << core << " " << min_weight << "\n"; + } + + void max_resolve(smt::theory_wmaxsat& th, ptr_vector const& core, rational const& w) { + SASSERT(!core.empty()); + expr_ref fml(m), asum(m); + app_ref cls(m), d(m), dd(m); + // + // d_0 := true + // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 + // soft (b_i or !d_i) + // == (b_i or !(!b_{i-1} or d_{i-1})) + // == (b_i or b_0 & b_1 & ... & b_{i-1}) + // + // Soft constraint is satisfied if previous soft constraint + // holds or if it is the first soft constraint to fail. + // + // Soundness of this rule can be established using MaxRes + // + for (unsigned i = 1; i < core.size(); ++i) { + expr* b_i = core[i-1]; + expr* b_i1 = core[i]; + if (i == 1) { + d = to_app(b_i); + } + else if (i == 2) { + d = m.mk_and(b_i, d); + m_trail.push_back(d); + } + else { + dd = mk_fresh_bool("d"); + fml = m.mk_implies(dd, d); + s().assert_expr(fml); + m_defs.push_back(fml); + fml = m.mk_implies(dd, b_i); + s().assert_expr(fml); + m_defs.push_back(fml); + fml = m.mk_and(d, b_i); + update_model(dd, fml); + d = dd; + } + cls = m.mk_or(b_i1, d); + m_trail.push_back(cls); + assert_weighted(th, cls, w); + } + } + + expr* assert_weighted(smt::theory_wmaxsat& th, expr* key, rational const& w) { + expr* c = th.assert_weighted(key, w); + m_weights.insert(c, w); + m_keys.insert(c, key); + m_trail.push_back(c); + return c; + } + + void update_model(expr* def, expr* value) { + expr_ref val(m); + if (m_model && m_model->eval(value, val, true)) { + m_model->register_decl(to_app(def)->get_decl(), val); + } + } + }; maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index e6edbf87e..ab1971a3e 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -56,36 +56,7 @@ namespace smt { s.insert(lit.var()); } else { - b_justification js = get_justification(lit.var()); - switch (js.get_kind()) { - case b_justification::CLAUSE: { - clause * cls = js.get_clause(); - if (!cls) break; - unsigned num_lits = cls->get_num_literals(); - for (unsigned j = 0; j < num_lits; ++j) { - literal lit2 = cls->get_literal(j); - if (lit2.var() != lit.var()) { - s |= m_antecedents.find(lit2.var()); - } - } - break; - } - case b_justification::BIN_CLAUSE: { - s |= m_antecedents.find(js.get_literal().var()); - break; - } - case b_justification::AXIOM: { - break; - } - case b_justification::JUSTIFICATION: { - literal_vector literals; - m_conflict_resolution->justification2literals(js.get_justification(), literals); - for (unsigned j = 0; j < literals.size(); ++j) { - s |= m_antecedents.find(literals[j].var()); - } - break; - } - } + justify(lit, s); } m_antecedents.insert(lit.var(), s); TRACE("context", display_literal_verbose(tout, lit); @@ -122,6 +93,39 @@ namespace smt { } } + void context::justify(literal lit, index_set& s) { + b_justification js = get_justification(lit.var()); + switch (js.get_kind()) { + case b_justification::CLAUSE: { + clause * cls = js.get_clause(); + if (!cls) break; + unsigned num_lits = cls->get_num_literals(); + for (unsigned j = 0; j < num_lits; ++j) { + literal lit2 = cls->get_literal(j); + if (lit2.var() != lit.var()) { + s |= m_antecedents.find(lit2.var()); + } + } + break; + } + case b_justification::BIN_CLAUSE: { + s |= m_antecedents.find(js.get_literal().var()); + break; + } + case b_justification::AXIOM: { + break; + } + case b_justification::JUSTIFICATION: { + literal_vector literals; + m_conflict_resolution->justification2literals(js.get_justification(), literals); + for (unsigned j = 0; j < literals.size(); ++j) { + s |= m_antecedents.find(literals[j].var()); + } + break; + } + } + } + void context::extract_fixed_consequences(unsigned& start, obj_map& vars, index_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); SASSERT(!inconsistent()); @@ -369,6 +373,142 @@ namespace smt { << ")\n"; } + void context::extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size) { + index_set _asms, _nasms; + u_map var2expr; + for (unsigned i = 0; i < asms.size(); ++i) { + literal lit = get_literal(asms[i]); + _asms.insert(lit.index()); + _nasms.insert((~lit).index()); + var2expr.insert(lit.var(), asms[i]); + } + + m_antecedents.reset(); + literal_vector const& lits = assigned_literals(); + for (unsigned i = 0; i < lits.size(); ++i) { + literal lit = lits[i]; + index_set s; + if (_asms.contains(lit.index())) { + s.insert(lit.var()); + } + else { + justify(lit, s); + } + m_antecedents.insert(lit.var(), s); + if (_nasms.contains(lit.index())) { + expr_ref_vector core(m_manager); + index_set::iterator it = s.begin(), end = s.end(); + for (; it != end; ++it) { + core.push_back(var2expr[*it]); + } + core.push_back(var2expr[lit.var()]); + cores.push_back(core); + min_core_size = std::min(min_core_size, core.size()); + } + } + } + + void context::preferred_sat(literal_vector& lits) { + bool retry = true; + while (retry) { + retry = false; + for (unsigned i = 0; i < lits.size(); ++i) { + literal lit = lits[i]; + if (lit == null_literal || get_assignment(lit) != l_undef) { + continue; + } + push_scope(); + assign(lit, b_justification::mk_axiom(), true); + while (!propagate()) { + lits[i] = null_literal; + retry = true; + if (!resolve_conflict() || inconsistent()) { + SASSERT(inconsistent()); + return; + } + } + } + } + } + + void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) { + unsigned num_true = 0, num_false = 0, num_undef = 0; + for (unsigned i = 0; i < asms.size(); ++i) { + literal lit = get_literal(asms[i]); + if (get_assignment(lit) == l_false) { + ++num_false; + } + if (get_assignment(lit) == l_true) { + ++num_true; + } + if (get_assignment(lit) == l_undef) { + ++num_undef; + } + } + out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n"; + } + + lbool context::preferred_sat(expr_ref_vector const& asms, vector& cores) { + pop_to_base_lvl(); + cores.reset(); + setup_context(false); + internalize_assertions(); + if (m_asserted_formulas.inconsistent() || inconsistent()) { + return l_false; + } + scoped_mk_model smk(*this); + init_search(); + flet l(m_searching, true); + unsigned level = m_scope_lvl; + unsigned min_core_size = UINT_MAX; + lbool is_sat = l_true; + unsigned num_restarts = 0; + + while (true) { + if (m_manager.canceled()) { + is_sat = l_undef; + break; + } + literal_vector lits; + for (unsigned i = 0; i < asms.size(); ++i) { + lits.push_back(get_literal(asms[i])); + } + preferred_sat(lits); + if (inconsistent()) { + SASSERT(m_scope_lvl == level); + is_sat = l_false; + break; + } + extract_cores(asms, cores, min_core_size); + IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size);); + + if (min_core_size <= 10) { + is_sat = l_undef; + break; + } + + is_sat = bounded_search(); + if (!restart(is_sat, level)) { + break; + } + ++num_restarts; + if (num_restarts >= min_core_size) { + is_sat = l_undef; + while (num_restarts <= 10*min_core_size) { + is_sat = bounded_search(); + if (!restart(is_sat, level)) { + break; + } + ++num_restarts; + } + break; + } + } + end_search(); + + return check_finalize(is_sat); + } + struct neg_literal { unsigned negate(unsigned i) { return (~to_literal(i)).index(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6b3d92602..e6d4d0c07 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1111,6 +1111,8 @@ namespace smt { if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); + //return false; + theory_id t1 = r1->m_th_var_list.get_th_id(); if (t1 == null_theory_id) return false; return get_theory(t1)->use_diseqs(); @@ -3293,19 +3295,6 @@ namespace smt { m_num_conflicts_since_restart = 0; } - struct context::scoped_mk_model { - context & m_ctx; - scoped_mk_model(context & ctx):m_ctx(ctx) { - m_ctx.m_proto_model = 0; - m_ctx.m_model = 0; - } - ~scoped_mk_model() { - if (m_ctx.m_proto_model.get() != 0) { - m_ctx.m_model = m_ctx.m_proto_model->mk_model(); - m_ctx.m_proto_model = 0; // proto_model is not needed anymore. - } - } - }; lbool context::search() { #ifndef _EXTERNAL_RELEASE @@ -3333,79 +3322,10 @@ namespace smt { TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";); TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << ", num_assigned: " << m_assigned_literals.size() << "\n";); - - if (m_last_search_failure != OK) { - if (status != l_false) { - // build candidate model before returning - mk_proto_model(status); - // status = l_undef; - } + + if (!restart(status, curr_lvl)) { break; } - - bool force_restart = false; - - if (status == l_false) { - break; - } - else if (status == l_true) { - SASSERT(!inconsistent()); - mk_proto_model(l_true); - // possible outcomes DONE l_true, DONE l_undef, CONTINUE - quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); - if (cmr == quantifier_manager::SAT) { - // done - break; - } - if (cmr == quantifier_manager::UNKNOWN) { - IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";); - // giving up - m_last_search_failure = QUANTIFIERS; - status = l_undef; - break; - } - status = l_undef; - force_restart = true; - } - - SASSERT(status == l_undef); - inc_limits(); - if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { - SASSERT(!inconsistent()); - IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations - << " :decisions " << m_stats.m_num_decisions - << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; - if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { - verbose_stream() << " :restart-outer " << m_restart_outer_threshold; - } - if (m_fparams.m_restart_adaptive) { - verbose_stream() << " :agility " << m_agility; - } - verbose_stream() << ")" << std::endl; verbose_stream().flush();); - // execute the restart - m_stats.m_num_restarts++; - if (m_scope_lvl > curr_lvl) { - pop_scope(m_scope_lvl - curr_lvl); - SASSERT(at_search_level()); - } - ptr_vector::iterator it = m_theory_set.begin(); - ptr_vector::iterator end = m_theory_set.end(); - for (; it != end && !inconsistent(); ++it) - (*it)->restart_eh(); - TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); - if (!inconsistent()) { - m_qmanager->restart_eh(); - } - if (inconsistent()) { - VERIFY(!resolve_conflict()); - status = l_false; - break; - } - } - if (m_fparams.m_simplify_clauses) - simplify_clauses(); - if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART) - del_inactive_lemmas(); } TRACE("search_lite", tout << "status: " << status << "\n";); @@ -3419,6 +3339,80 @@ namespace smt { end_search(); return status; } + + bool context::restart(lbool& status, unsigned curr_lvl) { + + if (m_last_search_failure != OK) { + if (status != l_false) { + // build candidate model before returning + mk_proto_model(status); + // status = l_undef; + } + return false; + } + + if (status == l_false) { + return false; + } + if (status == l_true) { + SASSERT(!inconsistent()); + mk_proto_model(l_true); + // possible outcomes DONE l_true, DONE l_undef, CONTINUE + quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); + if (cmr == quantifier_manager::SAT) { + // done + status = l_true; + return false; + } + if (cmr == quantifier_manager::UNKNOWN) { + IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";); + // giving up + m_last_search_failure = QUANTIFIERS; + status = l_undef; + return false; + } + } + inc_limits(); + if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { + SASSERT(!inconsistent()); + IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations + << " :decisions " << m_stats.m_num_decisions + << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; + if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { + verbose_stream() << " :restart-outer " << m_restart_outer_threshold; + } + if (m_fparams.m_restart_adaptive) { + verbose_stream() << " :agility " << m_agility; + } + verbose_stream() << ")" << std::endl; verbose_stream().flush();); + // execute the restart + m_stats.m_num_restarts++; + if (m_scope_lvl > curr_lvl) { + pop_scope(m_scope_lvl - curr_lvl); + SASSERT(at_search_level()); + } + ptr_vector::iterator it = m_theory_set.begin(); + ptr_vector::iterator end = m_theory_set.end(); + for (; it != end && !inconsistent(); ++it) + (*it)->restart_eh(); + TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); + if (!inconsistent()) { + m_qmanager->restart_eh(); + } + if (inconsistent()) { + VERIFY(!resolve_conflict()); + status = l_false; + return false; + } + } + if (m_fparams.m_simplify_clauses) + simplify_clauses(); + if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART) + del_inactive_lemmas(); + + status = l_undef; + return true; + } void context::tick(unsigned & counter) const { counter++; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 21d628e1a..c63d0614d 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -200,7 +200,20 @@ namespace smt { model_ref m_model; std::string m_unknown; void mk_proto_model(lbool r); - struct scoped_mk_model; + struct scoped_mk_model { + context & m_ctx; + scoped_mk_model(context & ctx):m_ctx(ctx) { + m_ctx.m_proto_model = 0; + m_ctx.m_model = 0; + } + ~scoped_mk_model() { + if (m_ctx.m_proto_model.get() != 0) { + m_ctx.m_model = m_ctx.m_proto_model->mk_model(); + m_ctx.m_proto_model = 0; // proto_model is not needed anymore. + } + } + }; + // ----------------------------------- // @@ -234,7 +247,6 @@ namespace smt { return m_params; } - bool get_cancel_flag() { return !m_manager.limit().inc(); } region & get_region() { @@ -1056,6 +1068,8 @@ namespace smt { void inc_limits(); + bool restart(lbool& status, unsigned curr_lvl); + void tick(unsigned & counter) const; lbool bounded_search(); @@ -1367,6 +1381,13 @@ namespace smt { void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector const& conseq, expr_ref_vector const& unfixed); + void justify(literal lit, index_set& s); + + void extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size); + + void preferred_sat(literal_vector& literals); + + void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size); public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); @@ -1410,6 +1431,8 @@ namespace smt { lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + + lbool preferred_sat(expr_ref_vector const& asms, vector& cores); lbool setup_and_check(bool reset_cancel = true); diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 6b626c2de..5e3b091bc 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -322,6 +322,9 @@ namespace smt { bool context::check_th_diseq_propagation() const { TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";); int num = get_num_bool_vars(); + if (inconsistent()) { + return true; + } for (bool_var v = 0; v < num; v++) { if (has_enode(v)) { enode * n = bool_var2enode(v); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index df39b4186..9bdf962ec 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -115,6 +115,11 @@ namespace smt { return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } + lbool preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_kernel.preferred_sat(asms, cores); + } + + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_kernel.find_mutexes(vars, mutexes); } @@ -282,6 +287,10 @@ namespace smt { return m_imp->get_consequences(assumptions, vars, conseq, unfixed); } + lbool kernel::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_imp->preferred_sat(asms, cores); + } + lbool kernel::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_imp->find_mutexes(vars, mutexes); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index ea09081ec..264fae011 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -133,11 +133,16 @@ namespace smt { lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); - /* + /** \brief find mutually exclusive variables. */ lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + /** + \brief Preferential SAT. + */ + lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + /** \brief Return the model associated with the last check command. */ diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index fd07188e5..b665c2a94 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -21,294 +21,351 @@ Notes: #include "smt_context.h" #include "ast_pp.h" #include "theory_wmaxsat.h" +#include "smt_justification.h" namespace smt { -theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc): - theory(m.mk_family_id("weighted_maxsat")), - m_mc(mc), - m_vars(m), - m_fmls(m), - m_zweights(m_mpz), - m_old_values(m_mpz), - m_zcost(m_mpz), - m_zmin_cost(m_mpz), - m_found_optimal(false), - m_propagate(false), - m_normalize(false), - m_den(1) -{} - -theory_wmaxsat::~theory_wmaxsat() { - m_old_values.reset(); -} - -/** - \brief return the complement of variables that are currently assigned. -*/ -void theory_wmaxsat::get_assignment(svector& result) { - result.reset(); + theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc): + theory(m.mk_family_id("weighted_maxsat")), + m_mc(mc), + m_vars(m), + m_fmls(m), + m_zweights(m_mpz), + m_old_values(m_mpz), + m_zcost(m_mpz), + m_zmin_cost(m_mpz), + m_found_optimal(false), + m_propagate(false), + m_normalize(false), + m_den(1) + {} - if (!m_found_optimal) { - for (unsigned i = 0; i < m_vars.size(); ++i) { - result.push_back(false); - } + theory_wmaxsat::~theory_wmaxsat() { + m_old_values.reset(); } - else { - std::sort(m_cost_save.begin(), m_cost_save.end()); - for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) { - if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) { + + /** + \brief return the complement of variables that are currently assigned. + */ + void theory_wmaxsat::get_assignment(svector& result) { + result.reset(); + + if (!m_found_optimal) { + for (unsigned i = 0; i < m_vars.size(); ++i) { result.push_back(false); - ++j; - } - else { - result.push_back(true); } } + else { + std::sort(m_cost_save.begin(), m_cost_save.end()); + for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) { + if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) { + result.push_back(false); + ++j; + } + else { + result.push_back(true); + } + } + } + TRACE("opt", + tout << "cost save: "; + for (unsigned i = 0; i < m_cost_save.size(); ++i) { + tout << m_cost_save[i] << " "; + } + tout << "\nvars: "; + for (unsigned i = 0; i < m_vars.size(); ++i) { + tout << mk_pp(m_vars[i].get(), get_manager()) << " "; + } + tout << "\nassignment: "; + for (unsigned i = 0; i < result.size(); ++i) { + tout << result[i] << " "; + } + tout << "\n";); } - TRACE("opt", - tout << "cost save: "; - for (unsigned i = 0; i < m_cost_save.size(); ++i) { - tout << m_cost_save[i] << " "; - } - tout << "\nvars: "; - for (unsigned i = 0; i < m_vars.size(); ++i) { - tout << mk_pp(m_vars[i].get(), get_manager()) << " "; - } - tout << "\nassignment: "; - for (unsigned i = 0; i < result.size(); ++i) { - tout << result[i] << " "; - } - tout << "\n";); -} - -void theory_wmaxsat::init_search_eh() { - m_propagate = true; -} - -expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true) { - context & ctx = get_context(); - 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()); - wfml = m.mk_or(var, fml); - ctx.assert_expr(wfml); - m_rweights.push_back(w); - m_vars.push_back(var); - m_fmls.push_back(fml); - m_assigned.push_back(false); - if (!is_true) { - m_rmin_cost += w; + void theory_wmaxsat::init_search_eh() { + m_propagate = true; } - m_normalize = true; - return ctx.bool_var2expr(register_var(var, true)); -} - -bool_var theory_wmaxsat::register_var(app* var, bool attach) { - context & ctx = get_context(); - bool_var bv; - SASSERT(!ctx.e_internalized(var)); - enode* x = ctx.mk_enode(var, false, true, true); - if (ctx.b_internalized(var)) { - bv = ctx.get_bool_var(var); + + expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w) { + context & ctx = get_context(); + 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()); + wfml = m.mk_or(var, fml); + ctx.assert_expr(wfml); + m_rweights.push_back(w); + m_vars.push_back(var); + m_fmls.push_back(fml); + m_assigned.push_back(false); + m_enabled.push_back(true); + m_normalize = true; + bool_var bv = register_var(var, true); + TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n"; + tout << wfml << "\n";); + return var; } - else { - bv = ctx.mk_bool_var(var); - } - ctx.set_enode_flag(bv, true); - if (attach) { - ctx.set_var_theory(bv, get_id()); - theory_var v = mk_var(x); - ctx.attach_th_var(x, this, v); - m_bool2var.insert(bv, v); - SASSERT(v == static_cast(m_var2bool.size())); - m_var2bool.push_back(bv); - SASSERT(ctx.bool_var2enode(bv)); - } - return bv; -} -rational const& theory_wmaxsat::get_min_cost() { - unsynch_mpq_manager mgr; - scoped_mpq q(mgr); - mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); - m_rmin_cost = rational(q); - return m_rmin_cost; -} - -void theory_wmaxsat::assign_eh(bool_var v, bool is_true) { - TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";); - if (is_true) { - if (m_normalize) normalize(); + void theory_wmaxsat::disable_var(expr* var) { context& ctx = get_context(); - theory_var tv = m_bool2var[v]; - if (m_assigned[tv]) return; - scoped_mpz w(m_mpz); - w = m_zweights[tv]; - ctx.push_trail(numeral_trail(m_zcost, m_old_values)); - ctx.push_trail(push_back_vector >(m_costs)); - ctx.push_trail(value_trail(m_assigned[tv])); - m_zcost += w; - m_costs.push_back(tv); - m_assigned[tv] = true; - if (m_zcost > m_zmin_cost) { - block(); + SASSERT(ctx.b_internalized(var)); + bool_var bv = ctx.get_bool_var(var); + theory_var tv = m_bool2var[bv]; + m_enabled[tv] = false; + TRACE("opt", tout << "disable: v" << tv << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";); + } + + bool_var theory_wmaxsat::register_var(app* var, bool attach) { + context & ctx = get_context(); + bool_var bv; + SASSERT(!ctx.e_internalized(var)); + enode* x = ctx.mk_enode(var, false, true, true); + if (ctx.b_internalized(var)) { + bv = ctx.get_bool_var(var); } - } -} - -final_check_status theory_wmaxsat::final_check_eh() { - if (m_normalize) normalize(); - return FC_DONE; -} - - -void theory_wmaxsat::reset_eh() { - theory::reset_eh(); - reset_local(); -} - -void theory_wmaxsat::reset_local() { - m_vars.reset(); - m_fmls.reset(); - m_rweights.reset(); - m_rmin_cost.reset(); - m_rcost.reset(); - m_zweights.reset(); - m_zcost.reset(); - m_zmin_cost.reset(); - m_cost_save.reset(); - m_bool2var.reset(); - m_var2bool.reset(); - m_propagate = false; - m_found_optimal = false; - m_assigned.reset(); -} - - -void theory_wmaxsat::propagate() { - context& ctx = get_context(); - for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { - bool_var bv = m_var2bool[i]; - lbool asgn = ctx.get_assignment(bv); - if (asgn == l_true) { - assign_eh(bv, true); + else { + bv = ctx.mk_bool_var(var); } + ctx.set_enode_flag(bv, true); + if (attach) { + ctx.set_var_theory(bv, get_id()); + theory_var v = mk_var(x); + ctx.attach_th_var(x, this, v); + m_bool2var.insert(bv, v); + SASSERT(v == static_cast(m_var2bool.size())); + m_var2bool.push_back(bv); + SASSERT(ctx.bool_var2enode(bv)); + } + return bv; } - m_propagate = false; -} - -bool theory_wmaxsat::is_optimal() const { - return !m_found_optimal || m_zcost < m_zmin_cost; -} - -expr_ref theory_wmaxsat::mk_block() { - ++m_stats.m_num_blocks; - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { - weight += m_zweights[costs[i]]; - disj.push_back(m.mk_not(m_vars[costs[i]].get())); - } - if (is_optimal()) { + + rational theory_wmaxsat::get_cost() { unsynch_mpq_manager mgr; scoped_mpq q(mgr); - mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); - rational rw = rational(q); - m_zmin_cost = weight; - m_found_optimal = true; + mgr.set(q, m_zcost, m_den.to_mpq().numerator()); + return rational(q); + } + + void theory_wmaxsat::init_min_cost(rational const& r) { + m_rmin_cost = r; + m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator(); + } + + + void theory_wmaxsat::assign_eh(bool_var v, bool is_true) { + if (is_true) { + if (m_normalize) normalize(); + context& ctx = get_context(); + theory_var tv = m_bool2var[v]; + if (m_assigned[tv] || !m_enabled[tv]) return; + scoped_mpz w(m_mpz); + w = m_zweights[tv]; + ctx.push_trail(numeral_trail(m_zcost, m_old_values)); + ctx.push_trail(push_back_vector >(m_costs)); + ctx.push_trail(value_trail(m_assigned[tv])); + m_zcost += w; + TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";); + m_costs.push_back(tv); + m_assigned[tv] = true; + if (m_zcost >= m_zmin_cost) { + block(); + } + else { + m_can_propagate = true; + } + } + } + + final_check_status theory_wmaxsat::final_check_eh() { + if (m_normalize) normalize(); + // std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n"; + return FC_DONE; + } + + + void theory_wmaxsat::reset_eh() { + theory::reset_eh(); + reset_local(); + } + + void theory_wmaxsat::reset_local() { + m_vars.reset(); + m_fmls.reset(); + m_rweights.reset(); + m_rmin_cost.reset(); + m_zweights.reset(); + m_zcost.reset(); + m_zmin_cost.reset(); m_cost_save.reset(); - m_cost_save.append(m_costs); + m_bool2var.reset(); + m_var2bool.reset(); + m_propagate = false; + m_can_propagate = false; + m_found_optimal = false; + m_assigned.reset(); + m_enabled.reset(); + } + + + void theory_wmaxsat::propagate() { + context& ctx = get_context(); + for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { + bool_var bv = m_var2bool[i]; + lbool asgn = ctx.get_assignment(bv); + if (asgn == l_true) { + assign_eh(bv, true); + } + } + m_propagate = false; + //while (m_found_optimal && max_unassigned_is_blocked() && !ctx.inconsistent()) { } + + m_can_propagate = false; + } + + bool theory_wmaxsat::is_optimal() const { + return !m_found_optimal || m_zcost < m_zmin_cost; + } + + expr_ref theory_wmaxsat::mk_block() { + ++m_stats.m_num_blocks; + ast_manager& m = get_manager(); + expr_ref_vector disj(m); + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { + theory_var tv = costs[i]; + if (m_enabled[tv]) { + weight += m_zweights[tv]; + disj.push_back(m.mk_not(m_vars[tv].get())); + } + } + if (is_optimal()) { + m_found_optimal = true; + m_cost_save.reset(); + m_cost_save.append(m_costs); + TRACE("opt", + tout << "costs: "; + for (unsigned i = 0; i < m_costs.size(); ++i) { + tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; + } + tout << "\n"; + //get_context().display(tout); + ); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); TRACE("opt", - tout << "costs: "; - for (unsigned i = 0; i < m_costs.size(); ++i) { - tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; - } - tout << "\n"; - get_context().display(tout); - ); + tout << result << " weight: " << weight << "\n"; + tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); + return result; } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - TRACE("opt", - tout << result << " weight: " << weight << "\n"; - tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); - return result; -} -expr_ref theory_wmaxsat::mk_optimal_block(svector const& ws, rational const& weight) { - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - rational new_w = weight*m_den; - m_zmin_cost = new_w.to_mpq().numerator(); - m_cost_save.reset(); - for (unsigned i = 0; i < ws.size(); ++i) { - bool_var bv = ws[i]; - theory_var v = m_bool2var[bv]; - m_cost_save.push_back(v); - disj.push_back(m.mk_not(m_vars[v].get())); - } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - return result; -} + void theory_wmaxsat::restart_eh() {} -void theory_wmaxsat::block() { - if (m_vars.empty()) { - return; + void theory_wmaxsat::block() { + if (m_vars.empty()) { + return; + } + ++m_stats.m_num_blocks; + context& ctx = get_context(); + literal_vector lits; + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { + weight += m_zweights[costs[i]]; + lits.push_back(literal(m_var2bool[costs[i]])); + } + TRACE("opt", ctx.display_literals_verbose(tout, lits); tout << "\n";); + + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, 0, 0))); + } + + bool theory_wmaxsat::max_unassigned_is_blocked() { + context& ctx = get_context(); + unsigned max_unassigned = m_max_unassigned_index; + if (max_unassigned < m_sorted_vars.size() && + m_zcost + m_zweights[m_sorted_vars[max_unassigned]] < m_zmin_cost) { + return false; + } + // update value of max-unassigned + while (max_unassigned < m_sorted_vars.size() && + ctx.get_assignment(m_var2bool[m_sorted_vars[max_unassigned]]) != l_undef) { + ++max_unassigned; + } + // + if (max_unassigned > m_max_unassigned_index) { + ctx.push_trail(value_trail(m_max_unassigned_index)); + m_max_unassigned_index = max_unassigned; + } + if (max_unassigned < m_sorted_vars.size() && + m_zcost + m_zweights[m_sorted_vars[max_unassigned]] >= m_zmin_cost) { + theory_var tv = m_sorted_vars[max_unassigned]; + propagate(m_var2bool[tv]); + m_max_unassigned_index++; + return true; + } + + return false; } - ++m_stats.m_num_blocks; - context& ctx = get_context(); - literal_vector lits; - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { - weight += m_zweights[costs[i]]; - lits.push_back(~literal(m_var2bool[costs[i]])); - } - TRACE("opt", - ast_manager& m = get_manager(); - tout << "block: "; - for (unsigned i = 0; i < lits.size(); ++i) { - expr_ref tmp(m); - ctx.literal2expr(lits[i], tmp); - tout << tmp << " "; - } - tout << "\n"; - ); - - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); -} + void theory_wmaxsat::propagate(bool_var v) { + ++m_stats.m_num_propagations; + context& ctx = get_context(); + literal_vector lits; + literal lit(v, true); + + SASSERT(ctx.get_assignment(lit) == l_undef); + + for (unsigned i = 0; i < m_costs.size(); ++i) { + bool_var w = m_var2bool[m_costs[i]]; + lits.push_back(literal(w)); + } + TRACE("opt", + ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); + ctx.display_literal_verbose(tout << " --> ", lit);); + + region& r = ctx.get_region(); + ctx.assign(lit, ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), r, lits.size(), lits.c_ptr(), 0, 0, lit, 0, 0))); + } -void theory_wmaxsat::normalize() { - m_den = rational::one(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - m_den = lcm(m_den, denominator(m_rweights[i])); + void theory_wmaxsat::normalize() { + m_den = rational::one(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + if (m_enabled[i]) { + m_den = lcm(m_den, denominator(m_rweights[i])); + } + } + m_den = lcm(m_den, denominator(m_rmin_cost)); + SASSERT(!m_den.is_zero()); + m_zweights.reset(); + m_sorted_vars.reset(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + rational r = m_rweights[i]*m_den; + SASSERT(r.is_int()); + mpq const& q = r.to_mpq(); + m_zweights.push_back(q.numerator()); + m_sorted_vars.push_back(i); + } + compare_cost compare_cost(*this); + std::sort(m_sorted_vars.begin(), m_sorted_vars.end(), compare_cost); + m_max_unassigned_index = 0; + + m_zcost.reset(); + rational r = m_rmin_cost * m_den; + m_zmin_cost = r.to_mpq().numerator(); + m_normalize = false; } - m_den = lcm(m_den, denominator(m_rmin_cost)); - SASSERT(!m_den.is_zero()); - m_zweights.reset(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - rational r = m_rweights[i]*m_den; - SASSERT(r.is_int()); - mpq const& q = r.to_mpq(); - m_zweights.push_back(q.numerator()); - } - rational r = m_rcost* m_den; - m_zcost = r.to_mpq().numerator(); - r = m_rmin_cost * m_den; - m_zmin_cost = r.to_mpq().numerator(); - m_normalize = false; -} }; diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 0804c4b68..0f711b9f8 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -28,6 +28,7 @@ namespace smt { class theory_wmaxsat : public theory { struct stats { unsigned m_num_blocks; + unsigned m_num_propagations; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; @@ -39,27 +40,31 @@ namespace smt { scoped_mpz_vector m_zweights; scoped_mpz_vector m_old_values; svector m_costs; // set of asserted theory variables + unsigned m_max_unassigned_index; // index of literal that is not yet assigned and has maximal weight. + svector m_sorted_vars; // set of all theory variables, sorted by cost svector m_cost_save; // set of asserted theory variables - rational m_rcost; // current sum of asserted costs rational m_rmin_cost; // current maximal cost assignment. scoped_mpz m_zcost; // current sum of asserted costs scoped_mpz m_zmin_cost; // current maximal cost assignment. bool m_found_optimal; u_map m_bool2var; // bool_var -> theory_var svector m_var2bool; // theory_var -> bool_var - bool m_propagate; + bool m_propagate; + bool m_can_propagate; bool m_normalize; rational m_den; // lcm of denominators for rational weights. - svector m_assigned; + svector m_assigned, m_enabled; stats m_stats; public: theory_wmaxsat(ast_manager& m, filter_model_converter& mc); virtual ~theory_wmaxsat(); void get_assignment(svector& result); - virtual void init_search_eh(); - expr* assert_weighted(expr* fml, rational const& w, bool is_true); + expr* assert_weighted(expr* fml, rational const& w); + void disable_var(expr* var); bool_var register_var(app* var, bool attach); - rational const& get_min_cost(); + rational get_cost(); + void init_min_cost(rational const& r); + class numeral_trail : public trail { typedef scoped_mpz T; T & m_value; @@ -79,6 +84,8 @@ namespace smt { m_old_values.shrink(m_old_values.size() - 1); } }; + + virtual void init_search_eh(); virtual void assign_eh(bool_var v, bool is_true); virtual final_check_status final_check_eh(); virtual bool use_diseqs() const { @@ -95,23 +102,30 @@ namespace smt { virtual void new_eq_eh(theory_var v1, theory_var v2) { } virtual void new_diseq_eh(theory_var v1, theory_var v2) { } virtual void display(std::ostream& out) const {} + virtual void restart_eh(); virtual void collect_statistics(::statistics & st) const { st.update("wmaxsat num blocks", m_stats.m_num_blocks); + st.update("wmaxsat num props", m_stats.m_num_propagations); } virtual bool can_propagate() { - return m_propagate; + return m_propagate || m_can_propagate; } virtual void propagate(); + bool is_optimal() const; expr_ref mk_block(); - expr_ref mk_optimal_block(svector const& ws, rational const& weight); + + private: void block(); + void propagate(bool_var v); void normalize(); + + bool max_unassigned_is_blocked(); class compare_cost { theory_wmaxsat& m_th; diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 441ece429..9163cfeda 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -154,6 +154,10 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector& return l_true; } +lbool solver::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return check_sat(0, 0); +} + bool solver::is_literal(ast_manager& m, expr* e) { return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 15932fd5d..d5d9ccfd5 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -151,9 +151,9 @@ public: /** \brief under assumptions, asms, retrieve set of consequences that - fix values for expressions that can be built from vars. - The consequences are clauses whose first literal constrain one of the - functions from vars and the other literals are negations of literals from asms. + fix values for expressions that can be built from vars. + The consequences are clauses whose first literal constrain one of the + functions from vars and the other literals are negations of literals from asms. */ virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); @@ -166,6 +166,12 @@ public: virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + /** + \brief Preferential SAT. Prefer assumptions to be true, produce cores that witness cases when not all assumptions can be met. + by default, preferred sat ignores the assumptions. + */ + virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + /** \brief Display the content of this solver. */