From 339cd6e537813ff2ea07293e099784ed680f1769 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 May 2016 13:45:50 -0700 Subject: [PATCH] mbo Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 130 ++++++++++++++++++++++++++- src/math/simplex/model_based_opt.h | 21 ++++- src/qe/qe_arith.cpp | 6 +- src/qe/qe_mbp.cpp | 92 +++++++++++++++++-- src/qe/qe_mbp.h | 1 + src/qe/qsat.cpp | 3 +- src/smt/theory_pb.cpp | 8 +- src/test/model_based_opt.cpp | 75 ++++++++++++++++ 8 files changed, 317 insertions(+), 19 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index e5db201a8..06ba38b4a 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -34,8 +34,7 @@ std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) { namespace opt { - model_based_opt::model_based_opt(): - m_objective_id(0) + model_based_opt::model_based_opt() { m_rows.push_back(row()); } @@ -448,5 +447,132 @@ namespace opt { set_row(m_objective_id, coeffs, c, t_le); } + void model_based_opt::get_live_rows(vector& rows) { + for (unsigned i = 0; i < m_rows.size(); ++i) { + if (m_rows[i].m_alive) { + rows.push_back(m_rows[i]); + } + } + } + + // + // pick glb and lub representative. + // The representative is picked such that it + // represents the fewest inequalities. + // The constraints that enforce a glb or lub are not forced. + // The constraints that separate the glb from ub or the lub from lb + // are not forced. + // In other words, suppose there are + // . N inequalities of the form t <= x + // . M inequalities of the form s >= x + // . t0 is glb among N under valuation. + // . s0 is lub among M under valuation. + // If N < M + // create the inequalities: + // t <= t0 for each t other than t0 (N-1 inequalities). + // t0 <= s for each s (M inequalities). + // If N >= M the construction is symmetric. + // + void model_based_opt::project(unsigned x) { + unsigned_vector& lub_rows = m_lub; + unsigned_vector& glb_rows = m_glb; + unsigned lub_index = UINT_MAX, glb_index = UINT_MAX; + bool lub_strict = false, glb_strict = false; + rational lub_val, glb_val; + rational const& x_val = m_var2value[x]; + unsigned_vector const& row_ids = m_var2row_ids[x]; + uint_set visited; + lub_rows.reset(); + glb_rows.reset(); + // select the lub and glb. + for (unsigned i = 0; i < row_ids.size(); ++i) { + unsigned row_id = row_ids[i]; + if (visited.contains(row_id)) { + continue; + } + visited.insert(row_id); + row& r = m_rows[row_id]; + if (!r.m_alive) { + continue; + } + rational a = get_coefficient(row_id, x); + if (a.is_zero()) { + continue; + } + if (r.m_type == t_eq) { + solve_for(row_id, x); + return; + } + if (a.is_pos()) { + rational lub_value = x_val - (r.m_value/a); + if (lub_rows.empty() || + lub_value < lub_val || + (lub_value == lub_val && r.m_type == t_lt && !lub_strict)) { + lub_val = lub_value; + lub_index = row_id; + lub_strict = r.m_type == t_lt; + } + lub_rows.push_back(row_id); + } + else { + SASSERT(a.is_neg()); + rational glb_value = x_val - (r.m_value/a); + if (glb_rows.empty() || + glb_value > glb_val || + (glb_value == glb_val && r.m_type == t_lt && !glb_strict)) { + glb_val = glb_value; + glb_index = row_id; + glb_strict = r.m_type == t_lt; + } + glb_rows.push_back(row_id); + } + } + unsigned row_index = (lub_rows.size() <= glb_rows.size())? lub_index : glb_index; + glb_rows.append(lub_rows); + if (row_index == UINT_MAX) { + for (unsigned i = 0; i < glb_rows.size(); ++i) { + unsigned row_id = glb_rows[i]; + SASSERT(m_rows[row_id].m_alive); + SASSERT(!get_coefficient(row_id, x).is_zero()); + m_rows[row_id].m_alive = false; + } + } + else { + rational coeff = get_coefficient(row_index, x); + for (unsigned i = 0; i < glb_rows.size(); ++i) { + unsigned row_id = glb_rows[i]; + if (row_id != row_index) { + resolve(row_index, coeff, row_id, x); + } + } + m_rows[row_index].m_alive = false; + } + } + + void model_based_opt::solve_for(unsigned row_id1, unsigned x) { + rational a = get_coefficient(row_id1, x); + row& r1 = m_rows[row_id1]; + SASSERT(!a.is_zero()); + SASSERT(r1.m_type == t_eq); + SASSERT(r1.m_alive); + unsigned_vector const& row_ids = m_var2row_ids[x]; + uint_set visited; + visited.insert(row_id1); + for (unsigned i = 0; i < row_ids.size(); ++i) { + unsigned row_id2 = row_ids[i]; + if (!visited.contains(row_id2)) { + visited.insert(row_id2); + resolve(row_id1, a, row_id2, x); + } + } + r1.m_alive = false; + } + + void model_based_opt::project(unsigned num_vars, unsigned const* vars) { + for (unsigned i = 0; i < num_vars; ++i) { + project(vars[i]); + } + } + } diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index b48a96edb..e4ba288c8 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -48,7 +48,6 @@ namespace opt { } }; }; - private: struct row { row(): m_type(t_le), m_value(0), m_alive(false) {} vector m_vars; // variables with coefficients @@ -58,11 +57,14 @@ namespace opt { bool m_alive; // rows can be marked dead if they have been processed. }; + private: + vector m_rows; - unsigned m_objective_id; + static const unsigned m_objective_id = 0; vector m_var2row_ids; vector m_var2value; vector m_new_vars; + unsigned_vector m_lub, m_glb; bool invariant(); bool invariant(unsigned index, row const& r); @@ -81,6 +83,10 @@ namespace opt { void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail); + void project(unsigned var); + + void solve_for(unsigned row_id, unsigned x); + public: model_based_opt(); @@ -106,6 +112,17 @@ namespace opt { // inf_eps maximize(); + + // + // Project set of variables from inequalities. + // + void project(unsigned num_vars, unsigned const* vars); + + // + // Extract current rows (after projection). + // + void get_live_rows(vector& rows); + void display(std::ostream& out) const; void display(std::ostream& out, row const& r) const; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 48dacdbf4..bdfd45133 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -29,6 +29,7 @@ Revision History: #include "expr_functors.h" #include "expr_safe_replace.h" #include "model_based_opt.h" +#include "model_evaluator.h" namespace qe { @@ -658,6 +659,9 @@ namespace qe { bool new_max = true; rational max_r, r; expr_ref val(m); + model_evaluator eval(mdl); + eval.set_model_completion(true); + bool is_int = a.is_int(m_var->x()); for (unsigned i = 0; i < num_ineqs(); ++i) { rational const& ac = m_ineq_coeffs[i]; @@ -669,7 +673,7 @@ namespace qe { // ac < 0: x + t/ac > 0 <=> x > max { - t/ac | ac < 0 } = max { t/|ac| | ac < 0 } // if (ac.is_pos() == do_pos) { - VERIFY(mdl.eval(ineq_term(i), val)); + eval(ineq_term(i), val); VERIFY(a.is_numeral(val, r)); r /= abs(ac); new_max = diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 7d5f3800e..d7ec22eee 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -28,10 +28,15 @@ Revision History: #include "th_rewriter.h" #include "model_v2_pp.h" #include "expr_functors.h" +#include "for_each_expr.h" using namespace qe; +struct noop_op_proc { + void operator()(expr*) {} +}; + /** \brief return two terms that are equal in the model. @@ -106,6 +111,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) { class mbp::impl { ast_manager& m; + th_rewriter m_rw; ptr_vector m_plugins; expr_mark m_visited; @@ -130,7 +136,6 @@ class mbp::impl { is_var.mark(vars[i].get()); } expr_ref tmp(m), t(m), v(m); - th_rewriter rw(m); for (unsigned i = 0; i < lits.size(); ++i) { expr* e = lits[i].get(), *l, *r; if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) { @@ -141,7 +146,7 @@ class mbp::impl { is_rem.mark(v); for (unsigned j = 0; j < lits.size(); ++j) { sub(lits[j].get(), tmp); - rw(tmp); + m_rw(tmp); lits[j] = tmp; } } @@ -177,6 +182,29 @@ class mbp::impl { } + void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) { + ast_manager& m = vars.get_manager(); + expr_mark lit_visited; + for_each_expr_proc fe; + for (unsigned i = 0; i < lits.size(); ++i) { + for_each_expr(fe, lit_visited, lits[i].get()); + } + unsigned j = 0; + for (unsigned i = 0; i < vars.size(); ++i) { + app* var = vars[i].get(); + if (lit_visited.is_marked(var)) { + if (i != j) { + vars[j] = vars[i].get(); + } + ++j; + } + } + if (vars.size() != j) { + vars.resize(j); + } + } + + void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) { TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";); ptr_vector todo; @@ -210,6 +238,42 @@ class mbp::impl { } } + void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + expr_safe_replace sub(m); + expr_ref val(m); + unsigned j = 0; + for (unsigned i = 0; i < vars.size(); ++i) { + app* var = vars[i].get(); + if (m.is_bool(var)) { + VERIFY(model.eval(var, val)); + sub.insert(var, val); + } + else { + if (j != i) { + vars[j] = vars[i].get(); + } + ++j; + } + } + if (j != vars.size()) { + vars.resize(j); + j = 0; + for (unsigned i = 0; i < fmls.size(); ++i) { + sub(fmls[i].get(), val); + m_rw(val); + if (!m.is_true(val)) { + if (j != i) { + fmls[j] = fmls[i].get(); + } + ++j; + } + } + if (j != fmls.size()) { + fmls.resize(j); + } + } + } + public: @@ -333,7 +397,7 @@ public: m_visited.reset(); } - impl(ast_manager& m):m(m) { + impl(ast_manager& m):m(m), m_rw(m) { add_plugin(alloc(arith_project_plugin, m)); add_plugin(alloc(datatype_project_plugin, m)); add_plugin(alloc(array_project_plugin, m)); @@ -359,14 +423,16 @@ public: void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { expr_ref val(m), tmp(m); app_ref var(m); - th_rewriter rw(m); + expr_ref_vector unused_fmls(m); bool progress = true; TRACE("qe", tout << vars << " " << fmls << "\n";); - while (progress && !vars.empty()) { - preprocess_solve(model, vars, fmls); + preprocess_solve(model, vars, fmls); + filter_variables(model, vars, fmls, unused_fmls); + project_bools(model, vars, fmls); + while (progress && !vars.empty() && !fmls.empty()) { app_ref_vector new_vars(m); progress = false; - while (!vars.empty()) { + while (!vars.empty() && !fmls.empty()) { var = vars.back(); vars.pop_back(); project_plugin* p = get_plugin(var); @@ -377,7 +443,7 @@ public: new_vars.push_back(var); } } - if (!progress && !new_vars.empty() && force_elim) { + if (!progress && !new_vars.empty() && !fmls.empty() && force_elim) { var = new_vars.back(); new_vars.pop_back(); expr_safe_replace sub(m); @@ -385,7 +451,7 @@ public: sub.insert(var, val); for (unsigned i = 0; i < fmls.size(); ++i) { sub(fmls[i].get(), tmp); - rw(tmp); + m_rw(tmp); if (m.is_true(tmp)) { project_plugin::erase(fmls, i); } @@ -396,9 +462,17 @@ public: progress = true; } vars.append(new_vars); + if (progress) { + preprocess_solve(model, vars, fmls); + } } + if (fmls.empty()) { + vars.reset(); + } + fmls.append(unused_fmls); TRACE("qe", tout << vars << " " << fmls << "\n";); } + }; mbp::mbp(ast_manager& m) { diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 332659c0b..7cf086824 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -37,6 +37,7 @@ namespace qe { virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0; virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0; virtual family_id get_family_id() = 0; + virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; static expr_ref pick_equality(ast_manager& m, model& model, expr* t); static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index fe11de199..0ab3c86bb 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -575,6 +575,7 @@ namespace qe { lbool check_sat() { while (true) { ++m_stats.m_num_rounds; + IF_VERBOSE(3, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";); check_cancel(); expr_ref_vector asms(m_asms); m_pred_abs.get_assumptions(m_model.get(), asms); @@ -1191,7 +1192,7 @@ namespace qe { lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) { expr_ref_vector defs(m); - expr_ref fml = negate_core(fmls); + expr_ref fml = mk_and(fmls); hoist(fml); m_objective = t; m_value = opt::inf_eps(); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 273bffd93..a85f9aa80 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1063,7 +1063,7 @@ namespace smt { } #endif else { - IF_VERBOSE(3, display(verbose_stream() << "no propagation ", c, true);); + IF_VERBOSE(14, display(verbose_stream() << "no propagation ", c, true);); } } @@ -1637,7 +1637,7 @@ namespace smt { // same order as the assignment stack. // It is not a correctness bug but causes to miss lemmas. // - IF_VERBOSE(2, display_resolved_lemma(verbose_stream());); + IF_VERBOSE(12, display_resolved_lemma(verbose_stream());); TRACE("pb", display_resolved_lemma(tout);); return false; } @@ -1735,12 +1735,12 @@ namespace smt { // 3x + 3y + z + u >= 4 // ~x /\ ~y => z + u >= - IF_VERBOSE(4, display(verbose_stream() << "lemma1: ", m_lemma);); + IF_VERBOSE(14, display(verbose_stream() << "lemma1: ", m_lemma);); hoist_maximal_values(); lbool is_true = m_lemma.normalize(false); m_lemma.prune(false); - IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma);); + IF_VERBOSE(14, display(verbose_stream() << "lemma2: ", m_lemma);); //unsigned l_size = m_ineq_literals.size() + ((is_true==l_false)?0:m_lemma.size()); //if (s_min_l_size >= l_size) { // verbose_stream() << "(pb.conflict min size: " << l_size << ")\n"; diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index 8c4148638..b5b8e2953 100644 --- a/src/test/model_based_opt.cpp +++ b/src/test/model_based_opt.cpp @@ -216,6 +216,77 @@ static void test4() { std::cout << "u: " << mbo.get_value(u) << "\n"; } +static void test5() { + opt::model_based_opt mbo; + unsigned x = mbo.add_var(rational(2)); + unsigned y = mbo.add_var(rational(3)); + unsigned z = mbo.add_var(rational(4)); + unsigned u = mbo.add_var(rational(5)); + + add_ineq(mbo, x, 1, y, -1, 0, opt::t_le); + add_ineq(mbo, x, 1, z, -1, 0, opt::t_le); + add_ineq(mbo, y, 1, u, -1, 0, opt::t_le); + add_ineq(mbo, z, 1, u, -1, 1, opt::t_le); + + unsigned vars[2] = { y, z }; + mbo.project(1, vars); + mbo.display(std::cout); + + mbo.project(1, vars); + mbo.display(std::cout); + + mbo.project(1, vars+1); + mbo.display(std::cout); + + vector rows; + mbo.get_live_rows(rows); +} + + +static void test6() { + opt::model_based_opt mbo; + unsigned x0 = mbo.add_var(rational(1)); + unsigned x = mbo.add_var(rational(2)); + unsigned y = mbo.add_var(rational(3)); + unsigned z = mbo.add_var(rational(4)); + unsigned u = mbo.add_var(rational(5)); + unsigned v = mbo.add_var(rational(6)); + unsigned w = mbo.add_var(rational(6)); + + add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le); + add_ineq(mbo, x, 1, y, -1, 0, opt::t_le); + add_ineq(mbo, y, 1, u, -1, 0, opt::t_le); + add_ineq(mbo, y, 1, z, -1, 1, opt::t_le); + add_ineq(mbo, y, 1, v, -1, 1, opt::t_le); + add_ineq(mbo, y, 1, w, -1, 1, opt::t_le); + + mbo.display(std::cout); + mbo.project(1, &y); + mbo.display(std::cout); +} + +static void test7() { + opt::model_based_opt mbo; + unsigned x0 = mbo.add_var(rational(2)); + unsigned x = mbo.add_var(rational(1)); + unsigned y = mbo.add_var(rational(3)); + unsigned z = mbo.add_var(rational(4)); + unsigned u = mbo.add_var(rational(5)); + unsigned v = mbo.add_var(rational(6)); + unsigned w = mbo.add_var(rational(6)); + + add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le); + add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt); + add_ineq(mbo, y, 1, u, -1, 0, opt::t_le); + add_ineq(mbo, y, 1, z, -1, 1, opt::t_le); + add_ineq(mbo, y, 1, v, -1, 1, opt::t_le); + add_ineq(mbo, y, 1, w, -1, 1, opt::t_lt); + + mbo.display(std::cout); + mbo.project(1, &y); + mbo.display(std::cout); +} + // test with mix of upper and lower bounds void tst_model_based_opt() { @@ -224,4 +295,8 @@ void tst_model_based_opt() { test2(); test3(); test4(); + test5(); + test6(); + test7(); + }