diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index ab711dde7..6f6daf8df 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -212,14 +212,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// auxiliary function for pull_ite_core
expr * mk_eq_value(expr * lhs, expr * value) {
- SASSERT(m().is_value(value));
- if (m().is_value(lhs)) {
- if (m().are_equal(lhs, value)) {
- return m().mk_true();
- }
- else if (m().are_distinct(lhs, value)) {
- return m().mk_false();
- }
+ if (m().are_equal(lhs, value)) {
+ return m().mk_true();
+ }
+ else if (m().are_distinct(lhs, value)) {
+ return m().mk_false();
}
return m().mk_eq(lhs, value);
}
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 60111a473..58a290c0b 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -51,13 +51,6 @@ namespace qe {
}
return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
}
-
-
-#if 0
- obj_map<expr, unsigned> m_expr2var;
- ptr_vector<expr> m_var2expr;
-
-#endif
struct arith_project_plugin::imp {
@@ -88,18 +81,23 @@ namespace qe {
}
}
- void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts)
- {
+ void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
rational w;
if (ts.find(x, w)) {
ts.insert(x, w + v);
}
else {
+ TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << "\n";);
ts.insert(x, v);
}
}
- void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map<expr, unsigned>& tids) {
+ //
+ // extract linear inequalities from literal 'lit' into the model-based optimization manager 'mbo'.
+ // It uses the current model to choose values for conditionals and it primes mbo with the current
+ // interpretation of sub-expressions that are treated as variables for mbo.
+ //
+ void linearize(opt::model_based_opt& mbo, model& model, expr* lit, obj_map<expr, unsigned>& tids) {
obj_map<expr, rational> ts;
rational c(0), mul(1);
expr_ref t(m);
@@ -112,19 +110,19 @@ namespace qe {
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);
+ linearize(mbo, model, mul, e1, c, ts, tids);
+ linearize(mbo, model, -mul, e2, c, ts, tids);
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);
+ linearize(mbo, model, mul, e1, c, ts, tids);
+ linearize(mbo, model, -mul, e2, c, ts, tids);
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);
+ linearize(mbo, model, mul, e1, c, ts, tids);
+ linearize(mbo, model, -mul, e2, c, ts, tids);
ty = opt::t_eq;
}
else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
@@ -137,55 +135,63 @@ namespace qe {
UNREACHABLE();
}
else {
+ TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
return;
}
- if (ty == opt::t_lt && is_int()) {
+#if 0
+ TBD for integers
+ if (ty == opt::t_lt && false) {
c += rational(1);
ty = opt::t_le;
}
+#endif
vars coeffs;
- extract_coefficients(ts, tids, coeffs);
+ extract_coefficients(mbo, model, ts, tids, coeffs);
mbo.add_constraint(coeffs, c, ty);
}
- void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map<expr, rational>& ts) {
+ //
+ // convert linear arithmetic term into an inequality for mbo.
+ //
+ void linearize(opt::model_based_opt& mbo, model& model, rational const& mul, expr* t, rational& c,
+ obj_map<expr, rational>& ts, obj_map<expr, unsigned>& tids) {
expr* t1, *t2, *t3;
rational mul1;
expr_ref val(m);
if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) {
- linearize(model, mul* mul1, t2, c, ts);
+ linearize(mbo, model, mul* mul1, t2, c, ts, tids);
}
else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) {
- linearize(model, mul* mul1, t1, c, ts);
+ linearize(mbo, model, mul* mul1, t1, c, ts, tids);
}
else if (a.is_add(t)) {
app* ap = to_app(t);
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
- linearize(model, mul, ap->get_arg(i), c, ts);
+ linearize(mbo, model, mul, ap->get_arg(i), c, ts, tids);
}
}
else if (a.is_sub(t, t1, t2)) {
- linearize(model, mul, t1, c, ts);
- linearize(model, -mul, t2, c, ts);
+ linearize(mbo, model, mul, t1, c, ts, tids);
+ linearize(mbo, model, -mul, t2, c, ts, tids);
}
else if (a.is_uminus(t, t1)) {
- linearize(model, -mul, t1, c, ts);
+ linearize(mbo, model, -mul, t1, c, ts, tids);
}
else if (a.is_numeral(t, mul1)) {
c += mul*mul1;
}
- else if (extract_mod(model, t, val)) {
- insert_mul(val, mul, ts);
- }
else if (m.is_ite(t, t1, t2, t3)) {
VERIFY(model.eval(t1, val));
SASSERT(m.is_true(val) || m.is_false(val));
TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
if (m.is_true(val)) {
- linearize(model, mul, t2, c, ts);
+ linearize(mbo, model, mul, t2, c, ts, tids);
+ linearize(mbo, model, t1, tids);
}
else {
- linearize(model, mul, t3, c, ts);
+ expr_ref not_t1(mk_not(m, t1), m);
+ linearize(mbo, model, mul, t3, c, ts, tids);
+ linearize(mbo, model, not_t1, tids);
}
}
else {
@@ -193,6 +199,9 @@ namespace qe {
}
}
+ //
+ // extract linear terms from t into c and ts.
+ //
void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
expr* t1, *t2, *t3;
rational mul1;
@@ -245,7 +254,9 @@ namespace qe {
}
}
-
+ //
+ // extract linear inequalities from literal lit.
+ //
bool is_linear(model& model, expr* lit, bool& found_eq) {
rational c(0), mul(1);
expr_ref t(m);
@@ -977,13 +988,13 @@ namespace qe {
// extract objective function.
vars coeffs;
rational c(0), mul(1);
- linearize(mdl, mul, t, c, ts);
- extract_coefficients(ts, tids, coeffs);
+ linearize(mbo, mdl, mul, t, c, ts, tids);
+ extract_coefficients(mbo, mdl, ts, tids, coeffs);
mbo.set_objective(coeffs, c);
// extract linear constraints
for (unsigned i = 0; i < fmls.size(); ++i) {
- linearize(mdl, mbo, fmls[i], tids);
+ linearize(mbo, mdl, fmls[i], tids);
}
// find optimal value
@@ -1021,13 +1032,21 @@ namespace qe {
return value;
}
- void extract_coefficients(obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
+ void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
coeffs.reset();
obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
for (; it != end; ++it) {
unsigned id;
if (!tids.find(it->m_key, id)) {
- id = tids.size();
+ rational r;
+ expr_ref val(m);
+ if (model.eval(it->m_key, val) && a.is_numeral(val, r)) {
+ id = mbo.add_var(r);
+ }
+ else {
+ TRACE("qe", tout << "extraction of coefficients cancelled\n";);
+ return;
+ }
tids.insert(it->m_key, id);
}
coeffs.push_back(var(id, it->m_value));
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index a1b5c2859..f14ccf3e2 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -280,12 +280,170 @@ static void test2(char const *ex) {
ctx.assert_expr(pr1);
ctx.assert_expr(npr2);
VERIFY(l_false == ctx.check());
- ctx.pop(1);
-
-
+ ctx.pop(1);
}
+typedef opt::model_based_opt::var var_t;
+
+static void mk_var(unsigned x, app_ref& v) {
+ ast_manager& m = v.get_manager();
+ arith_util a(m);
+ std::ostringstream strm;
+ strm << "v" << x;
+ v = m.mk_const(symbol(strm.str().c_str()), a.mk_real());
+}
+
+static void mk_term(vector<var_t> const& vars, rational const& coeff, app_ref& term) {
+ ast_manager& m = term.get_manager();
+ expr_ref_vector ts(m);
+ arith_util a(m);
+
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ app_ref var(m);
+ mk_var(vars[i].m_id, var);
+ rational coeff = vars[i].m_coeff;
+ ts.push_back(a.mk_mul(a.mk_numeral(coeff, false), var));
+ }
+ ts.push_back(a.mk_numeral(coeff, a.mk_real()));
+ term = a.mk_add(ts.size(), ts.c_ptr());
+}
+
+static void add_random_ineq(
+ expr_ref_vector& fmls,
+ opt::model_based_opt& mbo,
+ random_gen& r,
+ svector<int> const& values,
+ unsigned max_vars,
+ unsigned max_coeff)
+{
+ ast_manager& m = fmls.get_manager();
+ arith_util a(m);
+
+ unsigned num_vars = values.size();
+ uint_set used_vars;
+ vector<var_t> vars;
+ int value = 0;
+ for (unsigned i = 0; i < max_vars; ++i) {
+ unsigned x = r(num_vars);
+ if (used_vars.contains(x)) {
+ continue;
+ }
+ used_vars.insert(x);
+ int coeff = r(max_coeff + 1);
+ if (coeff == 0) {
+ continue;
+ }
+ unsigned sign = r(2);
+ coeff = sign == 0 ? coeff : -coeff;
+ vars.push_back(var_t(x, rational(coeff)));
+ value += coeff*values[x];
+ }
+ unsigned abs_value = value < 0 ? - value : value;
+ // value + k <= 0
+ // k <= - value
+ // range for k is 2*|value|
+ // k <= - value - range
+ opt::ineq_type rel = opt::t_le;
+
+ int coeff = 0;
+ if (r(4) == 0) {
+ rel = opt::t_eq;
+ coeff = -value;
+ }
+ else {
+ if (abs_value > 0) {
+ coeff = -value - r(2*abs_value);
+ }
+ else {
+ coeff = 0;
+ }
+ if (coeff != -value && r(3) == 0) {
+ rel = opt::t_lt;
+ }
+ }
+ expr_ref fml(m);
+ app_ref t1(m);
+ app_ref t2(a.mk_numeral(rational(0), a.mk_real()), m);
+ mk_term(vars, rational(coeff), t1);
+ switch (rel) {
+ case opt::t_eq:
+ fml = m.mk_eq(t1, t2);
+ break;
+ case opt::t_lt:
+ fml = a.mk_lt(t1, t2);
+ break;
+ case opt::t_le:
+ fml = a.mk_le(t1, t2);
+ break;
+ }
+ fmls.push_back(fml);
+ mbo.add_constraint(vars, rational(coeff), rel);
+}
+
+static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) {
+ qe::arith_project_plugin plugin(m);
+ model mdl(m);
+ expr_ref bound(m);
+ arith_util a(m);
+ for (unsigned i = 0; i < num_vars; ++i) {
+ app_ref var(m);
+ mk_var(i, var);
+ rational val = mbo.get_value(i);
+ mdl.register_decl(var->get_decl(), a.mk_numeral(val, false));
+ }
+ opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound);
+ opt::inf_eps value2 = mbo.maximize();
+ std::cout << "optimal: " << value1 << " " << value2 << "\n";
+ mbo.display(std::cout);
+}
+
+static void check_random_ineqs(random_gen& r, ast_manager& m, unsigned num_vars, unsigned max_value, unsigned num_ineqs, unsigned max_vars, unsigned max_coeff) {
+ opt::model_based_opt mbo;
+ expr_ref_vector fmls(m);
+
+ svector<int> values;
+ for (unsigned i = 0; i < num_vars; ++i) {
+ values.push_back(r(max_value + 1));
+ mbo.add_var(rational(values.back()));
+ }
+ for (unsigned i = 0; i < num_ineqs; ++i) {
+ add_random_ineq(fmls, mbo, r, values, max_vars, max_coeff);
+ }
+
+ vector<var_t> vars;
+ vars.reset();
+ vars.push_back(var_t(0, rational(2)));
+ vars.push_back(var_t(1, rational(-2)));
+ mbo.set_objective(vars, rational(0));
+
+
+ mbo.display(std::cout);
+ app_ref t(m);
+ mk_term(vars, rational(0), t);
+
+ test_maximize(mbo, m, num_vars, fmls, t);
+
+ for (unsigned i = 0; i < values.size(); ++i) {
+ std::cout << i << ": " << values[i] << " -> " << mbo.get_value(i) << "\n";
+ }
+}
+
+static void check_random_ineqs() {
+ random_gen r(1);
+ ast_manager m;
+ reg_decl_plugins(m);
+
+ for (unsigned i = 0; i < 100; ++i) {
+ check_random_ineqs(r, m, 4, 5, 5, 3, 6);
+ }
+}
+
+
+
+
void tst_qe_arith() {
+ check_random_ineqs();
+ return;
// enable_trace("qe");
testI(example8);
testR(example7);