From 2428bf18f11e25490b45f11826544485a30b7a33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Apr 2016 19:08:10 -0700 Subject: [PATCH] add model correction Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 79 +++++++++++++++++++++++++--- src/math/simplex/model_based_opt.h | 16 ++++-- src/opt/opt_context.cpp | 31 +++++------ src/opt/optsmt.h | 3 ++ src/qe/qe_arith.cpp | 56 +++++++++++++------- src/qe/qe_arith.h | 5 +- src/qe/qe_mbp.cpp | 8 +-- src/qe/qe_mbp.h | 2 +- src/qe/qsat.cpp | 18 +++---- src/qe/qsat.h | 2 +- src/util/inf_eps_rational.h | 1 + 11 files changed, 156 insertions(+), 65 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index ff6ecf1cd..989db2cad 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -97,9 +97,10 @@ namespace opt { // e.g. t2/a2 >= t3/a3 // then replace a3*x + t3 by t3/a3 - t2/a2 <= 0 // - bound_type model_based_opt::maximize(rational& value) { + inf_eps model_based_opt::maximize() { SASSERT(invariant()); unsigned_vector other; + unsigned_vector bound_trail, bound_vars; while (!objective().m_vars.empty()) { TRACE("opt", tout << "tableau\n";); var v = objective().m_vars.back(); @@ -120,17 +121,79 @@ namespace opt { mul_add(m_objective_id, - coeff/bound_coeff, bound_row_index); m_rows[bound_row_index].m_alive = false; + bound_trail.push_back(bound_row_index); + bound_vars.push_back(x); } else { - return unbounded; + return inf_eps::infinity(); } } - value = objective().m_value; - if (objective().m_type == t_lt) { - return strict; + // + // update the evaluation of variables to satisfy the bound. + + update_values(bound_vars, bound_trail); + + rational value = objective().m_value; + if (objective().m_type == t_lt) { + return inf_eps(inf_rational(value, rational(-1))); } else { - return non_strict; + return inf_eps(inf_rational(value)); + } + } + + + void model_based_opt::update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail) { + rational eps(0); + for (unsigned i = bound_trail.size(); i > 0; ) { + --i; + unsigned x = bound_vars[i]; + row const& r = m_rows[bound_trail[i]]; + rational val = r.m_coeff; + rational x_coeff; + vector const& vars = r.m_vars; + for (unsigned j = 0; j < vars.size(); ++j) { + var const& v = vars[j]; + if (x = v.m_id) { + x_coeff = v.m_coeff; + } + else { + val += m_var2value[v.m_id]*v.m_coeff; + } + } + SASSERT(!x_coeff.is_zero()); + val /= -x_coeff; + // Adjust epsilon to be s + if (eps.is_zero() || (!val.is_zero() && eps > abs(val))) { + eps = abs(val)/rational(2); + } + if (eps.is_zero() || (!r.m_value.is_zero() && eps > abs(r.m_value))) { + eps = abs(r.m_value)/rational(2); + } + // + // + // ax + t < 0 + // <=> x < -t/a + // <=> x := -t/a - epsilon + // + if (x_coeff.is_pos() && r.m_type == t_lt) { + val -= eps; + } + // + // -ax + t < 0 + // <=> -ax < -t + // <=> -x < -t/a + // <=> x > t/a + // <=> x := t/a + epsilon + // + + if (x_coeff.is_pos() && r.m_type == t_lt) { + val -= eps; + } + else if (x_coeff.is_neg() && r.m_type == t_lt) { + val += eps; + } + m_var2value[x] = val; } } @@ -343,6 +406,10 @@ namespace opt { return v; } + rational model_based_opt::get_value(unsigned var) { + return m_var2value[var]; + } + void model_based_opt::set_row(unsigned row_id, vector const& coeffs, rational const& c, ineq_type rel) { row& r = m_rows[row_id]; rational val(c); diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index 6a348ff31..8a1694059 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -23,6 +23,7 @@ Revision History: #include "util.h" #include "rational.h" +#include"inf_eps_rational.h" namespace opt { @@ -38,7 +39,7 @@ namespace opt { non_strict }; - + typedef inf_eps_rational inf_eps; class model_based_opt { public: @@ -71,8 +72,7 @@ namespace opt { bool invariant(); bool invariant(unsigned index, row const& r); - row& objective() { return m_rows[0]; } - + row& objective() { return m_rows[0]; } bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, unsigned_vector& other, bool is_pos); @@ -83,6 +83,8 @@ namespace opt { void mul_add(unsigned row_id1, rational const& c, unsigned row_id2); void set_row(unsigned row_id, vector const& coeffs, rational const& c, ineq_type rel); + + void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail); public: @@ -91,6 +93,9 @@ namespace opt { // add a fresh variable with value 'value'. unsigned add_var(rational const& value); + // retrieve updated value of variable. + rational get_value(unsigned var_id); + // add a constraint. We assume that the constraint is // satisfied under the values provided to the variables. void add_constraint(vector const& coeffs, rational const& c, ineq_type r); @@ -98,12 +103,13 @@ namespace opt { // Set the objective function (linear). void set_objective(vector const& coeffs, rational const& c); + // // find a maximal value for the objective function over the current values. // in other words, the returned maximal value may not be globally optimal, // but the current evaluation of variables are used to select a local // optimal. - bound_type maximize(rational& value); - + // + inf_eps maximize(); void display(std::ostream& out) const; void display(std::ostream& out, row const& r) const; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8757232d3..c96ba563a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1459,23 +1459,20 @@ namespace opt { lbool context::run_qsat_opt() { SASSERT(is_qsat_opt()); - app_ref objective(m); - opt::bound_type bound; - expr_ref value(m); - lbool result = qe::maximize(m_hard_constraints, objective, value, bound, m_params); - if (result != l_undef) { - switch (bound) { - case opt::unbounded: - case opt::strict: - case opt::non_strict: - // set_max - break; - // TBD: - - default: - break; - } + objective const& obj = m_objectives[0]; + app_ref term(obj.m_term); + if (obj.m_type == O_MINIMIZE) { + term = m_arith.mk_uminus(term); } - return l_undef; + inf_eps value; + lbool result = qe::maximize(m_hard_constraints, term, value, m_params); + if (result != l_undef && obj.m_type == O_MINIMIZE) { + value.neg(); + } + if (result != l_undef) { + m_optsmt.update_lower(obj.m_index, value); + m_optsmt.update_upper(obj.m_index, value); + } + return result; } } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index d11b84370..e01c58681 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -61,7 +61,9 @@ namespace opt { void get_model(model_ref& mdl, svector& labels); model* get_model(unsigned index) const { return m_models[index]; } + void update_lower(unsigned idx, inf_eps const& r); + void update_upper(unsigned idx, inf_eps const& r); void reset(); @@ -82,6 +84,7 @@ namespace opt { lbool update_upper(); + }; }; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 3a0d0bbac..243b3dce6 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -965,37 +965,57 @@ namespace qe { typedef opt::model_based_opt::var var; typedef vector vars; + - opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { opt::model_based_opt mbo; - + opt::inf_eps value; obj_map ts; obj_map tids; vars coeffs; rational c(0), mul(1); - linearize(mdl, mul, t, c, ts); + linearize(mdl, mul, t, c, ts); extract_coefficients(ts, tids, coeffs); mbo.set_objective(coeffs, c); for (unsigned i = 0; i < fmls.size(); ++i) { linearize(mdl, mbo, fmls[i], tids); } + - rational val; - opt::bound_type result = mbo.maximize(val); - value = a.mk_numeral(val, false); - switch (result) { - case opt::unbounded: + value = mbo.maximize(); + + + + expr_ref val(a.mk_numeral(value.get_rational(), false), m); + if (!value.is_finite()) { bound = m.mk_false(); - break; - case opt::strict: - bound = a.mk_le(value, t); - break; - case opt::non_strict: - bound = a.mk_lt(value, t); - break; + return value; + } + + // update model + ptr_vector vars; + obj_map::iterator it = tids.begin(), end = tids.end(); + for (; it != end; ++it) { + expr* e = it->m_key; + if (is_uninterp_const(e)) { + unsigned id = it->m_value; + func_decl* f = to_app(e)->get_decl(); + expr_ref val(a.mk_numeral(mbo.get_value(id), false), m); + mdl.register_decl(f, val); + } + else { + TRACE("qe", tout << "omitting model update for non-uninterpreted constant " << mk_pp(e, m) << "\n";); + } + } + + if (value.get_infinitesimal().is_neg()) { + bound = a.mk_le(val, t); + } + else { + bound = a.mk_lt(val, t); } - return result; + return value; } void extract_coefficients(obj_map const& ts, obj_map& tids, vars& coeffs) { @@ -1033,8 +1053,8 @@ namespace qe { return m_imp->a.get_family_id(); } - opt::bound_type arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { - return m_imp->maximize(fmls, mdl, t, value, bound); + opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { + return m_imp->maximize(fmls, mdl, t, bound); } bool arith_project(model& model, app* var, expr_ref_vector& lits) { diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index f79a61245..b89d16d04 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -22,14 +22,15 @@ namespace qe { class arith_project_plugin : public project_plugin { struct imp; - imp* m_imp; + imp* m_imp; public: arith_project_plugin(ast_manager& m); virtual ~arith_project_plugin(); virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits); virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits); virtual family_id get_family_id(); - opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound); + + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound); }; bool arith_project(model& model, app* var, expr_ref_vector& lits); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index c592445ea..7d5f3800e 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -213,9 +213,9 @@ class mbp::impl { public: - opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { arith_project_plugin arith(m); - return arith.maximize(fmls, mdl, t, value, bound); + return arith.maximize(fmls, mdl, t, bound); } void extract_literals(model& model, expr_ref_vector& fmls) { @@ -421,6 +421,6 @@ void mbp::extract_literals(model& model, expr_ref_vector& lits) { m_impl->extract_literals(model, lits); } -opt::bound_type mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { - return m_impl->maximize(fmls, mdl, t, value, bound); +opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { + return m_impl->maximize(fmls, mdl, t, bound); } diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 4081288b4..332659c0b 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -76,7 +76,7 @@ namespace qe { \brief Maximize objective t under current model for constraints in fmls. */ - opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound); + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound); }; } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 76cf62aa5..03d8987cf 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1162,8 +1162,7 @@ namespace qe { m_level(0), m_mode(mode), m_avars(m), - m_free_vars(m), - m_value(m) + m_free_vars(m) { reset(); } @@ -1283,17 +1282,15 @@ namespace qe { } app* m_objective; - expr_ref m_value; - opt::bound_type m_bound; + opt::inf_eps m_value; bool m_was_sat; - lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound) { + lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value) { expr_ref_vector defs(m); expr_ref fml = negate_core(fmls); hoist(fml); m_objective = t; - m_value = 0; - m_bound = opt::unbounded; + m_value = opt::inf_eps(); m_was_sat = false; m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); @@ -1319,7 +1316,6 @@ namespace qe { throw tactic_exception(s.c_str()); } value = m_value; - bound = m_bound; return l_true; } @@ -1327,16 +1323,16 @@ namespace qe { TRACE("qe", tout << "maximize: " << core << "\n";); m_was_sat |= !core.empty(); expr_ref bound(m); - m_bound = m_mbp.maximize(core, mdl, m_objective, m_value, bound); + m_value = m_mbp.maximize(core, mdl, m_objective, bound); m_ex.assert_expr(bound); } }; - lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p) { + lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p) { ast_manager& m = fmls.get_manager(); qsat qs(m, p, qsat_maximize); - return qs.maximize(fmls, t, value, bound); + return qs.maximize(fmls, t, value); } }; diff --git a/src/qe/qsat.h b/src/qe/qsat.h index fd10e3e75..08a2cbd53 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -114,7 +114,7 @@ namespace qe { void collect_statistics(statistics& st) const; }; - lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p); + lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p); } diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index 4327b47c0..048b6f383 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -23,6 +23,7 @@ Revision History: #include"debug.h" #include"vector.h" #include"rational.h" +#include"inf_rational.h" template class inf_eps_rational {