From c0de1e34acdcd35a624168fa3db041c1d2504b20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Nov 2013 14:54:42 -0800 Subject: [PATCH] working on upper bound optimziation Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 9 ++ src/ast/ast_smt2_pp.h | 3 + src/muz/pdr/pdr_farkas_learner.cpp | 4 +- src/opt/opt_cmds.cpp | 1 + src/opt/opt_context.cpp | 11 +- src/opt/opt_context.h | 2 + src/opt/opt_solver.cpp | 8 +- src/opt/optimize_objectives.cpp | 153 ++++++++++++++++--------- src/opt/optimize_objectives.h | 9 +- src/smt/theory_arith.h | 15 ++- src/smt/theory_arith_aux.h | 174 +++++++++++++++++++++++++---- src/smt/theory_arith_core.h | 26 +++-- src/smt/theory_arith_int.h | 12 +- src/smt/theory_diff_logic.h | 3 +- src/smt/theory_diff_logic_def.h | 15 +-- src/smt/theory_opt.h | 8 +- src/util/inf_eps_rational.h | 15 +++ 17 files changed, 343 insertions(+), 125 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 1ad2b8222..ce2c426ea 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1110,6 +1110,15 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) { return out; } +std::ostream& operator<<(std::ostream& out, expr_ref const& e) { + return out << mk_ismt2_pp(e.get(), e.get_manager()); +} + +std::ostream& operator<<(std::ostream& out, app_ref const& e) { + return out << mk_ismt2_pp(e.get(), e.get_manager()); +} + + #ifdef Z3DEBUG void pp(expr const * n, ast_manager & m) { std::cout << mk_ismt2_pp(const_cast(n), m) << std::endl; diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index aa84d6e03..175ec9c4a 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -110,4 +110,7 @@ struct mk_ismt2_pp { std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p); +std::ostream& operator<<(std::ostream& out, expr_ref const& e); +std::ostream& operator<<(std::ostream& out, app_ref const& e); + #endif diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 7c38bf86f..5946ccb2a 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -34,8 +34,6 @@ Revision History: #include "proof_utils.h" #include "reg_decl_plugins.h" -#define PROOF_MODE PGM_FINE -//#define PROOF_MODE PGM_COARSE namespace pdr { @@ -374,7 +372,7 @@ namespace pdr { farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr) : m_proof_params(get_proof_params(params)), - m_pr(PROOF_MODE), + m_pr(PGM_FINE), m_constr(0), m_combine_farkas_coefficients(true), p2o(m_pr, outer_mgr), diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index bb8bf3e73..e08b9652f 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -159,6 +159,7 @@ public: insert_timeout(p); insert_max_memory(p); p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); + opt::context::collect_param_descrs(p); } virtual char const * get_main_descr() const { return "check sat modulo objective function";} diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 781b6582e..e1b664f4c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -17,9 +17,6 @@ Notes: TODO: - there are race conditions for cancelation. - - it would also be a good idea to maintain a volatile bool to track - cancelation and then bail out of loops inside optimize() and derived - functions. --*/ @@ -30,6 +27,7 @@ Notes: #include "opt_solver.h" #include "arith_decl_plugin.h" #include "th_rewriter.h" +#include "opt_params.hpp" namespace opt { @@ -154,12 +152,17 @@ namespace opt { } } + void context::collect_param_descrs(param_descrs & r) { + opt_params::collect_param_descrs(r); + } + void context::updt_params(params_ref& p) { m_params.append(p); if (m_solver) { m_solver->updt_params(m_params); } - + opt_params _p(m_params); + m_opt_objectives.set_engine(_p.engine()); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index c71b941c7..0aa137748 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -68,6 +68,8 @@ namespace opt { void collect_statistics(statistics& stats); + static void collect_param_descrs(param_descrs & r); + void updt_params(params_ref& p); private: diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index e863f4e89..1c4a5bc4c 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -101,13 +101,7 @@ namespace opt { smt::theory_opt& opt = get_optimizer(); for (unsigned i = 0; i < m_objective_vars.size(); ++i) { smt::theory_var v = m_objective_vars[i]; - bool is_bounded = opt.maximize(v); - if (is_bounded) { - m_objective_values.push_back(opt.get_objective_value(v)); - } else { - inf_eps r(rational(1), inf_rational(0)); - m_objective_values.push_back(r); - } + m_objective_values.push_back(opt.maximize(v)); } } return r; diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 870d0d2f1..589214476 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -62,26 +62,18 @@ namespace opt { } } - /* Enumerate locally optimal assignments until fixedpoint. */ - lbool optimize_objectives::basic_opt(app_ref_vector& objectives) { - arith_util autil(m); - - opt_solver::scoped_push _push(*s); - - for (unsigned i = 0; i < objectives.size(); ++i) { - m_vars.push_back(s->add_objective(objectives[i].get())); - } - + lbool optimize_objectives::basic_opt() { + opt_solver::toggle_objective _t(*s, true); lbool is_sat = l_true; - // Disabled while testing and tuning: - // is_sat = update_upper(); - opt_solver::toggle_objective _t(*s, true); while (is_sat == l_true && !m_cancel) { - is_sat = update_lower(); + is_sat = s->check_sat(0, 0); + if (is_sat == l_true) { + update_lower(); + } } if (m_cancel || is_sat == l_undef) { @@ -90,73 +82,117 @@ namespace opt { return l_true; } - lbool optimize_objectives::update_lower() { - lbool is_sat = s->check_sat(0, 0); - if (is_sat == l_true) { - model_ref md; - s->get_model(md); - set_max(m_lower, s->get_objective_values()); - IF_VERBOSE(1, - for (unsigned i = 0; i < m_lower.size(); ++i) { - verbose_stream() << m_lower[i] << " "; - } - verbose_stream() << "\n"; - // model_pp(verbose_stream(), *md); - ); - expr_ref_vector disj(m); - expr_ref constraint(m); - - for (unsigned i = 0; i < m_lower.size(); ++i) { - inf_eps const& v = m_lower[i]; - disj.push_back(s->block_lower_bound(i, v)); - } - constraint = m.mk_or(disj.size(), disj.c_ptr()); - s->assert_expr(constraint); + /* + Enumerate locally optimal assignments until fixedpoint. + */ + lbool optimize_objectives::farkas_opt() { + smt::theory_opt& opt = s->get_optimizer(); + + IF_VERBOSE(1, verbose_stream() << typeid(opt).name() << "\n";); + if (typeid(smt::theory_inf_arith) != typeid(opt)) { + return l_undef; } - return is_sat; + + opt_solver::toggle_objective _t(*s, true); + lbool is_sat= l_true; + + while (is_sat == l_true && !m_cancel) { + is_sat = update_upper(); + } + + if (m_cancel || is_sat == l_undef) { + return l_undef; + } + return l_true; + } + + void optimize_objectives::update_lower() { + model_ref md; + s->get_model(md); + set_max(m_lower, s->get_objective_values()); + IF_VERBOSE(1, + for (unsigned i = 0; i < m_lower.size(); ++i) { + verbose_stream() << m_lower[i] << " "; + } + verbose_stream() << "\n"; + // model_pp(verbose_stream(), *md); + ); + expr_ref_vector disj(m); + expr_ref constraint(m); + + for (unsigned i = 0; i < m_lower.size(); ++i) { + inf_eps const& v = m_lower[i]; + disj.push_back(s->block_lower_bound(i, v)); + } + constraint = m.mk_or(disj.size(), disj.c_ptr()); + s->assert_expr(constraint); } lbool optimize_objectives::update_upper() { smt::theory_opt& opt = s->get_optimizer(); - IF_VERBOSE(1, verbose_stream() << typeid(opt).name() << "\n";); - if (typeid(smt::theory_inf_arith) != typeid(opt)) { - return l_true; - } + SASSERT(typeid(smt::theory_inf_arith) == typeid(opt)); + smt::theory_inf_arith& th = dynamic_cast(opt); expr_ref bound(m); expr_ref_vector bounds(m); opt_solver::scoped_push _push(*s); + // // NB: we have to create all bound expressions before calling check_sat // because the state after check_sat is not at base level. // + vector mid; + for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) { if (m_lower[i] < m_upper[i]) { - SASSERT(m_upper[i].get_infinity().is_pos()); smt::theory_var v = m_vars[i]; - bound = th.block_upper_bound(v, m_upper[i]); + mid.push_back((m_upper[i]+m_lower[i])/rational(2)); + bound = th.block_upper_bound(v, mid[i]); bounds.push_back(bound); } else { bounds.push_back(0); + mid.push_back(inf_eps()); } } + bool progress = false; for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) { - if (m_lower[i] < m_upper[i]) { + if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) { + th.enable_record_conflict(bounds[i].get()); lbool is_sat = s->check_sat(1, bounds.c_ptr() + i); - if (is_sat == l_true) { + th.enable_record_conflict(0); + switch(is_sat) { + case l_true: IF_VERBOSE(2, verbose_stream() << "Setting lower bound for v" << m_vars[i] << " to " << m_upper[i] << "\n";); - m_lower[i] = m_upper[i]; - } - else if (is_sat == l_false) { - // else: TBD extract Farkas coefficients. + m_lower[i] = mid[i]; + update_lower(); + break; + case l_false: + if (!th.conflict_minimize().get_infinity().is_zero()) { + // bounds is not in the core. The context is unsat. + m_upper[i] = m_lower[i]; + return l_false; + } + else { + m_upper[i] = std::min(m_upper[i], th.conflict_minimize()); + } + break; + default: + return l_undef; } + progress = true; } } + if (m_cancel) { + return l_undef; + } + if (!progress) { + return l_false; + } return l_true; } @@ -177,7 +213,24 @@ namespace opt { // First check_sat call to initialize theories lbool is_sat = s->check_sat(0, 0); if (is_sat == l_true) { - is_sat = basic_opt(objectives); + opt_solver::scoped_push _push(*s); + + for (unsigned i = 0; i < objectives.size(); ++i) { + m_vars.push_back(s->add_objective(objectives[i].get())); + } + + if (m_engine == symbol("basic")) { + is_sat = basic_opt(); + } + else if (m_engine == symbol("farkas")) { + is_sat = farkas_opt(); + } + else { + // TODO: implement symba engine + // report error on bad configuration. + NOT_IMPLEMENTED_YET(); + UNREACHABLE(); + } values.reset(); values.append(m_lower); } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index 227cd8f00..cb9f2241b 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -34,6 +34,7 @@ namespace opt { vector m_lower; vector m_upper; svector m_vars; + symbol m_engine; public: optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {} @@ -41,13 +42,17 @@ namespace opt { void set_cancel(bool f); + void set_engine(symbol const& e) { m_engine = e; } + private: - lbool basic_opt(app_ref_vector& objectives); + lbool basic_opt(); + + lbool farkas_opt(); void set_max(vector& dst, vector const& src); - lbool update_lower(); + void update_lower(); lbool update_upper(); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 724cce200..45e2ffdfa 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -90,6 +90,7 @@ namespace smt { static const int dead_row_id = -1; protected: bool proofs_enabled() const { return get_manager().proofs_enabled(); } + bool coeffs_enabled() const { return proofs_enabled() || m_bound_watch != null_bool_var; } struct linear_monomial { numeral m_coeff; @@ -995,11 +996,19 @@ namespace smt { // Optimization // // ----------------------------------- - virtual bool maximize(theory_var v); + virtual inf_eps_rational maximize(theory_var v); virtual theory_var add_objective(app* term); - virtual inf_eps_rational get_objective_value(theory_var v); virtual expr* block_lower_bound(theory_var v, inf_rational const& val); - virtual expr* block_upper_bound(theory_var v, inf_numeral const& val); + expr* block_upper_bound(theory_var v, inf_numeral const& val); + void enable_record_conflict(expr* bound); + void record_conflict(unsigned num_lits, literal const * lits, + unsigned num_eqs, enode_pair const * eqs, + unsigned num_params, parameter* params); + inf_eps_rational conflict_minimize(); + private: + bool_var m_bound_watch; + inf_eps_rational m_upper_bound; + public: // ----------------------------------- // // Pretty Printing diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index e864db589..cdd28e130 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -21,6 +21,8 @@ Revision History: #include"inf_eps_rational.h" #include"theory_arith.h" +#include"smt_farkas_util.h" +#include"th_rewriter.h" namespace smt { @@ -977,14 +979,20 @@ namespace smt { } template - bool theory_arith::maximize(theory_var v) { + inf_eps_rational theory_arith::maximize(theory_var v) { bool r = max_min(v, true); - if (!r && at_upper(v)) { + if (at_upper(v)) { m_objective_value = get_value(v); } - return r || at_upper(v); + else if (!r) { + m_objective_value = inf_eps_rational::infinity(); + } + return m_objective_value; } + /** + \brief: assert val < v + */ template expr* theory_arith::block_lower_bound(theory_var v, inf_rational const& val) { ast_manager& m = get_manager(); @@ -1000,6 +1008,9 @@ namespace smt { } } + /** + \brief assert val <= v + */ template expr* theory_arith::block_upper_bound(theory_var v, inf_numeral const& val) { ast_manager& m = get_manager(); @@ -1007,29 +1018,154 @@ namespace smt { std::ostringstream strm; strm << val << " <= v" << v; expr* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); - bool_var bv = ctx.mk_bool_var(b); - ctx.set_var_theory(bv, get_id()); - // ctx.set_enode_flag(bv, true); - inf_numeral val1 = val; - if (!Ext::is_infinite(val)) { - val1 += Ext::m_real_epsilon; + if (!ctx.b_internalized(b)) { + bool_var bv = ctx.mk_bool_var(b); + ctx.set_var_theory(bv, get_id()); + // ctx.set_enode_flag(bv, true); + atom* a = alloc(atom, bv, v, val, A_LOWER); + m_unassigned_atoms[v]++; + m_var_occs[v].push_back(a); + m_atoms.push_back(a); + insert_bv2a(bv, a); + TRACE("arith", tout << mk_pp(b, m) << "\n"; + display_atom(tout, a, false);); } - atom* a = alloc(atom, bv, v, val1, A_LOWER); - m_unassigned_atoms[v]++; - m_var_occs[v].push_back(a); - m_atoms.push_back(a); - insert_bv2a(bv, a); - TRACE("arith", tout << mk_pp(b, m) << "\n"; - display_atom(tout, a, false); - display_atoms(tout);); return b; } + + /** + \brief enable watching bound atom. + */ template - inf_eps_rational theory_arith::get_objective_value(theory_var v) { - return m_objective_value; + void theory_arith::enable_record_conflict(expr* bound) { + m_params.m_arith_bound_prop = BP_NONE; + SASSERT(propagation_mode() == BP_NONE); // bound propagtion rules are not (yet) handled. + if (bound) { + context& ctx = get_context(); + m_bound_watch = ctx.get_bool_var(bound); + } + else { + m_bound_watch = null_bool_var; + } + m_upper_bound = -inf_eps_rational::infinity(); } + /** + \brief + pos < 0 + == + r(Ax <= b) + q(v <= val) + == + val' <= q*v & q*v <= q*val + + q*v - val' >= 0 + + => + (q*v - val' - q*v)/q >= -v + == + val/q <= v + */ + + template + void theory_arith::record_conflict( + unsigned num_lits, literal const * lits, + unsigned num_eqs, enode_pair const * eqs, + unsigned num_params, parameter* params) { + ast_manager& m = get_manager(); + context& ctx = get_context(); + if (null_bool_var == m_bound_watch) { + return; + } + unsigned idx = num_lits; + for (unsigned i = 0; i < num_lits; ++i) { + if (m_bound_watch == lits[i].var()) { + //SASSERT(!lits[i].sign()); + idx = i; + break; + } + } + if (idx == num_lits) { + return; + } + SASSERT(num_params == 1 + num_lits + num_eqs); + SASSERT(params[0].is_symbol()); + SASSERT(params[0].get_symbol() == symbol("farkas")); // for now, just handle this rule. + farkas_util farkas(m); + expr_ref tmp(m), vq(m); + expr* x, *y, *e; + rational q; + for (unsigned i = 0; i < num_lits; ++i) { + parameter const& pa = params[i+1]; + SASSERT(pa.is_rational()); + if (idx == i) { + q = abs(pa.get_rational()); + continue; + } + ctx.literal2expr(~lits[i], tmp); + farkas.add(abs(pa.get_rational()), to_app(tmp)); + } + for (unsigned i = 0; i < num_eqs; ++i) { + enode_pair const& p = eqs[i]; + x = p.first->get_owner(); + y = p.second->get_owner(); + tmp = m.mk_not(m.mk_eq(x,y)); + parameter const& pa = params[1 + num_lits + i]; + SASSERT(pa.is_rational()); + farkas.add(abs(pa.get_rational()), to_app(tmp)); + } + tmp = farkas.get(); + std::cout << tmp << "\n"; + atom* a = get_bv2a(m_bound_watch); + SASSERT(a); + expr_ref_vector terms(m); + vector mults; + bool strict = false; + if (m_util.is_le(tmp, x, y) || m_util.is_ge(tmp, y, x)) { + } + else if (m_util.is_lt(tmp, x, y) || m_util.is_gt(tmp, y, x)) { + strict = true; + } + else if (m.is_eq(tmp, x, y)) { + } + else { + UNREACHABLE(); + } + e = var2expr(a->get_var()); + q = -q*farkas.get_normalize_factor(); + SASSERT(!m_util.is_int(e) || q.is_int()); // TBD: not fully handled. + if (q.is_one()) { + vq = e; + } + else { + vq = m_util.mk_mul(m_util.mk_numeral(q, q.is_int()), e); + } + vq = m_util.mk_add(m_util.mk_sub(x, y), vq); + if (!q.is_one()) { + vq = m_util.mk_div(vq, m_util.mk_numeral(q, q.is_int())); + } + th_rewriter rw(m); + rw(vq, tmp); + IF_VERBOSE(1, verbose_stream() << tmp << "\n";); + VERIFY(m_util.is_numeral(tmp, q)); + if (m_upper_bound < q) { + m_upper_bound = q; + if (strict) { + m_upper_bound -= get_epsilon(a->get_var()); + } + } + } + + /** + \brief find the minimal upper bound on the variable that was last enabled + for conflict recording. + */ + template + inf_eps_rational theory_arith::conflict_minimize() { + return m_upper_bound; + } + + /** \brief Maximize (Minimize) the given temporary row. Return true if succeeded. diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 983d0a9ea..68900cb50 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -879,7 +879,7 @@ namespace smt { bool_var bv = ctx.mk_bool_var(n); ctx.set_var_theory(bv, get_id()); rational _k; - m_util.is_numeral(rhs, _k); + VERIFY(m_util.is_numeral(rhs, _k)); inf_numeral k(_k); atom * a = alloc(atom, bv, v, k, kind); mk_bound_axioms(a); @@ -1315,7 +1315,8 @@ namespace smt { m_assume_eq_head(0), m_nl_rounds(0), m_nl_gb_exhausted(false), - m_nl_new_exprs(m) { + m_nl_new_exprs(m), + m_bound_watch(null_bool_var) { } template @@ -1980,7 +1981,7 @@ namespace smt { tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";); antecedents& ante = get_antecedents(); explain_bound(r, idx, !is_below, delta, ante); - b->push_justification(ante, numeral(1), proofs_enabled()); + b->push_justification(ante, numeral(1), coeffs_enabled()); set_conflict(ante.lits().size(), ante.lits().c_ptr(), @@ -2123,8 +2124,8 @@ namespace smt { void theory_arith::sign_bound_conflict(bound * b1, bound * b2) { SASSERT(b1->get_var() == b2->get_var()); antecedents& ante = get_antecedents(); - b1->push_justification(ante, numeral(1), proofs_enabled()); - b2->push_justification(ante, numeral(1), proofs_enabled()); + b1->push_justification(ante, numeral(1), coeffs_enabled()); + b2->push_justification(ante, numeral(1), coeffs_enabled()); set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas"); TRACE("arith_conflict", tout << "bound conflict\n";); @@ -2383,7 +2384,7 @@ namespace smt { if (!b->has_justification()) continue; if (!relax_bounds() || delta.is_zero()) { - b->push_justification(ante, it->m_coeff, proofs_enabled()); + b->push_justification(ante, it->m_coeff, coeffs_enabled()); continue; } numeral coeff = it->m_coeff; @@ -2445,7 +2446,7 @@ namespace smt { SASSERT(!is_b_lower || k_2 <= k_1); SASSERT(is_b_lower || k_2 >= k_1); if (new_atom == 0) { - b->push_justification(ante, coeff, proofs_enabled()); + b->push_justification(ante, coeff, coeffs_enabled()); continue; } SASSERT(!is_b_lower || k_2 < k_1); @@ -2459,7 +2460,7 @@ namespace smt { delta -= coeff*(k_2 - k_1); } TRACE("propagate_bounds", tout << "delta (after replace): " << delta << "\n";); - new_atom->push_justification(ante, coeff, proofs_enabled()); + new_atom->push_justification(ante, coeff, coeffs_enabled()); SASSERT(delta >= inf_numeral::zero()); } } @@ -2659,13 +2660,13 @@ namespace smt { for (unsigned i = 0; i < num_literals; i++) { ctx.display_detailed_literal(tout, lits[i]); tout << " "; - if (proofs_enabled()) { + if (coeffs_enabled()) { tout << "bound: " << bounds.lit_coeffs()[i] << "\n"; } } for (unsigned i = 0; i < num_eqs; i++) { tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " "; - if (proofs_enabled()) { + if (coeffs_enabled()) { tout << "bound: " << bounds.eq_coeffs()[i] << "\n"; } } @@ -2673,6 +2674,7 @@ namespace smt { tout << bounds.params(proof_rule)[i] << "\n"; } tout << "\n";); + record_conflict(num_literals, lits, num_eqs, eqs, bounds.num_params(), bounds.params(proof_rule)); ctx.set_conflict( ctx.mk_justification( ext_theory_conflict_justification(get_id(), r, num_literals, lits, num_eqs, eqs, @@ -2689,8 +2691,8 @@ namespace smt { typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { if (!it->is_dead() && is_fixed(it->m_var)) { - lower(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled()); - upper(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled()); + lower(it->m_var)->push_justification(antecedents, it->m_coeff, coeffs_enabled()); + upper(it->m_var)->push_justification(antecedents, it->m_coeff, coeffs_enabled()); } } } diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index e0ecc087a..a80f55de8 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -525,7 +525,7 @@ namespace smt { } // k += new_a_ij * lower_bound(x_j).get_rational(); k.addmul(new_a_ij, lower_bound(x_j).get_rational()); - lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled()); + lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); } else { SASSERT(at_upper(x_j)); @@ -541,7 +541,7 @@ namespace smt { } // k += new_a_ij * upper_bound(x_j).get_rational(); k.addmul(new_a_ij, upper_bound(x_j).get_rational()); - upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled()); + upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); } pol.push_back(row_entry(new_a_ij, x_j)); } @@ -566,7 +566,7 @@ namespace smt { } // k += new_a_ij * lower_bound(x_j).get_rational(); k.addmul(new_a_ij, lower_bound(x_j).get_rational()); - lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled()); + lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); } else { SASSERT(at_upper(x_j)); @@ -579,7 +579,7 @@ namespace smt { new_a_ij.neg(); // the upper terms are inverted // k += new_a_ij * upper_bound(x_j).get_rational(); k.addmul(new_a_ij, upper_bound(x_j).get_rational()); - upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled()); + upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled()); } TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";); pol.push_back(row_entry(new_a_ij, x_j)); @@ -772,8 +772,8 @@ namespace smt { // u += ncoeff * lower_bound(v).get_rational(); u.addmul(ncoeff, lower_bound(v).get_rational()); } - lower(v)->push_justification(ante, numeral::zero(), proofs_enabled()); - upper(v)->push_justification(ante, numeral::zero(), proofs_enabled()); + lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); + upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); } else if (gcds.is_zero()) { gcds = abs_ncoeff; diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index ecb512bda..9cc01e260 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -311,9 +311,8 @@ namespace smt { // // ----------------------------------- - virtual bool maximize(theory_var v); + virtual inf_eps_rational maximize(theory_var v); virtual theory_var add_objective(app* term); - virtual inf_eps_rational get_objective_value(theory_var v); virtual expr* block_lower_bound(theory_var v, inf_rational const& val); bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 98bd2268e..e6e3e94ca 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1001,7 +1001,7 @@ void theory_diff_logic::get_implied_bound_antecedents(edge_id bridge_edge, } template -bool theory_diff_logic::maximize(theory_var v) { +inf_eps_rational theory_diff_logic::maximize(theory_var v) { objective_term const& objective = m_objectives[v]; IF_VERBOSE(1, @@ -1029,12 +1029,14 @@ bool theory_diff_logic::maximize(theory_var v) { for (unsigned i = 0; i < potentials.size(); ++i) { tout << "v" << i << " -> " << potentials[i] << "\n"; }); - + rational r = m_objective_value.get_rational().to_rational(); + rational i = m_objective_value.get_infinitesimal().to_rational(); + return inf_eps_rational(inf_rational(r, i)); } else { std::cout << "Unbounded objective" << std::endl; + return inf_eps_rational::infinity(); } - return is_optimal; } template @@ -1054,13 +1056,6 @@ theory_var theory_diff_logic::add_objective(app* term) { return result; } -template -inf_eps_rational theory_diff_logic::get_objective_value(theory_var v) { - rational r = m_objective_value.get_rational().to_rational(); - rational i = m_objective_value.get_infinitesimal().to_rational(); - return inf_eps_rational(inf_rational(r, i)); -} - template expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const& val) { ast_manager& m = get_manager(); diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index d57875712..774e4abd1 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -28,15 +28,9 @@ namespace smt { class theory_opt { public: typedef inf_eps_rational inf_eps; - virtual bool maximize(theory_var v) { UNREACHABLE(); return false; }; + virtual inf_eps_rational maximize(theory_var v) { UNREACHABLE(); return inf_eps::infinity(); } virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } - virtual inf_eps get_objective_value(theory_var v) { - UNREACHABLE(); - return inf_eps(rational(1), inf_rational(0)); - } virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; } - - }; } diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index d7fdaf4fc..268bb8109 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -155,6 +155,11 @@ class inf_eps_rational { return inf_eps_rational(Numeral::minus_one()); } + static inf_eps_rational infinity() { + return inf_eps_rational(rational::one(), Numeral::zero()); + } + + inf_eps_rational & operator=(const inf_eps_rational & r) { m_infty = r.m_infty; m_r = r.m_r; @@ -179,6 +184,16 @@ class inf_eps_rational { return *this; } + inf_eps_rational & operator-=(const inf_rational & r) { + m_r -= r; + return *this; + } + + inf_eps_rational & operator+=(const inf_rational & r) { + m_r += r; + return *this; + } + inf_eps_rational & operator+=(const rational & r) { m_r += r; return *this;