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);
}