From c75fd02c954e50259f48d67a4da6040a75db6d9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Apr 2016 21:31:16 -0700 Subject: [PATCH] qsat-opt Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 16 ++--- src/opt/opt_context.cpp | 39 +++++++++++ src/opt/opt_context.h | 5 +- src/qe/qe_arith.cpp | 100 +++++++++++++++++++++++++-- src/qe/qsat.cpp | 18 +---- 5 files changed, 145 insertions(+), 33 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index f56f327d4..ff6ecf1cd 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -105,13 +105,10 @@ namespace opt { var v = objective().m_vars.back(); unsigned x = v.m_id; rational const& coeff = v.m_coeff; - rational const& x_val = m_var2value[x]; - unsigned_vector const& row_ids = m_var2row_ids[x]; unsigned bound_row_index; rational bound_coeff; other.reset(); if (find_bound(x, bound_row_index, bound_coeff, other, coeff.is_pos())) { - row& r = m_rows[bound_row_index]; SASSERT(!bound_coeff.is_zero()); for (unsigned i = 0; i < other.size(); ++i) { resolve(bound_row_index, bound_coeff, other[i], x); @@ -150,7 +147,7 @@ namespace opt { if (a.is_zero()) { // skip } - else if (a.is_pos() == is_pos) { + else if (a.is_pos() == is_pos || r.m_type == t_eq) { rational value = x_val - (r.m_value/a); if (bound_row_index == UINT_MAX) { lub_val = value; @@ -221,6 +218,7 @@ namespace opt { SASSERT(a1 == get_coefficient(row_id1, x)); SASSERT(!a1.is_zero()); + // // row1 is of the form a1*x + t1 <~ 0 // row2 is of the form a2*x + t2 <~ 0 // assume that a1, a2 have the same sign. @@ -229,20 +227,22 @@ namespace opt { // t1 - a1*t2/a2 <~~ 0 // where <~~ is strict if either <~1 or <~2 is strict. // if a1 is negative, then .... - // - if (!m_rows[row_id2].m_alive) { + // + + row& row2 = m_rows[row_id2]; + if (!row2.m_alive) { return false; } rational a2 = get_coefficient(row_id2, x); if (a2.is_zero()) { return false; } - if (a1.is_pos() == a2.is_pos()) { + if (a1.is_pos() == a2.is_pos() || row2.m_type == t_eq) { mul_add(row_id2, -a2/a1, row_id1); return true; } else { - m_rows[row_id2].m_alive = false; + row2.m_alive = false; return false; } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b4dbb3dd5..8757232d3 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -42,6 +42,7 @@ Notes: #include "filter_model_converter.h" #include "ast_pp_util.h" #include "inc_sat_solver.h" +#include "qsat.h" namespace opt { @@ -1439,4 +1440,42 @@ namespace opt { } } } + + bool context::is_qsat_opt() { + if (m_objectives.size() != 1) { + return false; + } + if (m_objectives[0].m_type != O_MAXIMIZE && + m_objectives[0].m_type != O_MINIMIZE) { + return false; + } + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + if (has_quantifiers(m_hard_constraints[i].get())) { + return true; + } + } + return false; + } + + 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; + } + } + return l_undef; + } } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index e427a487f..b7dceb674 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -289,12 +289,15 @@ namespace opt { void display_benchmark(); - // pareto void yield(); expr_ref mk_ge(expr* t, expr* s); expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj); + + // quantifiers + bool is_qsat_opt(); + lbool run_qsat_opt(); }; } diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index f1637dfb7..3a0d0bbac 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -28,6 +28,7 @@ Revision History: #include "expr_functors.h" #include "model_v2_pp.h" #include "expr_safe_replace.h" +#include "model_based_opt.h" namespace qe { @@ -98,6 +99,55 @@ namespace qe { } } + void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map& tids) { + obj_map ts; + rational c(0), mul(1); + expr_ref t(m); + opt::ineq_type ty = opt::t_le; + expr* e1, *e2; + bool is_not = m.is_not(lit, lit); + if (is_not) { + mul.neg(); + } + SASSERT(!m.is_not(lit)); + if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { + if (is_not) mul.neg(); + linearize(model, mul, e1, c, ts); + linearize(model, -mul, e2, c, ts); + ty = is_not ? opt::t_lt : opt::t_le; + } + else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { + if (is_not) mul.neg(); + linearize(model, mul, e1, c, ts); + linearize(model, -mul, e2, c, ts); + ty = is_not ? opt::t_le: opt::t_lt; + } + else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) { + linearize(model, mul, e1, c, ts); + linearize(model, -mul, e2, c, ts); + ty = opt::t_eq; + } + else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) { + UNREACHABLE(); + } + else if (m.is_distinct(lit) && is_not && is_arith(to_app(lit)->get_arg(0))) { + UNREACHABLE(); + } + else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) { + UNREACHABLE(); + } + else { + return; + } + if (ty == opt::t_lt && is_int()) { + c += rational(1); + ty = opt::t_le; + } + vars coeffs; + extract_coefficients(ts, tids, coeffs); + mbo.add_constraint(coeffs, c, ty); + } + void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map& ts) { expr* t1, *t2, *t3; rational mul1; @@ -913,18 +963,54 @@ namespace qe { return true; } + 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::model_based_opt mbo; + obj_map ts; + obj_map tids; + vars coeffs; rational c(0), mul(1); linearize(mdl, mul, t, c, ts); - - // TBD: - // pick variables one by one from ts. - // m_var = alloc(contains_app, m, v); - // perform upper or lower projection depending on sign of v. - // - return opt::unbounded; + 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: + 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 result; } + + void extract_coefficients(obj_map const& ts, obj_map& tids, vars& coeffs) { + coeffs.reset(); + obj_map::iterator it = ts.begin(), end = ts.end(); + for (; it != end; ++it) { + unsigned id; + if (!tids.find(it->m_key, id)) { + id = tids.size(); + tids.insert(it->m_key, id); + } + coeffs.push_back(var(id, it->m_value)); + } + } + }; arith_project_plugin::arith_project_plugin(ast_manager& m) { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index a220cf268..76cf62aa5 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1326,25 +1326,9 @@ namespace qe { void maximize(expr_ref_vector const& core, model& mdl) { TRACE("qe", tout << "maximize: " << core << "\n";); m_was_sat |= !core.empty(); - if (core.empty()) { - m_ex.assert_expr(m.mk_false()); - m_fa.assert_expr(m.mk_false()); - return; - } expr_ref bound(m); m_bound = m_mbp.maximize(core, mdl, m_objective, m_value, bound); - switch (m_bound) { - case opt::unbounded: - m_ex.assert_expr(m.mk_false()); - m_fa.assert_expr(m.mk_false()); - break; - case opt::strict: - m_ex.assert_expr(bound); - break; - case opt::non_strict: - m_ex.assert_expr(bound); - break; - } + m_ex.assert_expr(bound); } };