diff --git a/src/nlsat/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h index 6ec7a3461..442853377 100644 --- a/src/nlsat/nlsat_scoped_literal_vector.h +++ b/src/nlsat/nlsat_scoped_literal_vector.h @@ -64,6 +64,13 @@ namespace nlsat { for (unsigned i = 0; i < sz; i++) push_back(ls[i]); } + void append(scoped_literal_vector const& ls) { + append(ls.size(), ls.c_ptr()); + } + void swap(scoped_literal_vector& other) { + SASSERT(&m_solver == &other.m_solver); + m_lits.swap(other.m_lits); + } }; diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 00114cf05..fb9e85b8b 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -30,6 +30,8 @@ Notes: #include"arith_decl_plugin.h" #include"tactic.h" #include"ast_smt2_pp.h" +#include"polynomial.h" +#include"algebraic_numbers.h" struct goal2nlsat::imp { struct nlsat_expr2polynomial : public expr2polynomial { @@ -257,6 +259,7 @@ struct goal2nlsat::imp { process(g.form(i), g.dep(i)); } } + }; struct goal2nlsat::scoped_set_imp { @@ -289,4 +292,154 @@ void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver scoped_set_imp setter(*this, local_imp); local_imp(g); } + + +struct nlsat2goal::imp { + ast_manager& m; + arith_util a; + u_map const* m_x2t; +public: + imp(ast_manager& m):m(m),a(m) {} + + expr_ref operator()(nlsat::solver& s, u_map const& b2a, u_map const& x2t, nlsat::literal l) { + m_x2t = &x2t; + expr_ref result(m); + expr* t; + if (b2a.find(l.var(), t)) { + result = t; + } + else { + nlsat::atom const* at = s.bool_var2atom(l.var()); + SASSERT(at != 0); + if (at->is_ineq_atom()) { + nlsat::ineq_atom const* ia = to_ineq_atom(at); + unsigned sz = ia->size(); + expr_ref_vector ps(m); + bool is_int = true; + for (unsigned i = 0; is_int && i < sz; ++i) { + is_int = poly_is_int(ia->p(i)); + } + for (unsigned i = 0; i < sz; ++i) { + polynomial::polynomial* p = ia->p(i); + expr_ref t = poly2expr(s, p, is_int); + if (ia->is_even(i)) { + t = a.mk_power(t, a.mk_numeral(rational(2), a.is_int(t))); + } + ps.push_back(t); + } + result = a.mk_mul_simplify(ps); + expr_ref zero(m); + zero = a.mk_numeral(rational(0), a.is_int(result)); + switch (ia->get_kind()) { + case nlsat::atom::EQ: + result = m.mk_eq(result, zero); + break; + case nlsat::atom::LT: + if (l.sign()) { + l.neg(); + result = a.mk_ge(result, zero); + } + else { + result = a.mk_lt(result, zero); + } + break; + case nlsat::atom::GT: + if (l.sign()) { + l.neg(); + result = a.mk_le(result, zero); + } + else { + result = a.mk_gt(result, zero); + } + break; + default: + UNREACHABLE(); + } + } + else { + //nlsat::root_atom const* ra = nlsat::to_root_atom(at); + //ra->i(); + //expr_ref p = poly2expr(s, ra->p()); + //expr* x = m_x2t->find(ra->x()); + std::ostringstream strm; + s.display(strm, l.sign()?~l:l); + result = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); + } + } + + if (l.sign()) { + result = m.mk_not(result); + } + return result; + } + + expr_ref poly2expr(nlsat::solver& s, polynomial::polynomial* p, bool is_int) { + expr_ref result(m); + unsigned sz = polynomial::manager::size(p); + expr_ref_vector args(m); + for (unsigned i = 0; i < sz; ++i) { + args.push_back(mono2expr(s, + polynomial::manager::coeff(p, i), + polynomial::manager::get_monomial(p, i), is_int)); + } + result = a.mk_add_simplify(args); + return result; + } + + expr_ref mono2expr(nlsat::solver& s, polynomial::numeral const& c, polynomial::monomial* mon, bool is_int) { + expr_ref result(m); + expr_ref_vector args(m); + unsigned sz = polynomial::manager::size(mon); + for (unsigned i = 0; i < sz; ++i) { + unsigned d = polynomial::manager::degree(mon, i); + expr* t = m_x2t->find(polynomial::manager::get_var(mon, i)); + SASSERT(d >= 1); + if (d == 1) { + args.push_back(t); + } + else { + args.push_back(a.mk_power(t, a.mk_numeral(rational(d), a.is_int(t)))); + } + } + if (!s.pm().m().is_one(c)) { + args.push_back(a.mk_numeral(c, is_int)); + } + result = a.mk_mul_simplify(args); + return result; + } + + bool poly_is_int(polynomial::polynomial* p) { + bool is_int = true; + unsigned sz = polynomial::manager::size(p); + for (unsigned i = 0; is_int && i < sz; ++i) { + is_int = mono_is_int(polynomial::manager::get_monomial(p, i)); + } + return is_int; + } + + bool mono_is_int(polynomial::monomial* mon) { + bool is_int = true; + unsigned sz = polynomial::manager::size(mon); + for (unsigned i = 0; is_int && i < sz; ++i) { + is_int = a.is_int(m_x2t->find(polynomial::manager::get_var(mon, i))); + } + return is_int; + } +}; + + +nlsat2goal::nlsat2goal(ast_manager& m) { + m_imp = alloc(imp, m); +} + + +nlsat2goal::~nlsat2goal() { + dealloc(m_imp); +} + +expr_ref nlsat2goal::operator()(nlsat::solver& s, u_map const& b2a, u_map const& x2t, nlsat::literal l) { + return (*m_imp)(s, b2a, x2t, l); +} + + diff --git a/src/nlsat/tactic/goal2nlsat.h b/src/nlsat/tactic/goal2nlsat.h index ae9bbdb74..bdb71a6a3 100644 --- a/src/nlsat/tactic/goal2nlsat.h +++ b/src/nlsat/tactic/goal2nlsat.h @@ -57,17 +57,16 @@ class nlsat2goal { struct imp; imp * m_imp; public: - nlsat2goal(); + nlsat2goal(ast_manager& m); ~nlsat2goal(); static void collect_param_descrs(param_descrs & r); /** - \brief Translate the state of the nlsat engine back into a goal. - */ - void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x, - params_ref const & p, goal & g, model_converter_ref & mc); - + \brief Translate a literal into a formula. + */ + expr_ref operator()(nlsat::solver& s, u_map const& b2a, u_map const& x2t, nlsat::literal l); + }; #endif diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 585944263..1df22e385 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -36,7 +36,6 @@ Revision History: #include "expr_functors.h" #include "quant_hoist.h" #include "bool_rewriter.h" -#include "qe_util.h" #include "th_rewriter.h" #include "smt_kernel.h" #include "model_evaluator.h" @@ -2281,7 +2280,7 @@ namespace qe { } } - static void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) { + void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) { ast_manager& m = new_body.get_manager(); expr_ref tmp(m); unsigned nd = q->get_num_decls(); diff --git a/src/qe/qe.h b/src/qe/qe.h index 0370ff3a0..a75af19c5 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -223,6 +223,8 @@ namespace qe { qe_solver_plugin* mk_arith_plugin(i_solver_context& ctx, bool produce_models, smt_params& p); + void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars); + class def_vector { func_decl_ref_vector m_vars; expr_ref_vector m_defs; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index bc4a824d1..2b00efba0 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2010 Microsoft Corporation +Copyright (c) 2015 Microsoft Corporation Module Name: @@ -16,188 +16,557 @@ Author: Revision History: + --*/ #include "qe_arith.h" -#include "qe_util.h" #include "ast_util.h" #include "arith_decl_plugin.h" #include "ast_pp.h" #include "th_rewriter.h" #include "expr_functors.h" +#include "model_v2_pp.h" +#include "expr_safe_replace.h" namespace qe { + + bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) { + expr* t1, *t2; + ast_manager& m = a.get_manager(); + if (a.is_mod(e2, t1, t2) && + a.is_numeral(e1, k) && + k.is_zero() && + a.is_numeral(t2, k)) { + p = t1; + return true; + } + return false; + } + + bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t) { + expr* e1, *e2; + if (!a.get_manager().is_eq(e, e1, e2)) { + return false; + } + return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t); + } - class arith_project_util { - ast_manager& m; - arith_util a; - th_rewriter m_rw; - expr_ref_vector m_ineq_terms; - vector m_ineq_coeffs; - svector m_ineq_strict; + struct arith_project_plugin::imp { + + enum ineq_type { + t_eq, + t_lt, + t_le + }; + ast_manager& m; + arith_util a; + th_rewriter m_rw; + expr_ref_vector m_ineq_terms; + vector m_ineq_coeffs; + svector m_ineq_types; + expr_ref_vector m_div_terms; + vector m_div_divisors, m_div_coeffs; + expr_ref_vector m_new_lits; + rational m_delta, m_u; scoped_ptr m_var; + unsigned m_num_pos, m_num_neg; + bool m_pos_is_unit, m_neg_is_unit; - struct cant_project {}; + sort* var_sort() const { return m.get_sort(m_var->x()); } - void is_linear(rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { - expr* t1, *t2; + bool is_int() const { return a.is_int(m_var->x()); } + + void display(std::ostream& out) const { + for (unsigned i = 0; i < num_ineqs(); ++i) { + display_ineq(out, i); + } + for (unsigned i = 0; i < num_divs(); ++i) { + display_div(out, i); + } + } + + void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { + expr* t1, *t2, *t3; rational mul1; + expr_ref val(m); if (t == m_var->x()) { c += mul; } - else if (a.is_mul(t, t1, t2) && a.is_numeral(t1, mul1)) { - is_linear(mul* mul1, t2, c, ts); + else if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) { + is_linear(model, mul* mul1, t2, c, ts); } - else if (a.is_mul(t, t1, t2) && a.is_numeral(t2, mul1)) { - is_linear(mul* mul1, t1, c, ts); + else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) { + is_linear(model, mul* mul1, t1, c, ts); } else if (a.is_add(t)) { app* ap = to_app(t); for (unsigned i = 0; i < ap->get_num_args(); ++i) { - is_linear(mul, ap->get_arg(i), c, ts); + is_linear(model, mul, ap->get_arg(i), c, ts); } } else if (a.is_sub(t, t1, t2)) { - is_linear(mul, t1, c, ts); - is_linear(-mul, t2, c, ts); + is_linear(model, mul, t1, c, ts); + is_linear(model, -mul, t2, c, ts); } else if (a.is_uminus(t, t1)) { - is_linear(-mul, t1, c, ts); + is_linear(model, -mul, t1, c, ts); } else if (a.is_numeral(t, mul1)) { - ts.push_back(a.mk_numeral(mul*mul1, m.get_sort(t))); + ts.push_back(mk_num(mul*mul1)); + } + else if (extract_mod(model, t, val)) { + ts.push_back(mk_mul(mul, val)); + } + else if (m.is_ite(t, t1, t2, t3)) { + VERIFY(model.eval(t1, val)); + SASSERT(m.is_true(val) || m.is_false(val)); + if (m.is_true(val)) { + is_linear(model, mul, t2, c, ts); + } + else { + is_linear(model, mul, t3, c, ts); + } } else if ((*m_var)(t)) { - IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(t, m) << "\n";); + TRACE("qe", tout << "can't project:" << mk_pp(t, m) << "\n";); throw cant_project(); } - else if (mul.is_one()) { - ts.push_back(t); - } else { - ts.push_back(a.mk_mul(a.mk_numeral(mul, m.get_sort(t)), t)); + ts.push_back(mk_mul(mul, t)); } } - bool is_linear(expr* lit, rational& c, expr_ref& t, bool& is_strict) { - if (!(*m_var)(lit)) { - return false; - } + + bool is_linear(model& model, expr* lit, bool& found_eq) { + rational c(0), mul(1); + expr_ref t(m); + ineq_type ty = t_le; expr* e1, *e2; - c.reset(); - sort* s; expr_ref_vector ts(m); bool is_not = m.is_not(lit, lit); - rational mul(1); if (is_not) { mul.neg(); } SASSERT(!m.is_not(lit)); if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { - is_linear( mul, e1, c, ts); - is_linear(-mul, e2, c, ts); - s = m.get_sort(e1); - is_strict = is_not; + is_linear(model, mul, e1, c, ts); + is_linear(model, -mul, e2, c, ts); + ty = is_not?t_lt:t_le; } else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { - is_linear( mul, e1, c, ts); - is_linear(-mul, e2, c, ts); - s = m.get_sort(e1); - is_strict = !is_not; + is_linear(model, mul, e1, c, ts); + is_linear(model, -mul, e2, c, ts); + ty = is_not?t_le: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; + } + else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) { + expr_ref val(m); + rational r; + app* alit = to_app(lit); + vector > nums; + for (unsigned i = 0; i < alit->get_num_args(); ++i) { + VERIFY(model.eval(alit->get_arg(i), val) && a.is_numeral(val, r)); + nums.push_back(std::make_pair(alit->get_arg(i), r)); + } + std::sort(nums.begin(), nums.end(), compare_second()); + for (unsigned i = 0; i + 1 < nums.size(); ++i) { + SASSERT(nums[i].second < nums[i+1].second); + c.reset(); + ts.reset(); + 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); + } + t = mk_num(0); + c.reset(); + return true; + } + else if (m.is_distinct(lit) && is_not && is_arith(to_app(lit)->get_arg(0))) { + expr_ref eq = project_plugin::pick_equality(m, model, to_app(lit)->get_arg(0)); + return is_linear(model, eq, found_eq); + } + else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) { + expr_ref val1(m), val2(m); + rational r1, r2; + VERIFY(model.eval(e1, val1) && a.is_numeral(val1, r1)); + VERIFY(model.eval(e2, val2) && a.is_numeral(val2, r2)); + SASSERT(r1 != r2); + if (r1 < r2) { + std::swap(e1, e2); + } + ty = t_lt; + is_linear(model, mul, e1, c, ts); + is_linear(model, -mul, e2, c, ts); } - else if (m.is_eq(lit, e1, e2) && !is_not) { - is_linear( mul, e1, c, ts); - is_linear(-mul, e2, c, ts); - s = m.get_sort(e1); - is_strict = false; - } else { - IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(lit, m) << "\n";); + TRACE("qe", tout << "can't project:" << mk_pp(lit, m) << "\n";); throw cant_project(); } - if (ts.empty()) { - t = a.mk_numeral(rational(0), s); + if (ty == t_lt && is_int()) { + ts.push_back(mk_num(1)); + ty = t_le; } - else { - t = a.mk_add(ts.size(), ts.c_ptr()); + t = add(ts); + if (ty == t_eq && c.is_neg()) { + t = mk_uminus(t); + c.neg(); } + if (ty == 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_num_neg++; + ty = t_le; + } + accumulate_linear(model, c, t, ty); + found_eq = !c.is_zero() && ty == t_eq; return true; } - void project(model& model, expr_ref_vector& lits) { - unsigned num_pos = 0; - unsigned num_neg = 0; - m_ineq_terms.reset(); - m_ineq_coeffs.reset(); - m_ineq_strict.reset(); - expr_ref_vector new_lits(m); - for (unsigned i = 0; i < lits.size(); ++i) { - rational c(0); - expr_ref t(m); - bool is_strict; - if (is_linear(lits[i].get(), c, t, is_strict)) { - m_ineq_coeffs.push_back(c); - m_ineq_terms.push_back(t); - m_ineq_strict.push_back(is_strict); - if (c.is_zero()) { - m_rw(lits[i].get(), t); - new_lits.push_back(t); - } - else if (c.is_pos()) { - ++num_pos; - } - else { - ++num_neg; - } + bool is_numeral(model& model, expr* t, rational& r) { + expr* t1, *t2, *t3; + rational r1, r2; + expr_ref val(m); + if (a.is_numeral(t, r)) return true; + + if (a.is_uminus(t, t1) && is_numeral(model, t1, r)) { + r.neg(); + return true; + } + else if (a.is_mul(t, t1, t2) && is_numeral(model, t1, r1) && is_numeral(model, t2, r2)) { + r = r1*r2; + return true; + } + else if (a.is_add(t)) { + app* ap = to_app(t); + r = rational(1); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + if (!is_numeral(model, ap->get_arg(i), r1)) return false; + r *= r1; + } + return true; + } + else if (m.is_ite(t, t1, t2, t3)) { + VERIFY (model.eval(t1, val)); + if (m.is_true(val)) { + return is_numeral(model, t1, r); } else { - new_lits.push_back(lits[i].get()); + return is_numeral(model, t2, r); } } + else if (a.is_sub(t, t1, t2) && is_numeral(model, t1, r1) && is_numeral(model, t2, r2)) { + r = r1 - r2; + return true; + } + + return false; + } + + struct compare_second { + bool operator()(std::pair const& a, + std::pair const& b) const { + return a.second < b.second; + } + }; + + void accumulate_linear(model& model, rational const& c, expr_ref& t, ineq_type ty) { + if (c.is_zero()) { + switch (ty) { + case t_eq: + t = a.mk_eq(t, mk_num(0)); + break; + case t_lt: + t = a.mk_lt(t, mk_num(0)); + break; + case t_le: + t = a.mk_le(t, mk_num(0)); + break; + } + add_lit(model, m_new_lits, t); + } + else { + m_ineq_coeffs.push_back(c); + m_ineq_terms.push_back(t); + m_ineq_types.push_back(ty); + if (ty == t_eq) { + // skip + } + else if (c.is_pos()) { + ++m_num_pos; + m_pos_is_unit &= c.is_one(); + } + else { + ++m_num_neg; + m_neg_is_unit &= c.is_minus_one(); + } + } + } + + bool is_arith(expr* e) { + return a.is_int(e) || a.is_real(e); + } + + expr_ref add(expr_ref_vector const& ts) { + switch (ts.size()) { + case 0: + return mk_num(0); + case 1: + return expr_ref(ts[0], m); + default: + return expr_ref(a.mk_add(ts.size(), ts.c_ptr()), m); + } + } + + + // e is of the form (ax + t) mod k + bool is_mod(model& model, expr* e, rational& k, expr_ref& t, rational& c) { + expr* t1, *t2; + expr_ref_vector ts(m); + if (a.is_mod(e, t1, t2) && + a.is_numeral(t2, k) && + (*m_var)(t1)) { + c.reset(); + rational mul(1); + is_linear(model, mul, t1, c, ts); + t = add(ts); + return true; + } + return false; + } + + bool extract_mod(model& model, expr* e, expr_ref& val) { + rational c, k; + expr_ref t(m); + if (is_mod(model, e, k, t, c)) { + VERIFY (model.eval(e, val)); + SASSERT (a.is_numeral(val)); + TRACE("qe", tout << "extract: " << mk_pp(e, m) << " evals: " << val << " c: " << c << " t: " << t << "\n";); + if (!c.is_zero()) { + t = mk_sub(t, val); + m_div_terms.push_back(t); + m_div_divisors.push_back(k); + m_div_coeffs.push_back(c); + } + else { + t = m.mk_eq(a.mk_mod(t, mk_num(k)), val); + add_lit(model, m_new_lits, t); + } + return true; + } + return false; + } + + bool lit_is_true(model& model, expr* e) { + expr_ref val(m); + VERIFY(model.eval(e, val)); + CTRACE("qe", !m.is_true(val), tout << "eval: " << mk_pp(e, m) << " " << val << "\n";); + return m.is_true(val); + } + + expr_ref mk_num(unsigned n) { + rational r(n); + return mk_num(r); + } + + expr_ref mk_num(rational const& r) const { + return expr_ref(a.mk_numeral(r, var_sort()), m); + } + + expr_ref mk_divides(rational const& k, expr* t) { + return expr_ref(m.mk_eq(a.mk_mod(t, mk_num(abs(k))), mk_num(0)), m); + } + + void reset() { + reset_ineqs(); + reset_divs(); + m_delta = rational(1); + m_u = rational(0); + m_new_lits.reset(); + } + + void reset_divs() { + m_div_terms.reset(); + m_div_coeffs.reset(); + m_div_divisors.reset(); + } + + void reset_ineqs() { + m_ineq_terms.reset(); + m_ineq_coeffs.reset(); + m_ineq_types.reset(); + } + + 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]; } + 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: + result = a.mk_lt(result, mk_num(0)); + break; + case t_le: + result = a.mk_le(result, mk_num(0)); + break; + case t_eq: + result = m.mk_eq(result, mk_num(0)); + break; + } + return result; + } + 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; + } + } + unsigned num_ineqs() const { return m_ineq_terms.size(); } + expr* div_term(unsigned i) const { return m_div_terms[i]; } + rational const& div_coeff(unsigned i) const { return m_div_coeffs[i]; } + rational const& div_divisor(unsigned i) const { return m_div_divisors[i]; } + void display_div(std::ostream& out, unsigned i) const { + out << div_divisor(i) << " | ( " << mk_pp(div_term(i), m) << " " << div_coeff(i) << "*" + << mk_pp(m_var->x(), m) << ")\n"; + } + unsigned num_divs() const { return m_div_terms.size(); } + + void project(model& model, expr_ref_vector& lits) { + TRACE("qe", + tout << "project: " << mk_pp(m_var->x(), m) << "\n"; + tout << lits; + model_v2_pp(tout, model); ); + + m_num_pos = 0; m_num_neg = 0; + m_pos_is_unit = true; m_neg_is_unit = true; + unsigned eq_index = 0; + reset(); + bool found_eq = false; + for (unsigned i = 0; i < lits.size(); ++i) { + bool found_eq0 = false; + expr* e = lits[i].get(); + if (!(*m_var)(e)) { + m_new_lits.push_back(e); + } + else if (!is_linear(model, e, found_eq0)) { + TRACE("qe", tout << "can't project:" << mk_pp(e, m) << "\n";); + throw cant_project(); + } + if (found_eq0 && !found_eq) { + found_eq = true; + eq_index = num_ineqs()-1; + } + } + TRACE("qe", display(tout << mk_pp(m_var->x(), m) << ":\n"); + tout << "found eq: " << found_eq << " @ " << eq_index << "\n"; + tout << "num pos: " << m_num_pos << " num neg: " << m_num_neg << " num divs " << num_divs() << "\n"; + ); lits.reset(); - lits.append(new_lits); - if (num_pos == 0 || num_neg == 0) { + lits.append(m_new_lits); + if (found_eq) { + apply_equality(model, eq_index, lits); return; } - bool use_pos = num_pos < num_neg; - unsigned max_t = find_max(model, use_pos); - - for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { - if (i != max_t) { - if (m_ineq_coeffs[i].is_pos() == use_pos) { - lits.push_back(mk_le(i, max_t)); + if (num_divs() == 0 && (m_num_pos == 0 || m_num_neg == 0)) { + return; + } + if (num_divs() > 0) { + apply_divides(model, lits); + TRACE("qe", display(tout << "after division " << mk_pp(m_var->x(), m) << "\n");); + } + if (m_num_pos == 0 || m_num_neg == 0) { + return; + } + if ((m_num_pos <= 2 || m_num_neg <= 2) && + (m_num_pos == 1 || m_num_neg == 1 || (m_num_pos <= 3 && m_num_neg <= 3)) && + (!is_int() || m_pos_is_unit || m_neg_is_unit)) { + + unsigned index1 = num_ineqs(); + unsigned index2 = num_ineqs(); + bool is_pos = m_num_pos <= m_num_neg; + for (unsigned i = 0; i < num_ineqs(); ++i) { + if (ineq_coeff(i).is_pos() == is_pos) { + if (index1 == num_ineqs()) { + index1 = i; + } + else { + SASSERT(index2 == num_ineqs()); + index2 = i; + } } - else { - lits.push_back(mk_lt(i, max_t)); + } + for (unsigned i = 0; i < num_ineqs(); ++i) { + if (ineq_coeff(i).is_pos() != is_pos) { + SASSERT(index1 != num_ineqs()); + mk_lt(model, lits, i, index1); + if (index2 != num_ineqs()) { + mk_lt(model, lits, i, index2); + } } } } + else { + expr_ref t(m); + bool use_pos = m_num_pos < m_num_neg; + unsigned max_t = find_max(model, use_pos); + + for (unsigned i = 0; i < num_ineqs(); ++i) { + if (i != max_t) { + if (ineq_coeff(i).is_pos() == use_pos) { + t = mk_le(i, max_t); + add_lit(model, lits, t); + } + else { + mk_lt(model, lits, i, max_t); + } + } + } + } + TRACE("qe", tout << lits;); } unsigned find_max(model& mdl, bool do_pos) { unsigned result; - bool found = false; - rational found_val(0), r, found_c; + bool new_max = true; + rational max_r, r; expr_ref val(m); - for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { + 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)); + + // + // ac*x + t < 0 + // ac > 0: x + max { t/ac | ac > 0 } < 0 <=> x < - max { t/ac | ac > 0 } + // ac < 0: x + t/ac > 0 <=> x > max { - t/ac | ac < 0 } = max { t/|ac| | ac < 0 } + // if (ac.is_pos() == do_pos) { - VERIFY(mdl.eval(m_ineq_terms[i].get(), val)); + VERIFY(mdl.eval(ineq_term(i), val)); VERIFY(a.is_numeral(val, r)); r /= abs(ac); - IF_VERBOSE(1, verbose_stream() << "max: " << mk_pp(m_ineq_terms[i].get(), m) << " " << r << " " << (!found || r > found_val) << "\n";); - if (!found || r > found_val) { + new_max = + new_max || + (r > max_r) || + (r == max_r && 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";); + if (new_max) { result = i; - found_val = r; - found_c = ac; - found = true; + max_r = r; } + new_max = false; } } - SASSERT(found); - if (a.is_int(m_var->x()) && !found_c.is_one()) { - throw cant_project(); - } + SASSERT(!new_max); return result; } @@ -206,102 +575,310 @@ namespace qe { // a and b have different signs. // Infer: a|b|x + |b|t + |a|bx + |a|s <= 0 // e.g. |b|t + |a|s <= 0 - expr_ref mk_lt(unsigned i, unsigned j) { - rational const& ac = m_ineq_coeffs[i]; - rational const& bc = m_ineq_coeffs[j]; + void mk_lt(model& model, expr_ref_vector& lits, unsigned i, unsigned j) { + rational const& ac = ineq_coeff(i); + rational const& bc = ineq_coeff(j); SASSERT(ac.is_pos() != bc.is_pos()); SASSERT(ac.is_neg() != bc.is_neg()); - expr* t = m_ineq_terms[i].get(); - expr* s = m_ineq_terms[j].get(); + + TRACE("qe", display_ineq(tout, i); display_ineq(tout, j);); + + if (is_int() && !abs(ac).is_one() && !abs(bc).is_one()) { + return mk_int_lt(model, lits, i, j); + } + expr* t = ineq_term(i); + expr* s = ineq_term(j); expr_ref bt = mk_mul(abs(bc), t); expr_ref as = mk_mul(abs(ac), s); expr_ref ts = mk_add(bt, as); - expr* z = a.mk_numeral(rational(0), m.get_sort(t)); - expr_ref result1(m), result2(m); - if (m_ineq_strict[i] || m_ineq_strict[j]) { - result1 = a.mk_lt(ts, z); + expr_ref z = mk_num(0); + expr_ref fml(m); + if (t_lt == ineq_ty(i) || t_lt == ineq_ty(j)) { + fml = a.mk_lt(ts, z); } else { - result1 = a.mk_le(ts, z); + fml = a.mk_le(ts, z); } - m_rw(result1, result2); - return result2; + add_lit(model, lits, fml); + } + + void mk_int_lt(model& model, expr_ref_vector& lits, unsigned i, unsigned j) { + TRACE("qe", display_ineq(tout, i); display_ineq(tout, j);); + + expr* t = ineq_term(i); + expr* s = ineq_term(j); + 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(ac.is_pos() == bc.is_neg()); + rational abs_a = abs(ac); + rational abs_b = abs(bc); + expr_ref as(mk_mul(abs_a, s), m); + expr_ref bt(mk_mul(abs_b, t), m); + + rational slack = (abs_a - rational(1))*(abs_b-rational(1)); + rational sval, tval; + VERIFY (model.eval(ineq_term(i), tmp) && a.is_numeral(tmp, tval)); + VERIFY (model.eval(ineq_term(j), tmp) && a.is_numeral(tmp, sval)); + bool use_case1 = ac*sval + bc*tval + slack <= rational(0); + if (use_case1) { + expr_ref_vector ts(m); + ts.push_back(as); + ts.push_back(bt); + ts.push_back(mk_num(-slack)); + tmp = a.mk_le(add(ts), mk_num(0)); + add_lit(model, lits, tmp); + return; + } + + if (abs_a < abs_b) { + std::swap(abs_a, abs_b); + std::swap(ac, bc); + std::swap(s, t); + std::swap(as, bt); + std::swap(sval, tval); + } + SASSERT(abs_a >= abs_b); + + // create finite disjunction for |b|. + // exists x, z in [0 .. |b|-2] . b*x + s + z = 0 && ax + t <= 0 && bx + s <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && ax + t <= 0 && bx + s <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && a|b|x + |b|t <= 0 && bx + s <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && a|b|x + |b|t <= 0 && -z - s + s <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && a|b|x + |b|t <= 0 && -z <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && a|b|x + |b|t <= 0 + // <=> + // exists x, z in [0 .. |b|-2] . b*x = -z - s && a*n_sign(b)(s + z) + |b|t <= 0 + // <=> + // exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0 + // + + rational z = mod(sval, abs_b); + if (!z.is_zero()) z = abs_b - z; + expr_ref s_plus_z(mk_add(z, s), m); + + tmp = mk_divides(abs_b, s_plus_z); + add_lit(model, lits, tmp); + tmp = a.mk_le(mk_add(mk_mul(ac*n_sign(bc), s_plus_z), + mk_mul(abs_b, t)), mk_num(0)); + add_lit(model, lits, tmp); + } + + rational n_sign(rational const& b) { + return rational(b.is_pos()?-1:1); } // ax + t <= 0 // bx + s <= 0 // a and b have same signs. - // encode:// t/|a| <= s/|b| + // encode: + // t/|a| <= s/|b| // e.g. |b|t <= |a|s expr_ref mk_le(unsigned i, unsigned j) { - rational const& ac = m_ineq_coeffs[i]; - rational const& bc = m_ineq_coeffs[j]; + rational const& ac = ineq_coeff(i); + rational const& bc = ineq_coeff(j); SASSERT(ac.is_pos() == bc.is_pos()); SASSERT(ac.is_neg() == bc.is_neg()); - expr* t = m_ineq_terms[i].get(); - expr* s = m_ineq_terms[j].get(); + expr* t = ineq_term(i); + expr* s = ineq_term(j); expr_ref bt = mk_mul(abs(bc), t); expr_ref as = mk_mul(abs(ac), s); - expr_ref result1(m), result2(m); - if (m_ineq_strict[j] && !m_ineq_strict[i]) { - result1 = a.mk_lt(bt, as); + if (t_lt == ineq_ty(i) && t_le == ineq_ty(j)) { + return expr_ref(a.mk_lt(bt, as), m); } else { - result1 = a.mk_le(bt, as); + return expr_ref(a.mk_le(bt, as), m); } - m_rw(result1, result2); - return result2; } - expr_ref mk_add(expr* t1, expr* t2) { + rational r; + if (a.is_numeral(t1, r) && r.is_zero()) return expr_ref(t2, m); + if (a.is_numeral(t2, r) && r.is_zero()) return expr_ref(t1, m); return expr_ref(a.mk_add(t1, t2), m); } - expr_ref mk_mul(rational const& r, expr* t2) { - expr* t1 = a.mk_numeral(r, m.get_sort(t2)); - return expr_ref(a.mk_mul(t1, t2), m); + expr_ref mk_add(rational const& r, expr* e) { + if (r.is_zero()) return expr_ref(e, m); + return mk_add(mk_num(r), e); + } + + expr_ref mk_mul(rational const& r, expr* t) { + if (r.is_one()) return expr_ref(t, m); + return expr_ref(a.mk_mul(mk_num(r), t), m); } - public: - arith_project_util(ast_manager& m): - m(m), a(m), m_rw(m), m_ineq_terms(m) {} + expr_ref mk_sub(expr* t1, expr* t2) { + rational r1, r2; + if (a.is_numeral(t2, r2) && r2.is_zero()) return expr_ref(t1, m); + if (a.is_numeral(t1, r1) && a.is_numeral(t2, r2)) return mk_num(r1 - r2); + return expr_ref(a.mk_sub(t1, t2), m); + } - expr_ref operator()(model& model, app_ref_vector& vars, expr_ref_vector const& lits) { - app_ref_vector new_vars(m); - expr_ref_vector result(lits); - for (unsigned i = 0; i < vars.size(); ++i) { - app* v = vars[i].get(); - m_var = alloc(contains_app, m, v); - try { - project(model, result); - TRACE("qe", tout << "projected: " << mk_pp(v, m) << " "; - for (unsigned i = 0; i < result.size(); ++i) { - tout << mk_pp(result[i].get(), m) << "\n"; - }); - } - catch (cant_project) { - IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(v, m) << "\n";); - new_vars.push_back(v); + expr_ref mk_uminus(expr* t) { + rational r; + if (a.is_numeral(t, r)) { + return mk_num(-r); + } + return expr_ref(a.mk_uminus(t), m); + } + + void add_lit(model& model, expr_ref_vector& lits, expr* e) { + expr_ref orig(e, m), result(m); + m_rw(orig, result); + TRACE("qe", tout << mk_pp(orig, m) << " -> " << result << "\n";); + SASSERT(lit_is_true(model, orig)); + SASSERT(lit_is_true(model, result)); + if (!m.is_true(result)) { + lits.push_back(result); + } + } + + + // 3x + t = 0 & 7 | (c*x + s) & ax <= u + // 3 | -t & 21 | (-ct + 3s) & a-t <= 3u + + void apply_equality(model& model, unsigned eq_index, expr_ref_vector& lits) { + rational c = ineq_coeff(eq_index); + expr* t = ineq_term(eq_index); + SASSERT(c.is_pos()); + if (is_int()) { + add_lit(model, lits, mk_divides(c, ineq_term(eq_index))); + } + + for (unsigned i = 0; i < num_divs(); ++i) { + add_lit(model, lits, mk_divides(c*div_divisor(i), + mk_sub(mk_mul(c, div_term(i)), mk_mul(div_coeff(i), t)))); + } + for (unsigned i = 0; i < num_ineqs(); ++i) { + if (eq_index != i) { + 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; + } + TRACE("qe", tout << lhs << "\n";); + SASSERT (model.eval(lhs, val) && m.is_true(val)); + add_lit(model, lits, lhs); } } - vars.reset(); - vars.append(new_vars); - return qe::mk_and(result); - } + } + + // + // compute D and u. + // + // D = lcm(d1, d2) + // u = eval(x) mod D + // + // d1 | (a1x + t1) & d2 | (a2x + t2) + // = + // D | (D/d1)(a1x + t1) & D | (D/d2)(a2x + t2) + // = + // D | D1(a1*u + t1) & D | D2(a2*u + t2) & x = D*x' + u & 0 <= u < D + // = + // D | D1(a1*u + t1) & D | D2(a2*u + t2) & x = D*x' + u & 0 <= u < D + // + // x := D*x' + u + // + void apply_divides(model& model, expr_ref_vector& lits) { + SASSERT(m_delta.is_one()); + unsigned n = num_divs(); + if (n == 0) { + return; + } + for (unsigned i = 0; i < n; ++i) { + m_delta = lcm(m_delta, div_divisor(i)); + } + expr_ref val(m); + rational r; + VERIFY (model.eval(m_var->x(), val) && a.is_numeral(val, r)); + m_u = mod(r, m_delta); + SASSERT(m_u < m_delta && rational(0) <= m_u); + for (unsigned i = 0; i < n; ++i) { + add_lit(model, lits, mk_divides(div_divisor(i), + mk_add(mk_num(div_coeff(i) * m_u), div_term(i)))); + } + reset_divs(); + // + // update inequalities such that u is added to t and + // D is multiplied to coefficient of x. + // the interpretation of the new version of x is (x-u)/D + // + // a*x + t <= 0 + // a*(D*x' + u) + t <= 0 + // a*D*x' + a*u + t <= 0 + for (unsigned i = 0; i < num_ineqs(); ++i) { + if (!m_u.is_zero()) { + m_ineq_terms[i] = a.mk_add(ineq_term(i), mk_num(m_ineq_coeffs[i]*m_u)); + } + m_ineq_coeffs[i] *= m_delta; + } + r = (r - m_u) / m_delta; + SASSERT(r.is_int()); + val = a.mk_numeral(r, true); + model.register_decl(m_var->x()->get_decl(), val); + TRACE("qe", model_v2_pp(tout, model);); + } + + imp(ast_manager& m): + m(m), a(m), m_rw(m), m_ineq_terms(m), m_div_terms(m), m_new_lits(m) { + params_ref params; + params.set_bool("gcd_rouding", true); + m_rw.updt_params(params); + } + + ~imp() { + } + + bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return false; + } + + bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) { + SASSERT(a.is_real(v) || a.is_int(v)); + m_var = alloc(contains_app, m, v); + try { + project(model, lits); + } + catch (cant_project) { + TRACE("qe", tout << "can't project:" << mk_pp(v, m) << "\n";); + return false; + } + return true; + } }; - expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits) { - ast_manager& m = vars.get_manager(); - arith_project_util ap(m); - return ap(model, vars, lits); + arith_project_plugin::arith_project_plugin(ast_manager& m) { + m_imp = alloc(imp, m); } - expr_ref arith_project(model& model, app_ref_vector& vars, expr* fml) { - ast_manager& m = vars.get_manager(); - arith_project_util ap(m); - expr_ref_vector lits(m); - flatten_and(fml, lits); - return ap(model, vars, lits); + arith_project_plugin::~arith_project_plugin() { + dealloc(m_imp); } + bool arith_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + return (*m_imp)(model, var, vars, lits); + } + + bool arith_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return m_imp->solve(model, vars, lits); + } + + family_id arith_project_plugin::get_family_id() { + return m_imp->a.get_family_id(); + } + + bool arith_project(model& model, app* var, expr_ref_vector& lits) { + ast_manager& m = lits.get_manager(); + arith_project_plugin ap(m); + app_ref_vector vars(m); + return ap(model, var, vars, lits); + } } diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index 16a89794f..be5415a45 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -9,16 +9,33 @@ Copyright (c) 2015 Microsoft Corporation #define QE_ARITH_H_ #include "model.h" +#include "arith_decl_plugin.h" +#include "qe_mbp.h" namespace qe { + /** Loos-Weispfenning model-based projection for a basic conjunction. Lits is a vector of literals. return vector of variables that could not be projected. */ - expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits); - expr_ref arith_project(model& model, app_ref_vector& vars, expr* fml); + class arith_project_plugin : public project_plugin { + struct imp; + imp* m_imp; + public: + arith_project_plugin(ast_manager& m); + virtual ~arith_project_plugin(); + 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(); + }; + + bool arith_project(model& model, app* var, expr_ref_vector& lits); + + // match e := t mod k = 0. + bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t); + }; #endif diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 75cba61fe..8bb3fa6e2 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -32,6 +32,7 @@ Revision History: #include "nlarith_util.h" #include "model_evaluator.h" #include "smt_kernel.h" +#include "qe_arith.h" namespace qe { @@ -266,23 +267,8 @@ namespace qe { // // match 0 == p mod k, p mod k == 0 // - bool is_divides(app* e, numeral& k, expr_ref& p) { - expr* e1, *e2; - if (!m.is_eq(e, e1, e2)) { - return false; - } - return is_divides(e1, e2, k, p) || is_divides(e2, e1, k, p); - } - - bool is_divides(expr* e1, expr* e2, numeral& k, expr_ref& p) { - if (m_arith.is_mod(e2) && - m_arith.is_numeral(e1, k) && - k.is_zero() && - m_arith.is_numeral(to_app(e2)->get_arg(1), k)) { - p = to_app(e2)->get_arg(0); - return true; - } - return false; + bool is_divides(expr* e, numeral& k, expr_ref& p) { + return qe::is_divides(m_arith, e, k, p); } bool is_not_divides(app* e, app_ref& n, numeral& k, expr_ref& p) { diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp new file mode 100644 index 000000000..4f2ce81c5 --- /dev/null +++ b/src/qe/qe_arrays.cpp @@ -0,0 +1,427 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_arrays.cpp + +Abstract: + + Model based projection for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + +Revision History: + +--*/ + + +#include "qe_arrays.h" +#include "rewriter_def.h" +#include "expr_functors.h" +#include "expr_safe_replace.h" +#include "lbool.h" +#include "ast_util.h" +#include "ast_pp.h" + +namespace qe { + + struct array_project_plugin::imp { + + // rewriter or direct procedure. + struct rw_cfg : public default_rewriter_cfg { + ast_manager& m; + array_util& a; + expr_ref_vector m_lits; + model* m_model; + imp* m_imp; + + rw_cfg(ast_manager& m, array_util& a): + m(m), a(a), m_lits(m), m_model(0) {} + + br_status reduce_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result, proof_ref & pr) { + if (a.is_select(f) && a.is_store(args[0])) { + expr_ref val1(m), val2(m); + app* b = to_app(args[0]); + SASSERT(b->get_num_args() == n + 1); + for (unsigned i = 1; i < n; ++i) { + expr* arg1 = args[i]; + expr* arg2 = b->get_arg(i); + if (arg1 == arg2) { + val1 = val2 = arg1; + } + else { + VERIFY(m_model->eval(arg1, val1)); + VERIFY(m_model->eval(arg2, val2)); + } + switch(compare(val1, val2)) { + case l_true: + if (arg1 != arg2) { + m_lits.push_back(m.mk_eq(arg1, arg2)); + } + break; + case l_false: { + ptr_vector new_args; + if (i > 0) { + m_lits.resize(m_lits.size() - i); + } + m_lits.push_back(m.mk_not(m.mk_eq(arg1, arg2))); + new_args.push_back(b->get_arg(0)); + new_args.append(n-1, args+1); + result = m.mk_app(f, n, new_args.c_ptr()); + return BR_REWRITE1; + } + case l_undef: + return BR_FAILED; + } + } + result = b->get_arg(n); + return BR_DONE; + } + return BR_FAILED; + } + + lbool compare(expr* x, expr* y) { + NOT_IMPLEMENTED_YET(); + return l_undef; + } + }; + + struct indices { + expr_ref_vector m_values; + expr* const* m_vars; + + indices(ast_manager& m, model& model, unsigned n, expr* const* vars): + m_values(m), m_vars(vars) { + expr_ref val(m); + for (unsigned i = 0; i < n; ++i) { + VERIFY(model.eval(vars[i], val)); + m_values.push_back(val); + } + } + }; + + ast_manager& m; + array_util a; + scoped_ptr m_var; + + imp(ast_manager& m): m(m), a(m) {} + ~imp() {} + + virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return false; + } + + bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + + TRACE("qe", tout << mk_pp(var, m) << "\n" << lits;); + m_var = alloc(contains_app, m, var); + + // reduce select-store redeces based on model. + // rw_cfg rw(m); + // rw(lits); + + // try first to solve for var. + if (solve_eq(model, vars, lits)) { + return true; + } + + app_ref_vector selects(m); + + // check that only non-select occurrences are in disequalities. + if (!check_diseqs(lits, selects)) { + TRACE("qe", tout << "Could not project " << mk_pp(var, m) << " for:\n" << lits << "\n";); + return false; + } + + // remove disequalities. + elim_diseqs(lits); + + // Ackerman reduction on remaining select occurrences + // either replace occurrences by model value or other node + // that is congruent to model value. + + ackermanize_select(model, selects, vars, lits); + + TRACE("qe", tout << selects << "\n" << lits << "\n";); + return true; + } + + void ackermanize_select(model& model, app_ref_vector const& selects, app_ref_vector& vars, expr_ref_vector& lits) { + expr_ref_vector vals(m), reps(m); + expr_ref val(m); + expr_safe_replace sub(m); + + if (selects.empty()) { + return; + } + + app_ref sel(m); + for (unsigned i = 0; i < selects.size(); ++i) { + sel = m.mk_fresh_const("sel", m.get_sort(selects[i])); + VERIFY (model.eval(selects[i], val)); + model.register_decl(sel->get_decl(), val); + vals.push_back(to_app(val)); + reps.push_back(val); // TODO: direct pass could handle nested selects. + vars.push_back(sel); + sub.insert(selects[i], val); + } + + sub(lits); + remove_true(lits); + project_plugin::partition_args(model, selects, lits); + project_plugin::partition_values(model, reps, lits); + } + + void remove_true(expr_ref_vector& lits) { + for (unsigned i = 0; i < lits.size(); ++i) { + if (m.is_true(lits[i].get())) { + project_plugin::erase(lits, i); + } + } + } + + bool contains_x(expr* e) { + return (*m_var)(e); + } + + void mk_eq(indices& x, indices y, expr_ref_vector& lits) { + unsigned n = x.m_values.size(); + for (unsigned j = 0; j < n; ++j) { + lits.push_back(m.mk_eq(x.m_vars[j], y.m_vars[j])); + } + } + + // check that x occurs only under selects or in disequalities. + bool check_diseqs(expr_ref_vector const& lits, app_ref_vector& selects) { + expr_mark mark; + ptr_vector todo; + app* e; + for (unsigned i = 0; i < lits.size(); ++i) { + e = to_app(lits[i]); + if (is_diseq_x(e)) { + continue; + } + if (contains_x(e)) { + todo.push_back(e); + } + } + while (!todo.empty()) { + e = todo.back(); + todo.pop_back(); + if (mark.is_marked(e)) { + continue; + } + mark.mark(e); + if (m_var->x() == e) { + return false; + } + unsigned start = 0; + if (a.is_select(e)) { + if (e->get_arg(0) == m_var->x()) { + start = 1; + selects.push_back(e); + } + } + for (unsigned i = start; i < e->get_num_args(); ++i) { + todo.push_back(to_app(e->get_arg(i))); + } + } + return true; + } + + void elim_diseqs(expr_ref_vector& lits) { + for (unsigned i = 0; i < lits.size(); ++i) { + if (is_diseq_x(lits[i].get())) { + project_plugin::erase(lits, i); + } + } + } + + bool is_update_x(app* e) { + do { + if (m_var->x() == e) { + return true; + } + if (a.is_store(e) && contains_x(e->get_arg(0))) { + for (unsigned i = 1; i < e->get_num_args(); ++i) { + if (contains_x(e->get_arg(i))) { + return false; + } + } + e = to_app(e->get_arg(0)); + continue; + } + } + while (false); + return false; + } + + bool is_diseq_x(expr* e) { + expr *f, * s, *t; + if (m.is_not(e, f) && m.is_eq(f, s, t)) { + if (contains_x(s) && !contains_x(t) && is_update_x(to_app(s))) return true; + if (contains_x(t) && !contains_x(s) && is_update_x(to_app(t))) return true; + } + return false; + } + + bool solve_eq(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + // find an equality to solve for. + expr* s, *t; + for (unsigned i = 0; i < lits.size(); ++i) { + if (m.is_eq(lits[i].get(), s, t)) { + vector idxs; + expr_ref save(m), back(m); + save = lits[i].get(); + back = lits.back(); + lits[i] = back; + lits.pop_back(); + unsigned sz = lits.size(); + if (contains_x(s) && !contains_x(t) && is_app(s)) { + if (solve(model, to_app(s), t, idxs, vars, lits)) { + return true; + } + } + else if (contains_x(t) && !contains_x(s) && is_app(t)) { + if (solve(model, to_app(t), s, idxs, vars, lits)) { + return true; + } + } + // put back the equality literal. + lits.resize(sz); + lits.push_back(back); + lits[i] = save; + } + // TBD: not distinct? + } + return false; + } + + bool solve(model& model, app* s, expr* t, vector& idxs, app_ref_vector& vars, expr_ref_vector& lits) { + SASSERT(contains_x(s)); + SASSERT(!contains_x(t)); + + if (s == m_var->x()) { + expr_ref result(s, m); + expr_ref_vector args(m); + sort* range = get_array_range(m.get_sort(s)); + for (unsigned i = 0; i < idxs.size(); ++i) { + app_ref var(m); + var = m.mk_fresh_const("value", range); + vars.push_back(var); + args.reset(); + args.push_back(result); + args.append(idxs[i].m_values.size(), idxs[i].m_vars); + args.push_back(var); + result = a.mk_store(args.size(), args.c_ptr()); + } + expr_safe_replace sub(m); + sub.insert(s, result); + for (unsigned i = 0; i < lits.size(); ++i) { + sub(lits[i].get(), result); + lits[i] = result; + } + return true; + } + + if (a.is_store(s)) { + unsigned n = s->get_num_args()-2; + indices idx(m, model, n, s->get_args()+1); + for (unsigned i = 1; i < n; ++i) { + if (contains_x(s->get_arg(i))) { + return false; + } + } + unsigned i; + expr_ref_vector args(m); + switch (contains(idx, idxs, i)) { + case l_true: + mk_eq(idx, idxs[i], lits); + return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits); + case l_false: + for (unsigned i = 0; i < idxs.size(); ++i) { + expr_ref_vector eqs(m); + mk_eq(idx, idxs[i], eqs); + lits.push_back(m.mk_not(mk_and(eqs))); // TBD: extract single index of difference based on model. + } + args.push_back(t); + args.append(n, s->get_args()+1); + lits.push_back(m.mk_eq(a.mk_select(args.size(), args.c_ptr()), s->get_arg(n+1))); + idxs.push_back(idx); + return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits); + case l_undef: + return false; + } + } + return false; + } + + lbool contains(indices const& idx, vector const& idxs, unsigned& j) { + for (unsigned i = 0; i < idxs.size(); ++i) { + switch (compare(idx, idxs[i])) { + case l_true: + j = i; + return l_true; + case l_false: + break; + case l_undef: + return l_undef; + } + } + return l_false; + } + + lbool compare(indices const& idx1, indices const& idx2) { + unsigned n = idx1.m_values.size(); + for (unsigned i = 0; i < n; ++i) { + switch (compare(idx1.m_values[i], idx2.m_values[i])) { + case l_true: + break; + case l_false: + return l_false; + case l_undef: + return l_undef; + } + } + return l_true; + } + + lbool compare(expr* val1, expr* val2) { + if (val1 == val2) { + return l_true; + } + if (is_uninterp(val1) || + is_uninterp(val2)) { + // TBD chase definition of nested array. + return l_undef; + } + return l_true; + } + }; + + + array_project_plugin::array_project_plugin(ast_manager& m) { + m_imp = alloc(imp, m); + } + + array_project_plugin::~array_project_plugin() { + dealloc(m_imp); + } + + bool array_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + return (*m_imp)(model, var, vars, lits); + } + + bool array_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return m_imp->solve(model, vars, lits); + } + + family_id array_project_plugin::get_family_id() { + return m_imp->a.get_family_id(); + } + +}; + diff --git a/src/qe/qe_arrays.h b/src/qe/qe_arrays.h new file mode 100644 index 000000000..182d82255 --- /dev/null +++ b/src/qe/qe_arrays.h @@ -0,0 +1,42 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_arrays.h + +Abstract: + + Model based projection for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + +Revision History: + +--*/ + + +#ifndef __QE_ARRAYS_H_ +#define __QE_ARRAYS_H_ + +#include "array_decl_plugin.h" +#include "qe_mbp.h" + +namespace qe { + + class array_project_plugin : public project_plugin { + struct imp; + imp* m_imp; + public: + array_project_plugin(ast_manager& m); + virtual ~array_project_plugin(); + 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(); + }; + +}; + +#endif diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp new file mode 100644 index 000000000..81001dea5 --- /dev/null +++ b/src/qe/qe_datatypes.cpp @@ -0,0 +1,312 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_datatypes.cpp + +Abstract: + + Simple projection function for algebraic datatypes. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + +Revision History: + +--*/ + +#include "qe_arith.h" +#include "ast_pp.h" +#include "th_rewriter.h" +#include "expr_functors.h" +#include "model_v2_pp.h" +#include "expr_safe_replace.h" +#include "obj_pair_hashtable.h" +#include "qe_datatypes.h" + +namespace qe { + + struct datatype_project_plugin::imp { + ast_manager& m; + datatype_util dt; + app_ref m_val; + scoped_ptr m_var; + + imp(ast_manager& m): + m(m), dt(m), m_val(m) {} + + virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return lift_foreign(vars, lits); + } + + bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + expr_ref val(m); + VERIFY(model.eval(var, val)); + SASSERT(is_app(val)); + TRACE("qe", tout << mk_pp(var, m) << " := " << val << "\n";); + m_val = to_app(val); + if (!dt.is_constructor(m_val)) { + // assert: var does not occur in lits. + return true; + } + m_var = alloc(contains_app, m, var); + + + try { + if (dt.is_recursive(m.get_sort(var))) { + project_rec(model, vars, lits); + } + else { + project_nonrec(model, vars, lits); + } + } + catch (cant_project) { + TRACE("qe", tout << "can't project:" << mk_pp(var, m) << "\n";); + return false; + } + return true; + } + + void project_nonrec(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + expr_ref tmp(m), val(m); + expr_ref_vector args(m); + app_ref arg(m); + SASSERT(dt.is_constructor(m_val)); + func_decl* f = m_val->get_decl(); + ptr_vector const& acc = *dt.get_constructor_accessors(f); + for (unsigned i = 0; i < acc.size(); ++i) { + arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range()); + model.register_decl(arg->get_decl(), m_val->get_arg(i)); + args.push_back(arg); + } + val = m.mk_app(f, args.size(), args.c_ptr()); + TRACE("qe", tout << mk_pp(m_var->x(), m) << " |-> " << val << "\n";); + reduce(val, lits); + } + + void project_rec(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + func_decl* f = m_val->get_decl(); + expr_ref rhs(m); + expr_ref_vector eqs(m); + for (unsigned i = 0; i < lits.size(); ++i) { + if (solve(model, vars, lits[i].get(), rhs, eqs)) { + project_plugin::erase(lits, i); + reduce(rhs, lits); + lits.append(eqs); + return; + } + } + + // otherwise, unfold the constructor associated with m_var + // once according to the model. In this way, selector-constructor + // redexes are reduced and disequalities are eventually solved + // by virtue of the constructors being different. + project_nonrec(model, vars, lits); + } + + void reduce(expr* val, expr_ref_vector& lits) { + expr_safe_replace sub(m); + th_rewriter rw(m); + expr_ref tmp(m); + sub.insert(m_var->x(), val); + TRACE("qe", tout << mk_pp(m_var->x(), m) << " = " << mk_pp(val, m) << "\n"; + tout << lits << "\n";); + for (unsigned i = 0; i < lits.size(); ++i) { + sub(lits[i].get(), tmp); + rw(tmp); + lits[i] = tmp; + } + } + + bool contains_x(expr* e) { + return (*m_var)(e); + } + + bool solve(model& model, app_ref_vector& vars, expr* fml, expr_ref& t, expr_ref_vector& eqs) { + expr* t1, *t2; + if (m.is_eq(fml, t1, t2)) { + if (contains_x(t1) && !contains_x(t2) && is_app(t1)) { + return solve(model, vars, to_app(t1), t2, t, eqs); + } + if (contains_x(t2) && !contains_x(t1) && is_app(t2)) { + return solve(model, vars, to_app(t2), t1, t, eqs); + } + } + if (m.is_not(fml, t1) && m.is_distinct(t1)) { + expr_ref eq = project_plugin::pick_equality(m, model, t1); + return solve(model, vars, eq, t, eqs); + } + return false; + } + + bool solve(model& model, app_ref_vector& vars, app* a, expr* b, expr_ref& t, expr_ref_vector& eqs) { + SASSERT(contains_x(a)); + SASSERT(!contains_x(b)); + if (m_var->x() == a) { + t = b; + return true; + } + if (!dt.is_constructor(a)) { + return false; + } + func_decl* c = a->get_decl(); + func_decl* rec = dt.get_constructor_recognizer(c); + ptr_vector const & acc = *dt.get_constructor_accessors(c); + SASSERT(acc.size() == a->get_num_args()); + // + // It suffices to solve just the first available equality. + // The others are determined by the first. + // + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* l = a->get_arg(i); + if (is_app(l) && contains_x(l)) { + expr_ref r(m); + r = access(c, i, acc, b); + if (solve(model, vars, to_app(l), r, t, eqs)) { + for (unsigned j = 0; j < c->get_arity(); ++j) { + if (i != j) { + eqs.push_back(m.mk_eq(access(c, j, acc, b), a->get_arg(j))); + } + } + if (!is_app_of(b, c)) { + eqs.push_back(m.mk_app(rec, b)); + } + + return true; + } + } + } + return false; + } + + + expr* access(func_decl* c, unsigned i, ptr_vector const& acc, expr* e) { + if (is_app_of(e,c)) { + return to_app(e)->get_arg(i); + } + else { + return m.mk_app(acc[i], e); + } + } + + bool lift_foreign(app_ref_vector const& vars, expr_ref_vector& lits) { + + bool reduced = false; + expr_mark visited; + expr_mark has_var; + bool inserted = false; + for (unsigned i = 0; i < vars.size(); ++i) { + if (m.is_bool(vars[i])) continue; + if (dt.is_datatype(m.get_sort(vars[i]))) continue; + inserted = true; + has_var.mark(vars[i]); + visited.mark(vars[i]); + } + if (inserted) { + for (unsigned i = 0; i < lits.size(); ++i) { + expr* e = lits[i].get(), *l, *r; + if (m.is_eq(e, l, r) && reduce_eq(visited, has_var, l, r, lits)) { + project_plugin::erase(lits, i); + reduced = true; + } + } + CTRACE("qe", reduced, tout << vars << "\n" << lits << "\n";); + } + return reduced; + } + + bool reduce_eq(expr_mark& has_var, expr_mark& visited, expr* l, expr* r, expr_ref_vector& lits) { + if (!is_app(l) || !is_app(r)) { + return false; + } + bool reduce = false; + if (dt.is_constructor(to_app(r)) && contains_foreign(has_var, visited, r)) { + std::swap(l, r); + reduce = true; + } + reduce |= dt.is_constructor(to_app(l)) && contains_foreign(has_var, visited, l); + if (!reduce) { + return false; + } + func_decl* c = to_app(l)->get_decl(); + ptr_vector const& acc = *dt.get_constructor_accessors(c); + if (!is_app_of(r, c)) { + lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r)); + } + for (unsigned i = 0; i < acc.size(); ++i) { + lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r))); + } + return true; + } + + + ptr_vector todo; + + bool contains_foreign(expr_mark& has_var, expr_mark& visited, expr* e) { + todo.push_back(e); + while (!todo.empty()) { + expr* _f = todo.back(); + if (visited.is_marked(_f)) { + todo.pop_back(); + continue; + } + if (!is_app(_f)) { + visited.mark(_f); + todo.pop_back(); + continue; + } + app* f = to_app(_f); + bool has_new = false, has_v = false; + for (unsigned i = 0; i < f->get_num_args(); ++i) { + expr* arg = f->get_arg(i); + if (!visited.is_marked(arg)) { + todo.push_back(arg); + has_new = true; + } + else { + has_v |= has_var.is_marked(arg); + } + } + if (has_new) { + continue; + } + todo.pop_back(); + if (has_v) { + has_var.mark(f); + } + TRACE("qe", tout << "contains: " << mk_pp(f, m) << " " << has_var.is_marked(f) << "\n";); + visited.mark(f); + } + TRACE("qe", tout << "contains: " << mk_pp(e, m) << " " << has_var.is_marked(e) << "\n";); + return has_var.is_marked(e); + } + + }; + + datatype_project_plugin::datatype_project_plugin(ast_manager& m) { + m_imp = alloc(imp, m); + } + + datatype_project_plugin::~datatype_project_plugin() { + dealloc(m_imp); + } + + bool datatype_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + return (*m_imp)(model, var, vars, lits); + } + + bool datatype_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return m_imp->solve(model, vars, lits); + } + + + family_id datatype_project_plugin::get_family_id() { + return m_imp->dt.get_family_id(); + } + +} + + + diff --git a/src/qe/qe_datatypes.h b/src/qe/qe_datatypes.h new file mode 100644 index 000000000..f616e7f2e --- /dev/null +++ b/src/qe/qe_datatypes.h @@ -0,0 +1,42 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_datatypes.h + +Abstract: + + Model based projection for algebraic datatypes + +Author: + + Nikolaj Bjorner (nbjorner) 2015-06-13 + +Revision History: + +--*/ + + +#ifndef __QE_DATATYPES_H_ +#define __QE_DATATYPES_H_ + +#include "datatype_decl_plugin.h" +#include "qe_mbp.h" + +namespace qe { + + class datatype_project_plugin : public project_plugin { + struct imp; + imp* m_imp; + public: + datatype_project_plugin(ast_manager& m); + virtual ~datatype_project_plugin(); + 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(); + }; + +}; + +#endif diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 9a981cc9b..aad802a2a 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -31,7 +31,6 @@ Revision History: #include "var_subst.h" #include "uint_set.h" #include "ast_util.h" -#include "qe_util.h" #include "th_rewriter.h" #include "for_each_expr.h" #include "expr_safe_replace.h" diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp new file mode 100644 index 000000000..c8ec34726 --- /dev/null +++ b/src/qe/qe_mbp.cpp @@ -0,0 +1,369 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_mbp.cpp + +Abstract: + + Model-based projection utilities + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-29 + +Revision History: + + +--*/ + +#include "qe_mbp.h" +#include "qe_arith.h" +#include "qe_arrays.h" +#include "qe_datatypes.h" +#include "expr_safe_replace.h" +#include "ast_pp.h" +#include "ast_util.h" +#include "th_rewriter.h" +#include "model_v2_pp.h" +#include "expr_functors.h" + + +using namespace qe; + + +/** + \brief return two terms that are equal in the model. + The distinct term t is false in model, so there + are at least two arguments of t that are equal in the model. +*/ +expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) { + SASSERT(m.is_distinct(t)); + expr_ref val(m); + expr_ref_vector vals(m); + obj_map val2expr; + app* alit = to_app(t); + for (unsigned i = 0; i < alit->get_num_args(); ++i) { + expr* e1 = alit->get_arg(i), *e2; + VERIFY(model.eval(e1, val)); + if (val2expr.find(val, e2)) { + return expr_ref(m.mk_eq(e1, e2), m); + } + val2expr.insert(val, e1); + vals.push_back(val); + } + UNREACHABLE(); + return expr_ref(0, m); +} + +void project_plugin::partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits) { + ast_manager& m = vals.get_manager(); + expr_ref val(m); + expr_ref_vector trail(m), reps(m); + obj_map roots; + for (unsigned i = 0; i < vals.size(); ++i) { + expr* v = vals[i], *root; + VERIFY (model.eval(v, val)); + if (roots.find(val, root)) { + lits.push_back(m.mk_eq(v, root)); + } + else { + roots.insert(val, v); + trail.push_back(val); + reps.push_back(v); + } + } + if (reps.size() > 1) { + lits.push_back(mk_distinct(reps)); + } +} + +void project_plugin::partition_args(model& model, app_ref_vector const& selects, expr_ref_vector& lits) { + ast_manager& m = selects.get_manager(); + if (selects.empty()) return; + unsigned num_args = selects[0]->get_decl()->get_arity(); + for (unsigned j = 1; j < num_args; ++j) { + expr_ref_vector args(m); + for (unsigned i = 0; i < selects.size(); ++i) { + args.push_back(selects[i]->get_arg(j)); + } + project_plugin::partition_values(model, args, lits); + } +} + +void project_plugin::erase(expr_ref_vector& lits, unsigned& i) { + lits[i] = lits.back(); + lits.pop_back(); + --i; +} + +void project_plugin::push_back(expr_ref_vector& lits, expr* e) { + if (lits.get_manager().is_true(e)) return; + lits.push_back(e); +} + + +class mbp::impl { + ast_manager& m; + ptr_vector m_plugins; + + void add_plugin(project_plugin* p) { + family_id fid = p->get_family_id(); + SASSERT(!m_plugins.get(fid, 0)); + m_plugins.setx(fid, p, 0); + } + + project_plugin* get_plugin(app* var) { + family_id fid = m.get_sort(var)->get_family_id(); + return m_plugins.get(fid, 0); + } + + bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + expr_mark is_var, is_rem; + if (vars.empty()) { + return false; + } + bool reduced = false; + for (unsigned i = 0; i < vars.size(); ++i) { + is_var.mark(vars[i].get()); + } + expr_ref tmp(m), t(m), v(m); + th_rewriter rw(m); + for (unsigned i = 0; i < lits.size(); ++i) { + expr* e = lits[i].get(), *l, *r; + if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) { + reduced = true; + lits[i] = lits.back(); + lits.pop_back(); + --i; + expr_safe_replace sub(m); + sub.insert(v, t); + is_rem.mark(v); + for (unsigned j = 0; j < lits.size(); ++j) { + sub(lits[j].get(), tmp); + rw(tmp); + lits[j] = tmp; + } + } + } + if (reduced) { + for (unsigned i = 0; i < vars.size(); ++i) { + if (is_rem.is_marked(vars[i].get())) { + vars[i] = vars.back(); + vars.pop_back(); + } + } + } + return reduced; + } + + bool reduce_eq(expr_mark& is_var, expr* l, expr* r, expr_ref& v, expr_ref& t) { + if (is_var.is_marked(r)) { + std::swap(l, r); + } + if (is_var.is_marked(l)) { + contains_app cont(m, to_app(l)); + if (!cont(r)) { + v = to_app(l); + t = r; + return true; + } + } + return false; + } + +public: + + void extract_literals(model& model, expr_ref_vector& fmls) { + expr_ref val(m); + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3; + if (m.is_not(fml, nfml) && m.is_distinct(nfml)) { + fmls[i] = project_plugin::pick_equality(m, model, nfml); + --i; + } + else if (m.is_or(fml)) { + for (unsigned j = 0; j < to_app(fml)->get_num_args(); ++j) { + VERIFY (model.eval(to_app(fml)->get_arg(j), val)); + if (m.is_true(val)) { + fmls[i] = to_app(fml)->get_arg(j); + --i; + break; + } + } + } + else if (m.is_and(fml)) { + fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); + project_plugin::erase(fmls, i); + } + else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { + VERIFY (model.eval(f1, val)); + if (m.is_false(val)) { + f1 = mk_not(m, f1); + f2 = mk_not(m, f2); + } + project_plugin::push_back(fmls, f1); + project_plugin::push_back(fmls, f2); + project_plugin::erase(fmls, i); + } + else if (m.is_implies(fml, f1, f2)) { + VERIFY (model.eval(f2, val)); + if (m.is_true(val)) { + project_plugin::push_back(fmls, f2); + } + else { + project_plugin::push_back(fmls, mk_not(m, f1)); + } + project_plugin::erase(fmls, i); + } + else if (m.is_ite(fml, f1, f2, f3)) { + VERIFY (model.eval(f1, val)); + if (m.is_true(val)) { + project_plugin::push_back(fmls, f2); + } + else { + project_plugin::push_back(fmls, f3); + } + project_plugin::erase(fmls, i); + } + else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) { + project_plugin::push_back(fmls, nfml); + project_plugin::erase(fmls, i); + } + else if (m.is_not(fml, nfml) && m.is_and(nfml)) { + for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) { + VERIFY (model.eval(to_app(nfml)->get_arg(j), val)); + if (m.is_false(val)) { + fmls[i] = mk_not(m, to_app(nfml)->get_arg(j)); + --i; + break; + } + } + } + else if (m.is_not(fml, nfml) && m.is_or(nfml)) { + for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) { + project_plugin::push_back(fmls, mk_not(m, to_app(nfml)->get_arg(j))); + } + project_plugin::erase(fmls, i); + } + else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { + VERIFY (model.eval(f1, val)); + if (m.is_true(val)) { + f2 = mk_not(m, f2); + } + else { + f1 = mk_not(m, f1); + } + project_plugin::push_back(fmls, f1); + project_plugin::push_back(fmls, f2); + project_plugin::erase(fmls, i); + } + else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) { + project_plugin::push_back(fmls, f1); + project_plugin::push_back(fmls, mk_not(m, f2)); + project_plugin::erase(fmls, i); + } + else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { + VERIFY (model.eval(f1, val)); + if (m.is_true(val)) { + project_plugin::push_back(fmls, mk_not(m, f2)); + } + else { + project_plugin::push_back(fmls, mk_not(m, f3)); + } + project_plugin::erase(fmls, i); + } + else { + // TBD other Boolean operations. + } + } + } + + impl(ast_manager& m):m(m) { + add_plugin(alloc(arith_project_plugin, m)); + add_plugin(alloc(datatype_project_plugin, m)); + add_plugin(alloc(array_project_plugin, m)); + } + + ~impl() { + std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc()); + } + + void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + extract_literals(model, fmls); + bool change = true; + while (change && !vars.empty()) { + change = solve(model, vars, fmls); + for (unsigned i = 0; i < m_plugins.size(); ++i) { + if (m_plugins[i] && m_plugins[i]->solve(model, vars, fmls)) { + change = true; + } + } + } + } + + void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { + expr_ref val(m), tmp(m); + app_ref var(m); + th_rewriter rw(m); + bool progress = true; + while (progress && !vars.empty()) { + preprocess_solve(model, vars, fmls); + app_ref_vector new_vars(m); + progress = false; + while (!vars.empty()) { + var = vars.back(); + vars.pop_back(); + project_plugin* p = get_plugin(var); + if (p && (*p)(model, var, vars, fmls)) { + progress = true; + } + else { + new_vars.push_back(var); + } + } + if (!progress && !new_vars.empty() && force_elim) { + var = new_vars.back(); + new_vars.pop_back(); + expr_safe_replace sub(m); + VERIFY(model.eval(var, val)); + sub.insert(var, val); + for (unsigned i = 0; i < fmls.size(); ++i) { + sub(fmls[i].get(), tmp); + rw(tmp); + if (m.is_true(tmp)) { + fmls[i] = fmls.back(); + fmls.pop_back(); + --i; + } + else { + fmls[i] = tmp; + } + } + progress = true; + } + vars.append(new_vars); + } + } +}; + +mbp::mbp(ast_manager& m) { + m_impl = alloc(impl, m); +} + +mbp::~mbp() { + dealloc(m_impl); +} + +void mbp::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) { + (*m_impl)(force_elim, vars, mdl, fmls); +} + +void mbp::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + m_impl->preprocess_solve(model, vars, fmls); +} + +void mbp::extract_literals(model& model, expr_ref_vector& lits) { + m_impl->extract_literals(model, lits); +} diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h new file mode 100644 index 000000000..5b4c59762 --- /dev/null +++ b/src/qe/qe_mbp.h @@ -0,0 +1,76 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qe_mbp.h + +Abstract: + + Model-based projection utilities + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-28 + +Revision History: + + +--*/ + +#ifndef __QE_MBP_H__ +#define __QE_MBP_H__ + +#include "ast.h" +#include "params.h" +#include "model.h" + + +namespace qe { + + struct cant_project {}; + + class project_plugin { + public: + virtual ~project_plugin() {} + virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0; + virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0; + virtual family_id get_family_id() = 0; + + static expr_ref pick_equality(ast_manager& m, model& model, expr* t); + static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits); + static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits); + static void erase(expr_ref_vector& lits, unsigned& i); + static void push_back(expr_ref_vector& lits, expr* lit); + }; + + class mbp { + class impl; + impl * m_impl; + public: + mbp(ast_manager& m); + + ~mbp(); + + /** + \brief + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. + */ + void operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls); + + /** + \brief + Solve as many variables as possible using "cheap" quantifier elimination" + */ + void solve(model& model, app_ref_vector& vars, expr_ref_vector& lits); + + /** + \brief + Extract literals from formulas based on model. + */ + void extract_literals(model& model, expr_ref_vector& lits); + }; +} + +#endif