From 044e08a11467b9f3e3712f90129ad8b2b7bccf5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 May 2016 11:17:09 -0700 Subject: [PATCH] adding unit tests for qe_arith/mbo Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 91 +++++++++++++---------- src/test/qe_arith.cpp | 164 +++++++++++++++++++++++++++++++++++++++++- 2 files changed, 216 insertions(+), 39 deletions(-) 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 m_expr2var; - ptr_vector m_var2expr; - -#endif struct arith_project_plugin::imp { @@ -88,18 +81,23 @@ namespace qe { } } - void insert_mul(expr* x, rational const& v, obj_map& ts) - { + void insert_mul(expr* x, rational const& v, obj_map& 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& 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& tids) { obj_map 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& 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& ts, obj_map& 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 const& ts, obj_map& tids, vars& coeffs) { + void extract_coefficients(opt::model_based_opt& mbo, model& model, 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(); + 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 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 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 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 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 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);