From 72e82532b2495cb51938b104fc830e3f2867e793 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 31 Oct 2013 09:43:15 -0700 Subject: [PATCH] enabling upper bound test Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 6 +++- src/opt/opt_solver.h | 1 - src/opt/optimize_objectives.cpp | 63 +++++++++++++++++++++++---------- src/opt/optimize_objectives.h | 1 + src/smt/theory_arith.h | 8 ++--- src/smt/theory_arith_aux.h | 36 +++++++++---------- src/smt/theory_arith_core.h | 8 ++--- src/smt/theory_arith_pp.h | 2 +- src/smt/theory_opt.h | 8 +++-- 9 files changed, 82 insertions(+), 51 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 64d8a32be..515edcbff 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -77,6 +77,9 @@ namespace opt { else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) { return dynamic_cast(*arith_theory); } + else if (typeid(smt::theory_inf_arith) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } else if (typeid(smt::theory_rdl&) == typeid(*arith_theory)) { return dynamic_cast(*arith_theory); } @@ -172,7 +175,8 @@ namespace opt { return expr_ref(m.mk_true(), m); } else { - return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], val.get_numeral()), m); + inf_rational n = val.get_numeral(); + return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], n), m); } } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 3c149aefd..4afa65f31 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -91,7 +91,6 @@ namespace opt { smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat. - private: smt::theory_opt& get_optimizer(); }; } diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 8e111953e..086c52bf4 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -66,24 +66,16 @@ namespace opt { */ lbool optimize_objectives::basic_opt(app_ref_vector& objectives) { arith_util autil(m); - s->reset_objectives(); - m_lower.reset(); - m_upper.reset(); - // First check_sat call to initialize theories - lbool is_sat = s->check_sat(0, 0); - if (is_sat != l_true) { - return is_sat; - } opt_solver::scoped_push _push(*s); opt_solver::toggle_objective _t(*s, true); for (unsigned i = 0; i < objectives.size(); ++i) { - s->add_objective(objectives[i].get()); - m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); - m_upper.push_back(inf_eps(rational(1), inf_rational(0))); + m_vars.push_back(s->add_objective(objectives[i].get())); } - + + lbool is_sat = l_true; + // ready to test: is_sat = update_upper(); while (is_sat == l_true && !m_cancel) { is_sat = update_lower(); } @@ -117,8 +109,31 @@ namespace opt { } lbool optimize_objectives::update_upper() { - NOT_IMPLEMENTED_YET(); - return l_undef; + smt::theory_opt& opt = s->get_optimizer(); + + if (typeid(smt::theory_inf_arith) != typeid(opt)) { + return l_true; + } + smt::theory_inf_arith& th = dynamic_cast(opt); + + expr_ref bound(m); + lbool is_sat = l_true; + + for (unsigned i = 0; i < m_lower.size(); ++i) { + if (m_lower[i] < m_upper[i]) { + opt_solver::scoped_push _push(*s); + smt::theory_var v = m_vars[i]; + bound = th.block_upper_bound(v, m_upper[i]); + expr* bounds[1] = { bound }; + is_sat = s->check_sat(1, bounds); + if (is_sat) { + IF_VERBOSE(1, verbose_stream() << "Setting lower bound for " << v << " to " << m_upper[i] << "\n";); + m_lower[i] = m_upper[i]; + } + // else: TBD extract Farkas coefficients. + } + } + return l_true; } /** @@ -127,10 +142,22 @@ namespace opt { */ lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector& values) { s = &solver; - lbool result = basic_opt(objectives); - values.reset(); - values.append(m_lower); - return result; + s->reset_objectives(); + m_lower.reset(); + m_upper.reset(); + for (unsigned i = 0; i < objectives.size(); ++i) { + m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); + m_upper.push_back(inf_eps(rational(1), inf_rational(0))); + } + + // 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); + values.reset(); + values.append(m_lower); + } + return is_sat; } } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index cb3176d0d..227cd8f00 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -33,6 +33,7 @@ namespace opt { volatile bool m_cancel; vector m_lower; vector m_upper; + svector m_vars; public: optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {} diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 75a0f9ff3..56c361a93 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -273,14 +273,14 @@ namespace smt { class atom : public bound { protected: bool_var m_bvar; - numeral m_k; + inf_numeral m_k; unsigned m_atom_kind:2; // atom kind unsigned m_is_true:1; // cache: true if the atom was assigned to true. public: - atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind); + atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind); atom_kind get_atom_kind() const { return static_cast(m_atom_kind); } virtual ~atom() {} - numeral const & get_k() const { return m_k; } + inf_numeral const & get_k() const { return m_k; } bool_var get_bool_var() const { return m_bvar; } bool is_true() const { return m_is_true; } void assign_eh(bool is_true, inf_numeral const & epsilon); @@ -999,7 +999,7 @@ namespace smt { 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); // ----------------------------------- // // Pretty Printing diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index a1fff392f..a84a9ebf9 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -367,7 +367,7 @@ namespace smt { // ----------------------------------- template - theory_arith::atom::atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind): + theory_arith::atom::atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind): bound(v, inf_numeral::zero(), B_LOWER, true), m_bvar(bv), m_k(k), @@ -997,6 +997,22 @@ namespace smt { } } + template + expr* theory_arith::block_upper_bound(theory_var v, inf_numeral const& val) { + ast_manager& m = get_manager(); + context& ctx = get_context(); + std::ostringstream strm; + strm << val << " <= " << v; + expr* b = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); + bool_var bv = ctx.mk_bool_var(b); + 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); + return b; + } + template inf_eps_rational theory_arith::get_objective_value(theory_var v) { return m_objective_value; @@ -1117,15 +1133,6 @@ namespace smt { ); pivot(x_i, x_j, a_ij, false); - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; - if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; - if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; - tout << "value x_i: " << get_value(x_i) << "\n"; - if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; - if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; - tout << "value x_j: " << get_value(x_j) << "\n"; - - ); SASSERT(is_non_base(x_i)); SASSERT(is_base(x_j)); @@ -1137,15 +1144,6 @@ namespace smt { move_xi_to_lower = a_ij.is_neg(); move_to_bound(x_i, move_xi_to_lower); - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; - if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; - if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; - tout << "value x_i: " << get_value(x_i) << "\n"; - if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; - if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; - tout << "value x_j: " << get_value(x_j) << "\n"; - ); - row & r2 = m_rows[get_var_row(x_j)]; coeff.neg(); add_tmp_row(r, coeff, r2); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 195d78e25..11484c779 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -801,7 +801,7 @@ namespace smt { void theory_arith::mk_bound_axioms(atom * a1) { theory_var v = a1->get_var(); literal l1(a1->get_bool_var()); - numeral const & k1(a1->get_k()); + inf_numeral const & k1(a1->get_k()); atom_kind kind1 = a1->get_atom_kind(); TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";); atoms & occs = m_var_occs[v]; @@ -810,7 +810,7 @@ namespace smt { for (; it != end; ++it) { atom * a2 = *it; literal l2(a2->get_bool_var()); - numeral const & k2 = a2->get_k(); + inf_numeral const & k2 = a2->get_k(); atom_kind kind2 = a2->get_atom_kind(); SASSERT(k1 != k2 || kind1 != kind2); SASSERT(a2->get_var() == v); @@ -880,7 +880,7 @@ namespace smt { ctx.set_var_theory(bv, get_id()); rational _k; m_util.is_numeral(rhs, _k); - numeral k(_k); + inf_numeral k(_k); atom * a = alloc(atom, bv, v, k, kind); mk_bound_axioms(a); m_unassigned_atoms[v]++; @@ -2475,7 +2475,7 @@ namespace smt { bool_var bv = a->get_bool_var(); literal l(bv); if (get_context().get_assignment(bv) == l_undef) { - numeral const & k2 = a->get_k(); + inf_numeral const & k2 = a->get_k(); delta.reset(); if (a->get_atom_kind() == A_LOWER) { // v >= k k >= k2 |- v >= k2 diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 274cd5499..4eeb6a189 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -428,7 +428,7 @@ namespace smt { template void theory_arith::display_atom(std::ostream & out, atom * a, bool show_sign) const { theory_var v = a->get_var(); - numeral const & k = a->get_k(); + inf_numeral const & k = a->get_k(); enode * e = get_enode(v); if (show_sign) { if (!a->is_true()) diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index f1c6c242d..d57875712 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -27,14 +27,16 @@ Notes: namespace smt { class theory_opt { public: + typedef inf_eps_rational inf_eps; virtual bool maximize(theory_var v) { UNREACHABLE(); return false; }; virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } - virtual inf_eps_rational get_objective_value(theory_var v) { + virtual inf_eps get_objective_value(theory_var v) { UNREACHABLE(); - inf_eps_rational r(rational(1), inf_rational(0)); - return r; + return inf_eps(rational(1), inf_rational(0)); } virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; } + + }; }