From c3232693f074af8dc11c0db896cd662a57e87c0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Feb 2015 09:46:21 -0800 Subject: [PATCH] use PB solver instead of full arithmetic for bouding Pareto fronts so that difference logic theory isn't broken. Codeplex issue 175 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 92 ++++++++++++++++++----------------------- src/opt/opt_context.h | 2 +- src/opt/opt_pareto.cpp | 2 +- src/opt/opt_solver.cpp | 8 ++++ src/opt/opt_solver.h | 1 + 5 files changed, 51 insertions(+), 54 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5971cceb7..f22ce479e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -327,78 +327,66 @@ namespace opt { expr_ref context::mk_le(unsigned i, model_ref& mdl) { objective const& obj = m_objectives[i]; - expr_ref val(m), result(m), term(m); - mk_term_val(mdl, obj, term, val); - switch (obj.m_type) { - case O_MINIMIZE: - result = mk_ge(term, val); - break; - case O_MAXSMT: - result = mk_ge(term, val); - break; - case O_MAXIMIZE: - result = mk_ge(val, term); - break; - } - return result; + return mk_cmp(false, mdl, obj); } expr_ref context::mk_ge(unsigned i, model_ref& mdl) { objective const& obj = m_objectives[i]; - expr_ref val(m), result(m), term(m); - mk_term_val(mdl, obj, term, val); - switch (obj.m_type) { - case O_MINIMIZE: - result = mk_ge(val, term); - break; - case O_MAXSMT: - result = mk_ge(val, term); - break; - case O_MAXIMIZE: - result = mk_ge(term, val); - break; - } - return result; + return mk_cmp(true, mdl, obj); } + expr_ref context::mk_gt(unsigned i, model_ref& mdl) { expr_ref result = mk_le(i, mdl); result = m.mk_not(result); return result; } - - void context::mk_term_val(model_ref& mdl, objective const& obj, expr_ref& term, expr_ref& val) { - rational r; + + expr_ref context::mk_cmp(bool is_ge, model_ref& mdl, objective const& obj) { + rational k(0); + expr_ref val(m), result(m); switch (obj.m_type) { case O_MINIMIZE: + is_ge = !is_ge; case O_MAXIMIZE: - term = obj.m_term; - break; - case O_MAXSMT: { - unsigned sz = obj.m_terms.size(); - expr_ref_vector sum(m); - expr_ref zero(m); - zero = m_arith.mk_numeral(rational(0), false); - for (unsigned i = 0; i < sz; ++i) { - expr* t = obj.m_terms[i]; - rational const& w = obj.m_weights[i]; - sum.push_back(m.mk_ite(t, m_arith.mk_numeral(w, false), zero)); - } - if (sum.empty()) { - term = zero; + VERIFY(mdl->eval(obj.m_term, val) && is_numeral(val, k)); + if (is_ge) { + result = mk_ge(obj.m_term, val); } else { - term = m_arith.mk_add(sum.size(), sum.c_ptr()); - } + result = mk_ge(val, obj.m_term); + } + break; + case O_MAXSMT: { + m_opt_solver->ensure_pb(); + pb_util pb(m); + unsigned sz = obj.m_terms.size(); + ptr_vector terms; + vector coeffs; + for (unsigned i = 0; i < sz; ++i) { + terms.push_back(obj.m_terms[i]); + coeffs.push_back(obj.m_weights[i]); + VERIFY(mdl->eval(obj.m_terms[i], val)); + if (m.is_true(val)) { + k += obj.m_weights[i]; + } + } + if (is_ge) { + result = pb.mk_ge(sz, coeffs.c_ptr(), terms.c_ptr(), k); + } + else { + result = pb.mk_le(sz, coeffs.c_ptr(), terms.c_ptr(), k); + } break; } } TRACE("opt", - model_smt2_pp(tout << "Model:\n", m, *mdl, 0); - mdl->eval(term, val); tout << term << " " << val << "\n";); - VERIFY(mdl->eval(term, val) && is_numeral(val, r)); - } - + tout << (is_ge?">= ":"<= ") << k << "\n"; + display_objective(tout, obj); + tout << "\n"; + tout << result << "\n";); + return result; + } expr_ref context::mk_ge(expr* t, expr* s) { expr_ref result(m); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 3b764aaf5..001dd1b62 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -282,7 +282,7 @@ namespace opt { // pareto void yield(); expr_ref mk_ge(expr* t, expr* s); - void mk_term_val(model_ref& mdl, objective const& obj, expr_ref& term, expr_ref& val); + expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj); }; diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp index e8b295d9f..5e1d4b269 100644 --- a/src/opt/opt_pareto.cpp +++ b/src/opt/opt_pareto.cpp @@ -68,7 +68,7 @@ namespace opt { fmls.push_back(m.mk_or(gt.size(), gt.c_ptr())); fml = m.mk_and(fmls.size(), fmls.c_ptr()); IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";); - TRACE("opt", tout << fml << "\n";); + TRACE("opt", tout << fml << "\n"; model_smt2_pp(tout, m, *m_model, 0);); m_solver->assert_expr(fml); } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 2a12818c5..08bc20004 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -86,6 +86,14 @@ namespace opt { m_context.set_logic(logic); } + void opt_solver::ensure_pb() { + smt::theory_id th_id = m.get_family_id("pb"); + smt::theory* th = get_context().get_theory(th_id); + if (!th) { + get_context().register_plugin(alloc(smt::theory_pb, m, m_params)); + } + } + smt::theory_opt& opt_solver::get_optimizer() { smt::context& ctx = m_context.get_context(); smt::theory_id arith_id = m_context.m().get_family_id("arith"); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index f9702705f..e45f4be91 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -122,6 +122,7 @@ namespace opt { bool dump_benchmarks(); smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat. + void ensure_pb(); smt::theory_opt& get_optimizer();