From ddb30c51b53f19398215f9d31059b54077fc2b1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Dec 2013 12:17:33 -0800 Subject: [PATCH] debugging lia2maxsat Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 15 ++--- src/opt/maxsmt.h | 6 +- src/opt/opt_context.cpp | 116 ++++++++++++++++++++++-------------- src/opt/opt_context.h | 11 +++- src/opt/weighted_maxsat.cpp | 21 +++---- 5 files changed, 104 insertions(+), 65 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 4fc184a13..8232e169e 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -32,6 +32,7 @@ namespace opt { m_msolver = 0; m_s = &s; if (m_soft_constraints.empty()) { + TRACE("opt", tout << "no constraints\n";); m_msolver = 0; is_sat = s.check_sat(0, 0); m_answer.reset(); @@ -75,29 +76,29 @@ namespace opt { return m_answer; } - inf_eps maxsmt::get_value() const { + rational maxsmt::get_value() const { if (m_msolver) { - return inf_eps(m_msolver->get_value()); + return m_msolver->get_value(); } - return inf_eps(m_upper); + return m_upper; } - inf_eps maxsmt::get_lower() const { + rational maxsmt::get_lower() const { rational r = m_lower; if (m_msolver) { rational q = m_msolver->get_lower(); if (r < q) r = q; } - return inf_eps(r); + return r; } - inf_eps maxsmt::get_upper() const { + rational maxsmt::get_upper() const { rational r = m_upper; if (m_msolver) { rational q = m_msolver->get_upper(); if (r > q) r = q; } - return inf_eps(r); + return r; } void maxsmt::update_lower(rational const& r) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 14e8515b7..d4eff4334 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -74,9 +74,9 @@ namespace opt { rational weight(unsigned idx) const { return m_weights[idx]; } void commit_assignment(); - inf_eps get_value() const; - inf_eps get_lower() const; - inf_eps get_upper() const; + rational get_value() const; + rational get_lower() const; + rational get_upper() const; void update_lower(rational const& r); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index f38605a61..1bb34f6dd 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -209,8 +209,10 @@ namespace opt { } bool context::is_maxsat(expr* fml, expr_ref_vector& terms, - vector& weights, symbol& id, unsigned& index) { + vector& weights, rational& offset, + bool& neg, symbol& id, unsigned& index) { if (!is_app(fml)) return false; + neg = false; app* a = to_app(fml); if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) { terms.append(a->get_num_args(), a->get_args()); @@ -219,25 +221,46 @@ namespace opt { return true; } app_ref term(m); - if (is_minimize(fml, term, index)) { + offset = rational::zero(); + if (is_minimize(fml, term, index) && + get_pb_sum(term, terms, weights, offset)) { TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";); - rational coeff(0); // minimize 2*x + 3*y // <=> // (assert-soft (not x) 2) // (assert-soft (not y) 3) // - if (get_pb_sum(term, terms, weights, coeff) && coeff.is_zero()) { - for (unsigned i = 0; i < weights.size(); ++i) { - if (!weights[i].is_pos()) { - return false; - } + for (unsigned i = 0; i < weights.size(); ++i) { + if (weights[i].is_neg()) { + offset += weights[i]; + weights[i].neg(); } - for (unsigned i = 0; i < terms.size(); ++i) { + else { terms[i] = m.mk_not(terms[i].get()); } - return true; } + return true; + } + if (is_maximize(fml, term, index) && + get_pb_sum(term, terms, weights, offset)) { + TRACE("opt", tout << "try to convert maximization" << mk_pp(term, m) << "\n";); + // maximize 2*x + 3*y - z + // <=> + // (assert-soft x 2) + // (assert-soft y 3) + // (assert-soft (not z) 1) + // offset := 6 + // maximize = offset - penalty + // + for (unsigned i = 0; i < weights.size(); ++i) { + if (weights[i].is_neg()) { + weights[i].neg(); + terms[i] = m.mk_not(terms[i].get()); + } + offset += weights[i]; + } + neg = true; + return true; } return false; } @@ -281,9 +304,11 @@ namespace opt { app_ref tr(m); expr_ref_vector terms(m); vector weights; + rational offset; unsigned index; symbol id; - if (is_maxsat(fml, terms, weights, id, index)) { + bool neg; + if (is_maxsat(fml, terms, weights, offset, neg, id, index)) { objective& obj = m_objectives[index]; if (obj.m_type != O_MAXSMT) { // change from maximize/minimize. @@ -298,6 +323,9 @@ namespace opt { SASSERT(obj.m_id == id); obj.m_terms.reset(); obj.m_terms.append(terms); + obj.m_offset = offset; + obj.m_neg = neg; + TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";); } else if (is_maximize(fml, tr, index)) { m_objectives[index].m_term = tr; @@ -390,51 +418,47 @@ namespace opt { void context::display_assignment(std::ostream& out) { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; - switch(obj.m_type) { - case O_MAXSMT: { - symbol s = obj.m_id; - if (s != symbol::null) { - out << s << " : "; - } - maxsmt* ms = m_maxsmts.find(s); - out << ms->get_value() << "\n"; - break; - } - default: - break; - } + display_objective(out, obj); + out << get_upper(i) << "\n"; } - m_optsmt.display_assignment(out); } void context::display_range_assignment(std::ostream& out) { - for (unsigned i = 0; i < m_objectives.size(); ++i) { + for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; - switch(obj.m_type) { - case O_MAXSMT: { - symbol s = obj.m_id; - if (s != symbol::null) { - out << s << " : "; - } - maxsmt* ms = m_maxsmts.find(s); - out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n"; - break; - } - default: - break; - } + display_objective(out, obj); + out << " [" << get_lower(i) << ":" << get_upper(i) << "]\n"; } - m_optsmt.display_range_assignment(out); } + void context::display_objective(std::ostream& out, objective const& obj) const { + switch(obj.m_type) { + case O_MAXSMT: { + symbol s = obj.m_id; + if (s != symbol::null) { + out << s << " : "; + } + break; + } + default: + out << obj.m_term << " "; + break; + } + } + + expr_ref context::get_lower(unsigned idx) { if (idx > m_objectives.size()) { throw default_exception("index out of bounds"); } objective const& obj = m_objectives[idx]; switch(obj.m_type) { - case O_MAXSMT: - return to_expr(m_maxsmts.find(obj.m_id)->get_lower()); + case O_MAXSMT: { + rational r = m_maxsmts.find(obj.m_id)->get_lower(); + if (obj.m_neg) r.neg(); + r += obj.m_offset; + return to_expr(inf_eps(r)); + } case O_MINIMIZE: case O_MAXIMIZE: return to_expr(m_optsmt.get_lower(obj.m_index)); @@ -450,8 +474,12 @@ namespace opt { } objective const& obj = m_objectives[idx]; switch(obj.m_type) { - case O_MAXSMT: - return to_expr(m_maxsmts.find(obj.m_id)->get_upper()); + case O_MAXSMT: { + rational r = m_maxsmts.find(obj.m_id)->get_upper(); + if (obj.m_neg) r.neg(); + r += obj.m_offset; + return to_expr(inf_eps(r)); + } case O_MINIMIZE: case O_MAXIMIZE: return to_expr(m_optsmt.get_upper(obj.m_index)); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index b1424d165..2e19c3cb3 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -49,6 +49,8 @@ namespace opt { app_ref m_term; // for maximize, minimize term expr_ref_vector m_terms; // for maxsmt vector m_weights; // for maxsmt + rational m_offset; // for maxsmt + bool m_neg; // negate symbol m_id; // for maxsmt unsigned m_index; // for maximize/minimize index @@ -56,6 +58,8 @@ namespace opt { m_type(is_max?O_MAXIMIZE:O_MINIMIZE), m_term(t), m_terms(t.get_manager()), + m_offset(0), + m_neg(false), m_id(), m_index(idx) {} @@ -64,6 +68,8 @@ namespace opt { m_type(O_MAXSMT), m_term(m), m_terms(m), + m_offset(0), + m_neg(false), m_id(id), m_index(0) {} @@ -119,7 +125,8 @@ namespace opt { bool is_maximize(expr* fml, app_ref& term, unsigned& index); bool is_minimize(expr* fml, app_ref& term, unsigned& index); bool is_maxsat(expr* fml, expr_ref_vector& terms, - vector& weights, symbol& id, unsigned& index); + vector& weights, rational& offset, bool& neg, + symbol& id, unsigned& index); expr* mk_maximize(unsigned index, app* t); expr* mk_minimize(unsigned index, app* t); expr* mk_maxsat(unsigned index, unsigned num_fmls, expr* const* fmls); @@ -132,6 +139,8 @@ namespace opt { opt_solver& get_solver(); + void display_objective(std::ostream& out, objective const& obj) const; + }; } diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 613ce41d5..dbc943fbd 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -218,12 +218,15 @@ namespace smt { if (m_min_cost_atom) { lits.push_back(~literal(m_min_cost_bv)); } - IF_VERBOSE(2, verbose_stream() << "block: " << m_costs.size() << " " << lits.size() << " " << m_min_cost << "\n";); - IF_VERBOSE(2, for (unsigned i = 0; i < lits.size(); ++i) { - verbose_stream() << lits[i] << " "; - } - verbose_stream() << "\n"; - ); + IF_VERBOSE(2, + verbose_stream() << "block: "; + for (unsigned i = 0; i < lits.size(); ++i) { + expr_ref tmp(m); + ctx.literal2expr(lits[i], tmp); + verbose_stream() << tmp << " "; + } + verbose_stream() << "\n"; + ); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (is_final && m_cost < m_min_cost) { @@ -312,6 +315,7 @@ namespace opt { */ lbool operator()() { + TRACE("opt", tout << "weighted maxsat\n";); smt::theory_weighted_maxsat& wth = ensure_theory(); lbool result; { @@ -319,11 +323,7 @@ namespace opt { for (unsigned i = 0; i < m_soft.size(); ++i) { wth.assert_weighted(m_soft[i].get(), m_weights[i]); } -#if 1 result = s.check_sat_core(0,0); -#else - result = iterative_weighted_maxsat(s, *wth); -#endif wth.get_assignment(m_assignment); if (!m_assignment.empty() && result == l_false) { @@ -331,6 +331,7 @@ namespace opt { } } m_upper = wth.get_min_cost(); + TRACE("opt", tout << "min cost: " << m_upper << "\n";); wth.reset(); return result; }