From 68c7d64d00e8c31eba34eecb5611fe104af31697 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Apr 2016 11:18:20 -0700 Subject: [PATCH] adding model-based opt facility Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/math/simplex/CMakeLists.txt | 1 + src/api/dotnet/ArithExpr.cs | 3 + src/api/dotnet/BoolExpr.cs | 4 +- src/math/simplex/model_based_opt.cpp | 307 ++++++++++++++++++ src/math/simplex/model_based_opt.h | 102 ++++++ src/qe/qe_arith.cpp | 245 +++----------- src/qe/qe_arith.h | 2 +- src/qe/qe_mbp.cpp | 4 +- src/qe/qe_mbp.h | 8 +- src/qe/qsat.cpp | 14 +- src/qe/qsat.h | 2 +- 11 files changed, 465 insertions(+), 227 deletions(-) create mode 100644 src/math/simplex/model_based_opt.cpp create mode 100644 src/math/simplex/model_based_opt.h diff --git a/contrib/cmake/src/math/simplex/CMakeLists.txt b/contrib/cmake/src/math/simplex/CMakeLists.txt index 6f965919d..de55f1634 100644 --- a/contrib/cmake/src/math/simplex/CMakeLists.txt +++ b/contrib/cmake/src/math/simplex/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(simplex SOURCES simplex.cpp + model_based_opt.cpp COMPONENT_DEPENDENCIES util ) diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs index 705a9f6ca..b6beaef0c 100644 --- a/src/api/dotnet/ArithExpr.cs +++ b/src/api/dotnet/ArithExpr.cs @@ -60,6 +60,9 @@ namespace Microsoft.Z3 /// Operator overloading for arithmetical operator public static ArithExpr operator /(double a, ArithExpr b) { return MkNum(b, a) / b; } + /// Operator overloading for arithmetical operator + public static ArithExpr operator -(ArithExpr a) { return a.Context.MkUnaryMinus(a); } + /// Operator overloading for arithmetical operator public static ArithExpr operator -(ArithExpr a, ArithExpr b) { return a.Context.MkSub(a, b); } diff --git a/src/api/dotnet/BoolExpr.cs b/src/api/dotnet/BoolExpr.cs index b25d99570..c52109352 100644 --- a/src/api/dotnet/BoolExpr.cs +++ b/src/api/dotnet/BoolExpr.cs @@ -39,9 +39,7 @@ namespace Microsoft.Z3 /// Disjunction of Boolean expressions public static BoolExpr operator|(BoolExpr a, BoolExpr b) { return a.Context.MkOr(a, b); } - /// - /// Conjunction of Boolean expressions - /// + /// Conjunction of Boolean expressions public static BoolExpr operator &(BoolExpr a, BoolExpr b) { return a.Context.MkAnd(a, b); } /// Xor of Boolean expressions diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp new file mode 100644 index 000000000..10008345a --- /dev/null +++ b/src/math/simplex/model_based_opt.cpp @@ -0,0 +1,307 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + model_based_opt.cpp + +Abstract: + + Model-based optimization for linear real arithmetic. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-27-4 + +Revision History: + + +--*/ + +#include "model_based_opt.h" + +namespace opt { + + + bool model_based_opt::invariant() { + // variables in each row are sorted. + for (unsigned i = 0; i < m_rows.size(); ++i) { + if (!invariant(m_rows[i])) { + return false; + } + } + return invariant(m_objective); + } + + bool model_based_opt::invariant(row const& r) { + rational val = r.m_coeff; + vector const& vars = r.m_vars; + for (unsigned i = 0; i < vars.size(); ++i) { + var const& v = vars[i]; + SASSERT(i + 1 == vars.size() || v.m_id < vars[i+1].m_id); + SASSERT(!v.m_coeff.is_zero()); + val += v.m_coeff * m_var2value[v.m_id]; + } + SASSERT(val == r.m_value); + SASSERT(r.m_type != t_eq || val.is_zero()); + SASSERT(r.m_type != t_lt || val.is_neg()); + SASSERT(r.m_type != t_le || !val.is_pos()); + return true; + } + + // a1*x + obj + // a2*x + t2 <= 0 + // a3*x + t3 <= 0 + // a4*x + t4 <= 0 + // a1 > 0, a2 > 0, a3 > 0, a4 < 0 + // x <= -t2/a2 + // x <= -t2/a3 + // determine lub among these. + // then resolve lub with others + // e.g., -t2/a2 <= -t3/a3, then + // replace inequality a3*x + t3 <= 0 by -t2/a2 + t3/a3 <= 0 + // mark a4 as invalid. + // + + // a1 < 0, a2 < 0, a3 < 0, a4 > 0 + // x >= t2/a2 + // x >= t3/a3 + // determine glb among these + // the resolve glb with others. + // 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) { + // tbd + SASSERT(invariant()); + vector & vars = m_objective.m_vars; + unsigned_vector other; + while (!vars.empty()) { + var const& v = 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_index; + other.reset(); + if (find_bound(x, bound_index, other, coeff.is_pos())) { + rational bound_coeff = m_rows[bound_index].m_coeff; + for (unsigned i = 0; i < other.size(); ++i) { + resolve(other[i], bound_coeff, bound_index, x); + } + // coeff*x + objective -> coeff*(bound) + objective + // tbd: + multiply(coeff/bound_coeff, bound_index); + //add(m_objective_id, bound_index); + m_rows[bound_index].m_alive = false; + } + else { + return unbounded; + } + } + value = m_objective.m_coeff; + switch (m_objective.m_type) { + case t_lt: return strict; + case t_le: return non_strict; + case t_eq: return non_strict; + } + return non_strict; + } + + bool model_based_opt::find_bound(unsigned x, unsigned& bound_index, unsigned_vector& other, bool is_pos) { + bound_index = UINT_MAX; + rational lub_val; + rational const& x_val = m_var2value[x]; + unsigned_vector const& row_ids = m_var2row_ids[x]; + for (unsigned i = 0; i < row_ids.size(); ++i) { + unsigned row_id = row_ids[i]; + row& r = m_rows[row_id]; + if (r.m_alive) { + rational a = get_coefficient(row_id, x); + if (a.is_pos() == is_pos) { + rational value = r.m_value - x_val*a; // r.m_value = val_x*a + val(t), val(t) := r.m_value - val_x*a; + if (bound_index == UINT_MAX) { + lub_val = value; + bound_index = row_id; + } + else if ((is_pos && value < lub_val) || (!is_pos && value > lub_val)) { + other.push_back(bound_index); + lub_val = value; + bound_index = row_id; + } + else { + other.push_back(bound_index); + } + } + else if (!a.is_zero()) { + r.m_alive = false; + } + } + } + return bound_index != UINT_MAX; + } + + rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) { + row const& r = m_rows[row_id]; + unsigned lo = 0, hi = r.m_vars.size(); + while (lo < hi) { + unsigned mid = lo + (hi - lo)/2; + SASSERT(mid < hi); + unsigned id = r.m_vars[mid].m_id; + if (id == var_id) { + lo = mid; + break; + } + if (id < var_id) { + lo = mid + 1; + } + else { + hi = mid - 1; + } + } + unsigned id = r.m_vars[lo].m_id; + if (id == var_id) { + return r.m_vars[lo].m_coeff; + } + else { + return rational::zero(); + } + } + + bool model_based_opt::resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x) { + // 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. + // if a1 is positive, then val(t1*a2/a1) <= val(t2*a1/a2) + // replace row2 with the new inequality of the form: + // 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) { + return false; + } + rational a2 = get_coefficient(row_id2, x); + if (a2.is_zero()) { + return false; + } + else if (a1.is_pos() && a2.is_pos()) { + multiply(-a1/a2, row_id2); + add(row_id2, row_id1); + return true; + } + else if (a1.is_neg() && a2.is_neg()) { + NOT_IMPLEMENTED_YET(); + // tbd + return true; + } + else { + m_rows[row_id2].m_alive = false; + return false; + } + } + + void model_based_opt::multiply(rational const& c, unsigned row_id) { + if (c.is_one()) { + return; + } + row& r = m_rows[row_id]; + SASSERT(r.m_alive); + for (unsigned i = 0; i < r.m_vars.size(); ++i) { + r.m_vars[i].m_coeff *= c; + } + r.m_coeff *= c; + r.m_value *= c; + } + + // add row2 to row1, store result in row1. + + void model_based_opt::add(unsigned row_id1, unsigned row_id2) { + m_new_vars.reset(); + row& r1 = m_rows[row_id1]; + row const& r2 = m_rows[row_id2]; + unsigned i = 0, j = 0; + for(; i < r1.m_vars.size() || j < r2.m_vars.size(); ) { + if (j == r2.m_vars.size()) { + m_new_vars.append(r1.m_vars.size() - i, r1.m_vars.c_ptr() + i); + } + else if (i == r1.m_vars.size()) { + for (; j < r2.m_vars.size(); ++j) { + m_new_vars.push_back(r2.m_vars[j]); + m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1); + } + } + else { + unsigned v1 = r1.m_vars[i].m_id; + unsigned v2 = r2.m_vars[j].m_id; + if (v1 == v2) { + m_new_vars.push_back(r1.m_vars[i]); + m_new_vars.back().m_coeff += r2.m_vars[j].m_coeff; + ++i; + ++j; + if (m_new_vars.back().m_coeff.is_zero()) { + m_new_vars.pop_back(); + } + } + else if (v1 < v2) { + m_new_vars.push_back(r1.m_vars[i]); + ++i; + } + else { + m_new_vars.push_back(r2.m_vars[j]); + m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1); + ++j; + } + } + } + r1.m_coeff += r2.m_coeff; + r1.m_vars.swap(m_new_vars); + r1.m_value += r2.m_value; + if (r2.m_type == t_lt) { + r1.m_type = t_lt; + } + } + + void model_based_opt::display(std::ostream& out) const { + for (unsigned i = 0; i < m_rows.size(); ++i) { + display(out, m_rows[i]); + } + } + + void model_based_opt::display(std::ostream& out, row const& r) const { + vector const& vars = r.m_vars; + for (unsigned i = 0; i < vars.size(); ++i) { + if (i > 0 && vars[i].m_coeff.is_pos()) { + out << "+ "; + } + out << vars[i].m_coeff << "* v" << vars[i].m_id << " "; + } + out << r.m_coeff; + switch (r.m_type) { + case t_eq: + out << " = 0\n"; + break; + case t_lt: + out << " < 0\n"; + break; + case t_le: + out << " <= 0\n"; + break; + } + } + + unsigned model_based_opt::add_var(rational const& value) { + NOT_IMPLEMENTED_YET(); + return 0; + } + + void model_based_opt::add_constraint(vector const& coeffs, rational const& c, ineq_type r) { + NOT_IMPLEMENTED_YET(); + } + + void model_based_opt::set_objective(vector const& coeffs, rational const& c) { + NOT_IMPLEMENTED_YET(); + } + +} + diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h new file mode 100644 index 000000000..d881d3caa --- /dev/null +++ b/src/math/simplex/model_based_opt.h @@ -0,0 +1,102 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + model_based_opt.h + +Abstract: + + Model-based optimization for linear real arithmetic. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-27-4 + +Revision History: + + +--*/ + +#ifndef __MODEL_BASED_OPT_H__ +#define __MODEL_BASED_OPT_H__ + +#include "util.h" +#include "rational.h" + +namespace opt { + + enum ineq_type { + t_eq, + t_lt, + t_le + }; + + enum bound_type { + unbounded, + strict, + non_strict + }; + + class model_based_opt { + public: + struct var { + unsigned m_id; + rational m_coeff; + var(unsigned id, rational const& c): m_id(id), m_coeff(c) {} + }; + private: + struct row { + vector m_vars; // variables with coefficients + rational m_coeff; // constant in inequality + ineq_type m_type; // inequality type + rational m_value; // value of m_vars + m_coeff under interpretation of m_var2value. + bool m_alive; // rows can be marked dead if they have been processed. + }; + vector m_rows; + vector m_var2row_ids; + vector m_var2value; + row m_objective; + vector m_new_vars; + + bool invariant(); + bool invariant(row const& r); + + + bool find_bound(unsigned x, unsigned& bound_index, unsigned_vector& other, bool is_pos); + + rational get_coefficient(unsigned row_id, unsigned var_id); + + bool resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x); + + void multiply(rational const& c, unsigned row_id); + + void add(unsigned row_id1, unsigned row_id2); + + public: + + // add a fresh variable with value 'value'. + unsigned add_var(rational const& value); + + // 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); + + // 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); + + + void display(std::ostream& out) const; + void display(std::ostream& out, row const& r) const; + + }; + +} + +#endif diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index d128a4fe9..f1637dfb7 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -51,175 +51,6 @@ namespace qe { return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t); } - enum ineq_type { - t_eq, - t_lt, - t_le - }; - - struct tableau { - struct var { - unsigned m_id; - rational m_coeff; - var(unsigned id, rational const& c): m_id(id), m_coeff(c) {} - }; - struct row { - vector m_vars; // variables with coefficients - rational m_coeff; // constant in inequality - ineq_type m_type; // inequality type - rational m_value; // value of m_vars + m_coeff under interpretation of m_var2value. - bool m_alive; // rows can be marked dead if they have been processed. - }; - vector m_rows; - vector m_var2rows; - vector m_var2value; - row m_objective; - - void invariant() { - // variables in each row are sorted. - } - - mbp::bound_type maximize(rational& value) { - // tbd - return mbp::unbounded; - } - - rational get_coefficient(unsigned row_id, unsigned var_id) { - row const& r = m_rows[row_id]; - unsigned lo = 0, hi = r.m_vars.size(); - while (lo < hi) { - unsigned mid = lo + (hi - lo)/2; - SASSERT(mid < hi); - unsigned id = r.m_vars[mid].m_id; - if (id == var_id) { - lo = mid; - break; - } - if (id < var_id) { - lo = mid + 1; - } - else { - hi = mid - 1; - } - } - unsigned id = r.m_vars[lo].m_id; - if (id == var_id) { - return r.m_vars[lo].m_coeff; - } - else { - return rational::zero(); - } - } - - void resolve(unsigned row_id1, unsigned row_id2, unsigned x) { - // 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. - // if a1 is positive, then val(t1*a2/a1) <= val(t2*a1/a2) - // replace row2 with the new inequality of the form: - // t1 - a1*t2/a2 <~~ 0 - // where <~~ is strict if either <~1 or <~2 is strict. - // if a1 is negative, then .... - // - } - - void multiply(rational const& c, unsigned row_id) { - if (c.is_one()) { - return; - } - row& r = m_rows[row_id]; - SASSERT(r.m_alive); - for (unsigned i = 0; i < r.m_vars.size(); ++i) { - r.m_vars[i].m_coeff *= c; - } - r.m_coeff *= c; - r.m_value *= c; - } - - // subtract row2 from row1, store result in row2 - - vector m_new_vars; - - void subtract(unsigned row_id1, unsigned row_id2) { - m_new_vars.reset(); - row const& r1 = m_rows[row_id1]; - row& r2 = m_rows[row_id2]; - unsigned i = 0, j = 0; - for(; i < r1.m_vars.size() || j < r2.m_vars.size(); ) { - if (j == r2.m_vars.size()) { - for (; i < r1.m_vars.size(); ++i) { - m_new_vars.push_back(r1.m_vars[i]); - m_var2rows[r1.m_vars[i].m_id].push_back(row_id2); - } - } - else if (i == r1.m_vars.size()) { - for (; j < r2.m_vars.size(); ++j) { - m_new_vars.push_back(r2.m_vars[j]); - m_new_vars.back().m_coeff.neg(); - } - } - else { - unsigned v1 = r1.m_vars[i].m_id; - unsigned v2 = r2.m_vars[j].m_id; - if (v1 == v2) { - m_new_vars.push_back(r1.m_vars[i]); - m_new_vars.back().m_coeff -= r2.m_vars[j].m_coeff; - ++i; - ++j; - if (m_new_vars.back().m_coeff.is_zero()) { - m_new_vars.pop_back(); - } - } - else if (v1 < v2) { - m_new_vars.push_back(r1.m_vars[i]); - m_var2rows[r1.m_vars[i].m_id].push_back(row_id2); - ++i; - } - else { - m_new_vars.push_back(r2.m_vars[j]); - m_new_vars.back().m_coeff.neg(); - ++j; - } - } - } - r2.m_coeff.neg(); - r2.m_coeff += r1.m_coeff; - r2.m_vars.swap(m_new_vars); - r2.m_value.neg(); - r2.m_value += r1.m_value; - if (r1.m_type == t_lt) { - r2.m_type = t_lt; - } - } - - void display(std::ostream& out) const { - for (unsigned i = 0; i < m_rows.size(); ++i) { - display(out, m_rows[i]); - } - } - - void display(std::ostream& out, row const& r) const { - vector const& vars = r.m_vars; - for (unsigned i = 0; i < vars.size(); ++i) { - if (i > 0 && vars[i].m_coeff.is_pos()) { - out << "+ "; - } - out << vars[i].m_coeff << "* v" << vars[i].m_id << " "; - } - out << r.m_coeff; - switch (r.m_type) { - case t_eq: - out << " = 0\n"; - break; - case t_lt: - out << " < 0\n"; - break; - case t_le: - out << " <= 0\n"; - break; - } - } - }; #if 0 obj_map m_expr2var; @@ -234,7 +65,7 @@ namespace qe { th_rewriter m_rw; expr_ref_vector m_ineq_terms; vector m_ineq_coeffs; - svector m_ineq_types; + svector m_ineq_types; expr_ref_vector m_div_terms; vector m_div_divisors, m_div_coeffs; expr_ref_vector m_new_lits; @@ -368,7 +199,7 @@ namespace qe { bool is_linear(model& model, expr* lit, bool& found_eq) { rational c(0), mul(1); expr_ref t(m); - ineq_type ty = t_le; + opt::ineq_type ty = opt::t_le; expr* e1, *e2; expr_ref_vector ts(m); bool is_not = m.is_not(lit, lit); @@ -379,17 +210,17 @@ namespace qe { if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { is_linear(model, mul, e1, c, ts); is_linear(model, -mul, e2, c, ts); - ty = is_not?t_lt:t_le; + ty = is_not? opt::t_lt : opt::t_le; } else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { is_linear(model, mul, e1, c, ts); is_linear(model, -mul, e2, c, ts); - ty = is_not?t_le:t_lt; + ty = is_not? opt::t_le: opt::t_lt; } else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) { is_linear(model, mul, e1, c, ts); is_linear(model, -mul, e2, c, ts); - ty = t_eq; + ty = opt::t_eq; } else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) { expr_ref val(m); @@ -408,7 +239,7 @@ namespace qe { is_linear(model, mul, nums[i+1].first, c, ts); is_linear(model, -mul, nums[i].first, c, ts); t = add(ts); - accumulate_linear(model, c, t, t_lt); + accumulate_linear(model, c, t, opt::t_lt); } t = mk_num(0); c.reset(); @@ -427,7 +258,7 @@ namespace qe { if (r1 < r2) { std::swap(e1, e2); } - ty = t_lt; + ty = opt::t_lt; is_linear(model, mul, e1, c, ts); is_linear(model, -mul, e2, c, ts); } @@ -435,24 +266,24 @@ namespace qe { TRACE("qe", tout << "can't project:" << mk_pp(lit, m) << "\n";); throw cant_project(); } - if (ty == t_lt && is_int()) { + if (ty == opt::t_lt && is_int()) { ts.push_back(mk_num(1)); - ty = t_le; + ty = opt::t_le; } t = add(ts); - if (ty == t_eq && c.is_neg()) { + if (ty == opt::t_eq && c.is_neg()) { t = mk_uminus(t); c.neg(); } - if (ty == t_eq && c > rational(1)) { + if (ty == opt::t_eq && c > rational(1)) { m_ineq_coeffs.push_back(-c); m_ineq_terms.push_back(mk_uminus(t)); - m_ineq_types.push_back(t_le); + m_ineq_types.push_back(opt::t_le); m_num_neg++; - ty = t_le; + ty = opt::t_le; } accumulate_linear(model, c, t, ty); - found_eq = !c.is_zero() && ty == t_eq; + found_eq = !c.is_zero() && ty == opt::t_eq; return true; } @@ -503,16 +334,16 @@ namespace qe { } }; - void accumulate_linear(model& model, rational const& c, expr_ref& t, ineq_type ty) { + void accumulate_linear(model& model, rational const& c, expr_ref& t, opt::ineq_type ty) { if (c.is_zero()) { switch (ty) { - case t_eq: + case opt::t_eq: t = a.mk_eq(t, mk_num(0)); break; - case t_lt: + case opt::t_lt: t = a.mk_lt(t, mk_num(0)); break; - case t_le: + case opt::t_le: t = a.mk_le(t, mk_num(0)); break; } @@ -522,7 +353,7 @@ namespace qe { m_ineq_coeffs.push_back(c); m_ineq_terms.push_back(t); m_ineq_types.push_back(ty); - if (ty == t_eq) { + if (ty == opt::t_eq) { // skip } else if (c.is_pos()) { @@ -632,18 +463,18 @@ namespace qe { expr* ineq_term(unsigned i) const { return m_ineq_terms[i]; } rational const& ineq_coeff(unsigned i) const { return m_ineq_coeffs[i]; } - ineq_type ineq_ty(unsigned i) const { return m_ineq_types[i]; } + opt::ineq_type ineq_ty(unsigned i) const { return m_ineq_types[i]; } app_ref mk_ineq_pred(unsigned i) { app_ref result(m); result = to_app(mk_add(mk_mul(ineq_coeff(i), m_var->x()), ineq_term(i))); switch (ineq_ty(i)) { - case t_lt: + case opt::t_lt: result = a.mk_lt(result, mk_num(0)); break; - case t_le: + case opt::t_le: result = a.mk_le(result, mk_num(0)); break; - case t_eq: + case opt::t_eq: result = m.mk_eq(result, mk_num(0)); break; } @@ -652,9 +483,9 @@ namespace qe { void display_ineq(std::ostream& out, unsigned i) const { out << mk_pp(ineq_term(i), m) << " " << ineq_coeff(i) << "*" << mk_pp(m_var->x(), m); switch (ineq_ty(i)) { - case t_eq: out << " = 0\n"; break; - case t_le: out << " <= 0\n"; break; - case t_lt: out << " < 0\n"; break; + case opt::t_eq: out << " = 0\n"; break; + case opt::t_le: out << " <= 0\n"; break; + case opt::t_lt: out << " < 0\n"; break; } } unsigned num_ineqs() const { return m_ineq_terms.size(); } @@ -769,7 +600,7 @@ namespace qe { bool is_int = a.is_int(m_var->x()); for (unsigned i = 0; i < num_ineqs(); ++i) { rational const& ac = m_ineq_coeffs[i]; - SASSERT(!is_int || t_le == ineq_ty(i)); + SASSERT(!is_int || opt::t_le == ineq_ty(i)); // // ac*x + t < 0 @@ -783,7 +614,7 @@ namespace qe { new_max = new_max || (r > max_r) || - (r == max_r && t_lt == ineq_ty(i)) || + (r == max_r && opt::t_lt == ineq_ty(i)) || (r == max_r && is_int && ac.is_one()); TRACE("qe", tout << "max: " << mk_pp(ineq_term(i), m) << "/" << abs(ac) << " := " << r << " " << (new_max?"":"not ") << "new max\n";); @@ -821,7 +652,7 @@ namespace qe { expr_ref ts = mk_add(bt, as); expr_ref z = mk_num(0); expr_ref fml(m); - if (t_lt == ineq_ty(i) || t_lt == ineq_ty(j)) { + if (opt::t_lt == ineq_ty(i) || opt::t_lt == ineq_ty(j)) { fml = a.mk_lt(ts, z); } else { @@ -838,7 +669,7 @@ namespace qe { rational ac = ineq_coeff(i); rational bc = ineq_coeff(j); expr_ref tmp(m); - SASSERT(t_le == ineq_ty(i) && t_le == ineq_ty(j)); + SASSERT(opt::t_le == ineq_ty(i) && opt::t_le == ineq_ty(j)); SASSERT(ac.is_pos() == bc.is_neg()); rational abs_a = abs(ac); rational abs_b = abs(bc); @@ -917,7 +748,7 @@ namespace qe { expr* s = ineq_term(j); expr_ref bt = mk_mul(abs(bc), t); expr_ref as = mk_mul(abs(ac), s); - if (t_lt == ineq_ty(i) && t_le == ineq_ty(j)) { + if (opt::t_lt == ineq_ty(i) && opt::t_le == ineq_ty(j)) { return expr_ref(a.mk_lt(bt, as), m); } else { @@ -988,9 +819,9 @@ namespace qe { expr_ref lhs(m), val(m); lhs = mk_sub(mk_mul(c, ineq_term(i)), mk_mul(ineq_coeff(i), t)); switch (ineq_ty(i)) { - case t_lt: lhs = a.mk_lt(lhs, mk_num(0)); break; - case t_le: lhs = a.mk_le(lhs, mk_num(0)); break; - case t_eq: lhs = m.mk_eq(lhs, mk_num(0)); break; + case opt::t_lt: lhs = a.mk_lt(lhs, mk_num(0)); break; + case opt::t_le: lhs = a.mk_le(lhs, mk_num(0)); break; + case opt::t_eq: lhs = m.mk_eq(lhs, mk_num(0)); break; } TRACE("qe", tout << lhs << "\n";); SASSERT (model.eval(lhs, val) && m.is_true(val)); @@ -1082,17 +913,17 @@ namespace qe { return true; } - mbp::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { + opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { obj_map ts; 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 mbp::unbounded; + return opt::unbounded; } }; @@ -1116,7 +947,7 @@ namespace qe { return m_imp->a.get_family_id(); } - mbp::bound_type arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { + 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); } diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index 9ba3fa5fc..f79a61245 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -29,7 +29,7 @@ namespace qe { 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(); - mbp::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound); + opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, 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 a3d8d077c..c592445ea 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -213,7 +213,7 @@ class mbp::impl { public: - mbp::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { + opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { arith_project_plugin arith(m); return arith.maximize(fmls, mdl, t, value, bound); } @@ -421,6 +421,6 @@ void mbp::extract_literals(model& model, expr_ref_vector& lits) { m_impl->extract_literals(model, lits); } -mbp::bound_type mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) { +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); } diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 2fc5a9fb9..4081288b4 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -24,6 +24,7 @@ Revision History: #include "ast.h" #include "params.h" #include "model.h" +#include "model_based_opt.h" namespace qe { @@ -75,12 +76,7 @@ namespace qe { \brief Maximize objective t under current model for constraints in fmls. */ - enum bound_type { - unbounded, - strict, - non_strict - }; - bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound); + opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound); }; } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 3c3a5c0dd..a220cf268 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1284,16 +1284,16 @@ namespace qe { app* m_objective; expr_ref m_value; - mbp::bound_type m_bound; + opt::bound_type m_bound; bool m_was_sat; - lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, mbp::bound_type& bound) { + lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound) { expr_ref_vector defs(m); expr_ref fml = negate_core(fmls); hoist(fml); m_objective = t; m_value = 0; - m_bound = mbp::unbounded; + m_bound = opt::unbounded; m_was_sat = false; m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); @@ -1334,14 +1334,14 @@ namespace qe { expr_ref bound(m); m_bound = m_mbp.maximize(core, mdl, m_objective, m_value, bound); switch (m_bound) { - case mbp::unbounded: + case opt::unbounded: m_ex.assert_expr(m.mk_false()); m_fa.assert_expr(m.mk_false()); break; - case mbp::strict: + case opt::strict: m_ex.assert_expr(bound); break; - case mbp::non_strict: + case opt::non_strict: m_ex.assert_expr(bound); break; } @@ -1349,7 +1349,7 @@ namespace qe { }; - lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, mbp::bound_type& bound, params_ref const& p) { + lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p) { ast_manager& m = fmls.get_manager(); qsat qs(m, p, qsat_maximize); return qs.maximize(fmls, t, value, bound); diff --git a/src/qe/qsat.h b/src/qe/qsat.h index dfba75e6c..fd10e3e75 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, mbp::bound_type& bound, params_ref const& p); + lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p); }