diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index d2f308488..d27d17790 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -126,6 +126,15 @@ namespace opt { } } + void maxsmt::add(expr* f, rational const& w) { + TRACE("opt", tout << mk_pp(f, m) << " weight: " << w << "\n";); + SASSERT(m.is_bool(f)); + SASSERT(w.is_pos()); + m_soft_constraints.push_back(f); + m_weights.push_back(w); + m_upper += w; + } + void maxsmt::display_answer(std::ostream& out) const { for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { out << mk_pp(m_soft_constraints[i], m) diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index ffcfcab63..c4cf33cac 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -64,14 +64,7 @@ namespace opt { void updt_params(params_ref& p); - void add(expr* f, rational const& w) { - SASSERT(m.is_bool(f)); - SASSERT(w.is_pos()); - m_soft_constraints.push_back(f); - m_weights.push_back(w); - m_upper += w; - } - + 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]; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 36775aab3..bf6faa005 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -547,6 +547,10 @@ namespace opt { void context::from_fmls(expr_ref_vector const& fmls) { + TRACE("opt", + for (unsigned i = 0; i < fmls.size(); ++i) { + tout << mk_pp(fmls[i], m) << "\n"; + }); m_hard_constraints.reset(); expr* orig_term; for (unsigned i = 0; i < fmls.size(); ++i) { @@ -607,6 +611,10 @@ namespace opt { break; } } + TRACE("opt", + for (unsigned i = 0; i < fmls.size(); ++i) { + tout << mk_pp(fmls[i].get(), m) << "\n"; + }); } void context::internalize() { @@ -670,6 +678,11 @@ namespace opt { } } + void context::display(std::ostream& out) { + + } + + void context::display_assignment(std::ostream& out) { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index fe5f91406..3fad9a59d 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -123,6 +123,7 @@ namespace opt { virtual std::string reason_unknown() const { return std::string("unknown"); } virtual void display_assignment(std::ostream& out); + void display(std::ostream& out); static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 36242543d..36c7911c3 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -778,92 +778,8 @@ namespace opt { } } }; - /** - Iteratively increase cost until there is an assignment during - final_check that satisfies min_cost. - - Takes: log (n / log(n)) iterations - */ - class iwmax : public maxsmt_solver_wbase { - public: - iwmax(solver* s, ast_manager& m, smt::context& ctx): maxsmt_solver_wbase(s, m, ctx) {} - virtual ~iwmax() {} - lbool operator()() { - scoped_ensure_theory wth(*this); - solver::scoped_push _s(s()); - for (unsigned i = 0; i < m_soft.size(); ++i) { - wth().assert_weighted(m_soft[i].get(), m_weights[i]); - } - solver::scoped_push __s(s()); - rational cost = wth().get_min_cost(); - rational log_cost(1), tmp(1); - while (tmp < cost) { - ++log_cost; - tmp *= rational(2); - } - expr_ref_vector bounds(m); - expr_ref bound(m); - lbool result = l_false; - unsigned nsc = 0; - m_upper = cost; - while (result == l_false) { - bound = wth().set_min_cost(log_cost); - s().push(); - ++nsc; - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";); - TRACE("opt", tout << "cost: " << log_cost << " " << bound << "\n";); - bounds.push_back(bound); - result = conditional_solve(bound); - if (result == l_false) { - m_lower = log_cost; - } - if (log_cost > cost) { - break; - } - log_cost *= rational(2); - if (m_cancel) { - result = l_undef; - } - } - s().pop(nsc); - return result; - } - private: - lbool conditional_solve(expr* cond) { - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.conditional solve)\n";); - smt::theory_wmaxsat& wth = *get_theory(); - bool was_sat = false; - lbool is_sat = l_true; - while (l_true == is_sat) { - is_sat = s().check_sat(1,&cond); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - if (wth.is_optimal()) { - s().get_model(m_model); - was_sat = true; - } - expr_ref fml = wth.mk_block(); - s().assert_expr(fml); - } - } - if (was_sat) { - wth.get_assignment(m_assignment); - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - } - if (is_sat == l_true) { - m_lower = m_upper = wth.get_min_cost(); - } - TRACE("opt", tout << "min cost: " << m_upper << "\n";); - return is_sat; - } - - }; class wmax : public maxsmt_solver_wbase { public: @@ -914,19 +830,21 @@ namespace opt { }; class bvmax : public maxsmt_solver_base { - solver* mk_sat_solver(solver* s) { + solver* mk_sat_solver() { tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); - unsigned sz = s->get_num_assertions(); + unsigned sz = s().get_num_assertions(); for (unsigned i = 0; i < sz; ++i) { - sat_solver->assert_expr(s->get_assertion(i)); + sat_solver->assert_expr(s().get_assertion(i)); } return sat_solver; } public: - bvmax(solver* s, ast_manager& m): maxsmt_solver_base(mk_sat_solver(s), m) {} + bvmax(solver* s, ast_manager& m): maxsmt_solver_base(s, m) { + m_s = mk_sat_solver(); + } virtual ~bvmax() {} // @@ -1058,9 +976,6 @@ namespace opt { if (m_maxsmt) { return *m_maxsmt; } - if (m_engine == symbol("iwmax")) { - m_maxsmt = alloc(iwmax, s.get(), m, s->get_context()); - } else if (m_engine == symbol("pwmax")) { m_maxsmt = alloc(pwmax, s.get(), m); } @@ -1118,6 +1033,7 @@ namespace opt { void updt_params(params_ref& p) { opt_params _p(p); m_engine = _p.wmaxsat_engine(); + std::cout << m_engine << "\n"; m_maxsmt = 0; } }; @@ -1159,6 +1075,92 @@ namespace opt { #if 0 + + /** + Iteratively increase cost until there is an assignment during + final_check that satisfies min_cost. + + Takes: log (n / log(n)) iterations + */ + class iwmax : public maxsmt_solver_wbase { + public: + + iwmax(solver* s, ast_manager& m, smt::context& ctx): maxsmt_solver_wbase(s, m, ctx) {} + virtual ~iwmax() {} + + lbool operator()() { + pb_util + solver::scoped_push _s(s()); + for (unsigned i = 0; i < m_soft.size(); ++i) { + wth().assert_weighted(m_soft[i].get(), m_weights[i]); + } + solver::scoped_push __s(s()); + rational cost = wth().get_min_cost(); + rational log_cost(1), tmp(1); + while (tmp < cost) { + ++log_cost; + tmp *= rational(2); + } + expr_ref_vector bounds(m); + expr_ref bound(m); + lbool result = l_false; + unsigned nsc = 0; + m_upper = cost; + while (result == l_false) { + bound = wth().set_min_cost(log_cost); + s().push(); + ++nsc; + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";); + TRACE("opt", tout << "cost: " << log_cost << " " << bound << "\n";); + bounds.push_back(bound); + result = conditional_solve(wth(), bound); + if (result == l_false) { + m_lower = log_cost; + } + if (log_cost > cost) { + break; + } + log_cost *= rational(2); + if (m_cancel) { + result = l_undef; + } + } + s().pop(nsc); + return result; + } + private: + lbool conditional_solve(smt::theory_wmaxsat& wth, expr* cond) { + bool was_sat = false; + lbool is_sat = l_true; + while (l_true == is_sat) { + is_sat = s().check_sat(1,&cond); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + if (wth.is_optimal()) { + s().get_model(m_model); + was_sat = true; + } + expr_ref fml = wth.mk_block(); + s().assert_expr(fml); + } + } + if (was_sat) { + wth.get_assignment(m_assignment); + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + } + if (is_sat == l_true) { + m_lower = m_upper = wth.get_min_cost(); + } + TRACE("opt", tout << "min cost: " << m_upper << " sat: " << is_sat << "\n";); + return is_sat; + } + + }; + // ------------------------------------------------------ // Version from CP'13 lbool wpm2b_solve() { diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 92b1b4626..556f5047a 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -29,8 +29,6 @@ theory_wmaxsat::theory_wmaxsat(ast_manager& m, ref& mc): m_mc(mc), m_vars(m), m_fmls(m), - m_min_cost_atom(m), - m_min_cost_atoms(m), m_zweights(m_mpz), m_old_values(m_mpz), m_zcost(m_mpz), @@ -138,21 +136,6 @@ rational const& theory_wmaxsat::get_min_cost() { return m_rmin_cost; } -expr* theory_wmaxsat::set_min_cost(rational const& c) { - m_normalize = true; - ast_manager& m = get_manager(); - std::ostringstream strm; - strm << "cost <= " << c; - m_rmin_cost = c; - m_min_cost_atom = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); - m_min_cost_atoms.push_back(m_min_cost_atom); - m_mc->insert(m_min_cost_atom->get_decl()); - - m_min_cost_bv = register_var(m_min_cost_atom, false); - - return m_min_cost_atom; -} - 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) { @@ -194,8 +177,6 @@ void theory_wmaxsat::reset_eh() { m_cost_save.reset(); m_bool2var.reset(); m_var2bool.reset(); - m_min_cost_atom = 0; - m_min_cost_atoms.reset(); m_propagate = false; m_found_optimal = false; m_assigned.reset(); @@ -231,9 +212,6 @@ expr_ref theory_wmaxsat::mk_block() { weight += m_zweights[costs[i]]; disj.push_back(m.mk_not(m_vars[costs[i]].get())); } - if (m_min_cost_atom) { - disj.push_back(m.mk_not(m_min_cost_atom)); - } if (is_optimal()) { unsynch_mpq_manager mgr; scoped_mpq q(mgr); @@ -272,9 +250,6 @@ expr_ref theory_wmaxsat::mk_optimal_block(svector const& ws, rational m_cost_save.push_back(v); disj.push_back(m.mk_not(m_vars[v].get())); } - if (m_min_cost_atom) { - disj.push_back(m.mk_not(m_min_cost_atom)); - } expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); return result; } @@ -297,9 +272,6 @@ void theory_wmaxsat::block() { weight += m_zweights[costs[i]]; lits.push_back(~literal(m_var2bool[costs[i]])); } - if (m_min_cost_atom) { - lits.push_back(~literal(m_min_cost_bv)); - } TRACE("opt", tout << "block: "; for (unsigned i = 0; i < lits.size(); ++i) { diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 21f7fd907..b6974957c 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -32,9 +32,6 @@ namespace smt { 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 - app_ref m_min_cost_atom; // atom tracking modified lower bound - app_ref_vector m_min_cost_atoms; - bool_var m_min_cost_bv; // max cost Boolean variable vector m_rweights; // weights of theory variables. scoped_mpz_vector m_zweights; scoped_mpz_vector m_old_values; @@ -60,7 +57,6 @@ namespace smt { bool_var assert_weighted(expr* fml, rational const& w); bool_var register_var(app* var, bool attach); rational const& get_min_cost(); - expr* set_min_cost(rational const& c); class numeral_trail : public trail { typedef scoped_mpz T; T & m_value;