diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h index af19e46e6..61d146136 100644 --- a/src/ast/rewriter/pb_rewriter_def.h +++ b/src/ast/rewriter/pb_rewriter_def.h @@ -209,9 +209,6 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: k = PBU::numeral::one(); } else if (g > PBU::numeral::one()) { - IF_VERBOSE(3, verbose_stream() << "cut " << g << "\n"; - display(verbose_stream(), args, k, is_eq); - ); // // Example 5x + 5y + 2z + 2u >= 5 diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp new file mode 100644 index 000000000..0aee3cbd5 --- /dev/null +++ b/src/opt/pb_sls.cpp @@ -0,0 +1,220 @@ +#include "pb_sls.h" +#include "smt_literal.h" +#include "ast_pp.h" + +namespace smt { + struct pb_sls::imp { + + struct clause { + literal_vector m_lits; + scoped_mpz_vector m_weights; + scoped_mpz m_k; + scoped_mpz m_value; + bool m_eq; + clause(unsynch_mpz_manager& m): + m_weights(m), + m_k(m), + m_value(m), + m_eq(true) + {} + clause(clause const& cls): + m_lits(cls.m_lits), + m_weights(cls.m_weights.m()), + m_k(cls.m_k), + m_value(cls.m_value), + m_eq(cls.m_eq) { + for (unsigned i = 0; i < cls.m_weights.size(); ++i) { + m_weights.push_back(cls.m_weights[i]); + } + } + }; + + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + ast_manager& m; + pb_util pb; + unsynch_mpz_manager mgr; + volatile bool m_cancel; + vector m_clauses; // clauses to be satisfied + vector m_soft; // soft constraints + vector m_weights; // weights of soft constraints + rational m_value; // current value of soft constraints + vector m_pos, m_neg; // positive and negative occurs. + svector m_assignment; // current assignment. + obj_map m_expr2var; // map expressions to Boolean variables. + ptr_vector m_var2expr; // reverse map + + imp(ast_manager& m): + m(m), + pb(m), + m_cancel(false) + {} + + ~imp() { + } + + void add(expr* f) { + clause cls(mgr); + if (compile_clause(f, cls)) { + m_clauses.push_back(cls); + } + } + void add(expr* f, rational const& w) { + clause cls(mgr); + if (compile_clause(f, cls)) { + m_clauses.push_back(cls); + } + } + + void init_value(expr* f, bool b) { + literal lit = mk_literal(f); + SASSERT(!lit.sign()); + //if (m_assignment[lit.var()] != b) { + m_assignment[lit.var()] = b; + //} + } + + lbool operator()() { + return l_undef; + } + + bool get_value(expr* f) { + unsigned var; + if (m_expr2var.find(f, var)) { + return m_assignment[var]; + } + UNREACHABLE(); + return true; + } + bool get_value(literal l) { + return l.sign() ^ m_assignment[l.var()]; + } + void set_cancel(bool f) { + m_cancel = f; + } + void collect_statistics(statistics& st) const { + } + void get_model(model_ref& mdl) { + } + void updt_params(params_ref& p) { + } + + literal mk_literal(expr* f) { + literal result; + bool sign = false; + while (m.is_not(f, f)) { + sign = !sign; + } + if (m.is_true(f)) { + result = true_literal; + } + else if (m.is_false(f)) { + result = false_literal; + } + else { + unsigned var; + if (!m_expr2var.find(f, var)) { + var = m_pos.size(); + SASSERT(m_expr2var.size() == var); + m_pos.push_back(unsigned_vector()); + m_neg.push_back(unsigned_vector()); + m_assignment.push_back(false); + m_expr2var.insert(f, var); + m_var2expr.push_back(f); + } + result = literal(var); + } + if (sign) { + result.neg(); + } + return result; + } + + bool compile_clause(expr* _f, clause& cls) { + if (!is_app(_f)) return false; + app* f = to_app(_f); + unsigned sz = f->get_num_args(); + expr* const* args = f->get_args(); + literal lit; + rational coeff; + if (pb.is_ge(f) || pb.is_eq(f)) { + for (unsigned i = 0; i < sz; ++i) { + coeff = pb.get_coeff(f, i); + SASSERT(coeff.is_int()); + lit = mk_literal(args[i]); + if (lit == null_literal) return false; + cls.m_lits.push_back(lit); + cls.m_weights.push_back(coeff.to_mpq().numerator()); + if (get_value(lit)) { + cls.m_value += coeff.to_mpq().numerator(); + } + } + cls.m_eq = pb.is_eq(f); + coeff = pb.get_k(f); + SASSERT(coeff.is_int()); + cls.m_k = coeff.to_mpq().numerator(); + } + else if (m.is_or(f)) { + for (unsigned i = 0; i < sz; ++i) { + lit = mk_literal(args[i]); + if (lit == null_literal) return false; + cls.m_lits.push_back(lit); + cls.m_weights.push_back(mpz(1)); + if (get_value(lit)) { + cls.m_value += mpz(1); + } + } + cls.m_eq = false; + cls.m_k = mpz(1); + } + else { + lit = mk_literal(f); + if (lit == null_literal) return false; + cls.m_lits.push_back(lit); + cls.m_weights.push_back(mpz(1)); + cls.m_eq = true; + cls.m_k = mpz(1); + } + return true; + } + + }; + + pb_sls::pb_sls(ast_manager& m) { + m_imp = alloc(imp, m); + } + pb_sls::~pb_sls() { + dealloc(m_imp); + } + void pb_sls::add(expr* f) { + m_imp->add(f); + } + void pb_sls::add(expr* f, rational const& w) { + m_imp->add(f, w); + } + void pb_sls::init_value(expr* f, bool b) { + m_imp->init_value(f, b); + } + lbool pb_sls::operator()() { + return (*m_imp)(); + } + bool pb_sls::get_value(expr* f) { + return m_imp->get_value(f); + } + void pb_sls::set_cancel(bool f) { + m_imp->set_cancel(f); + } + void pb_sls::collect_statistics(statistics& st) const { + m_imp->collect_statistics(st); + } + void pb_sls::get_model(model_ref& mdl) { + m_imp->get_model(mdl); + } + void pb_sls::updt_params(params_ref& p) { + m_imp->updt_params(p); + } + +} diff --git a/src/opt/pb_sls.h b/src/opt/pb_sls.h new file mode 100644 index 000000000..01362fe31 --- /dev/null +++ b/src/opt/pb_sls.h @@ -0,0 +1,50 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + pb_sls.h + +Abstract: + + SLS for PB optimization. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-03-18 + +Notes: + +--*/ +#ifndef _PB_SLS_H_ +#define _PB_SLS_H_ + +#include "pb_decl_plugin.h" +#include "model.h" +#include "lbool.h" +#include "params.h" +#include "statistics.h" + +namespace smt { + + class pb_sls { + struct imp; + imp* m_imp; + public: + pb_sls(ast_manager& m); + ~pb_sls(); + void add(expr* f); + void add(expr* f, rational const& w); + void init_value(expr* f, bool b); + lbool operator()(); + bool get_value(expr* f); + void set_cancel(bool f); + void collect_statistics(statistics& st) const; + void get_model(model_ref& mdl); + void updt_params(params_ref& p); + }; + + +}; + +#endif diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 330dc8df8..89e0a5813 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -539,6 +539,10 @@ namespace opt { if (wth().is_optimal()) { m_upper = wth().get_min_cost(); updt_model(s); + s.display(std::cout); + model_ref mdl; + s.get_model(mdl); + model_smt2_pp(std::cout, m, *(mdl.get()), 0); } expr_ref fml = wth().mk_block(); s.assert_expr(fml);