From 7714d05c1ab45182f98814918b0766b3dcc9a01a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jun 2018 18:30:36 -0700 Subject: [PATCH] fill out qe_solve_plugin functionality Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.h | 2 + src/qe/qe_lite.cpp | 169 +++++---------------------------- src/qe/qe_solve_plugin.cpp | 125 +++++++++++++++++++++--- src/qe/qe_solve_plugin.h | 6 +- src/util/plugin_manager.h | 5 + 5 files changed, 144 insertions(+), 163 deletions(-) diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 88b50af82..17602efcf 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -358,8 +358,10 @@ namespace datatype { bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); } bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); } + bool is_constructor(expr* e) const { return is_app(e) && is_constructor(to_app(e)); } bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);} bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);} + bool is_is(expr * e) const { return is_app(e) && is_is(to_app(e)); } bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index c027d2d07..3b8d41316 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -36,6 +36,7 @@ Revision History: #include "ast/datatype_decl_plugin.h" #include "qe/qe_vartest.h" +#include "qe/qe_solve_plugin.h" namespace eq { @@ -72,6 +73,7 @@ namespace eq { beta_reducer m_subst; expr_ref_vector m_subst_map; expr_ref_vector m_new_exprs; + plugin_manager m_solvers; ptr_vector m_map; int_vector m_pos2var; @@ -221,97 +223,6 @@ namespace eq { } } - bool is_invertible_const(bool is_int, expr* x, rational& a_val) { - expr* y; - if (a.is_uminus(x, y) && is_invertible_const(is_int, y, a_val)) { - a_val.neg(); - return true; - } - else if (a.is_numeral(x, a_val) && !a_val.is_zero()) { - if (!is_int || a_val.is_one() || a_val.is_minus_one()) { - return true; - } - } - return false; - } - - bool is_invertible_mul(bool is_int, expr*& arg, rational& a_val) { - if (is_variable(arg)) { - a_val = rational(1); - return true; - } - expr* x, *y; - if (a.is_mul(arg, x, y)) { - if (is_variable(x) && is_invertible_const(is_int, y, a_val)) { - arg = x; - return true; - } - if (is_variable(y) && is_invertible_const(is_int, x, a_val)) { - arg = y; - return true; - } - } - return false; - } - - typedef std::pair signed_expr; - - expr_ref solve_arith(bool is_int, rational const& r, bool sign, svector const& exprs) { - expr_ref_vector result(m); - for (unsigned i = 0; i < exprs.size(); ++i) { - bool sign2 = exprs[i].first; - expr* e = exprs[i].second; - rational r2(r); - if (sign == sign2) { - r2.neg(); - } - if (!r2.is_one()) { - result.push_back(a.mk_mul(a.mk_numeral(r2, is_int), e)); - } - else { - result.push_back(e); - } - } - return expr_ref(a.mk_add(result.size(), result.c_ptr()), m); - } - - bool solve_arith(expr* lhs, expr* rhs, ptr_vector& vs, expr_ref_vector& ts) { - if (!a.is_int(lhs) && !a.is_real(rhs)) { - return false; - } - rational a_val; - bool is_int = a.is_int(lhs); - svector todo, done; - todo.push_back(std::make_pair(true, lhs)); - todo.push_back(std::make_pair(false, rhs)); - while (!todo.empty()) { - expr* e = todo.back().second; - bool sign = todo.back().first; - todo.pop_back(); - if (a.is_add(e)) { - for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - todo.push_back(std::make_pair(sign, to_app(e)->get_arg(i))); - } - } - else if (is_invertible_mul(is_int, e, a_val)) { - done.append(todo); - vs.push_back(to_var(e)); - a_val = rational(1)/a_val; - ts.push_back(solve_arith(is_int, a_val, sign, done)); - TRACE("qe_lite", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << mk_pp(ts.back(), m) << "\n";); - return true; - } - else { - done.push_back(std::make_pair(sign, e)); - } - } - return false; - } - - bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { - return solve_arith(lhs, rhs, vs, ts); - } - bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector& vs, expr_ref_vector& ts) { if (!is_variable(lhs)) { std::swap(lhs, rhs); @@ -343,65 +254,25 @@ namespace eq { */ bool is_var_eq(expr * e, ptr_vector& vs, expr_ref_vector & ts) { - expr* lhs, *rhs; - var* v; + expr* lhs = nullptr, *rhs = nullptr; // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases + if (m.is_eq(e, lhs, rhs) && trivial_solve(lhs, rhs, e, vs, ts)) { + return true; + } + family_id fid = get_sort(e)->get_family_id(); if (m.is_eq(e, lhs, rhs)) { - // (iff (not VAR) t) (iff t (not VAR)) cases - if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { - if (!is_neg_var(m, lhs, v)) { - std::swap(lhs, rhs); - } - if (!is_neg_var(m, lhs, v)) { - return false; - } - vs.push_back(v); - ts.push_back(m.mk_not(rhs)); - TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); + fid = get_sort(lhs)->get_family_id(); + } + qe::solve_plugin* p = m_solvers.get_plugin(fid); + if (p) { + expr_ref res = (*p)(e); + if (res != e && m.is_eq(res, lhs, rhs) && is_variable(lhs)) { + vs.push_back(to_var(lhs)); + ts.push_back(rhs); return true; } - if (trivial_solve(lhs, rhs, e, vs, ts)) { - return true; - } - if (arith_solve(lhs, rhs, e, vs, ts)) { - return true; - } - return false; } - - // (ite cond (= VAR t) (= VAR t2)) case - expr* cond, *e2, *e3; - if (m.is_ite(e, cond, e2, e3)) { - if (is_var_eq(e2, vs, ts)) { - expr_ref_vector ts2(m); - ptr_vector vs2; - if (is_var_eq(e3, vs2, ts2) && same_vars(vs, vs2)) { - for (unsigned i = 0; i < vs.size(); ++i) { - ts[i] = m.mk_ite(cond, ts[i].get(), ts2[i].get()); - } - return true; - } - } - return false; - } - - // VAR = true case - if (is_variable(e)) { - ts.push_back(m.mk_true()); - vs.push_back(to_var(e)); - TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); - return true; - } - - // VAR = false case - if (is_neg_var(m, e, v)) { - ts.push_back(m.mk_false()); - vs.push_back(v); - TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); - return true; - } - return false; } @@ -785,9 +656,15 @@ namespace eq { m_new_exprs(m), m_new_args(m), m_rewriter(m), - m_params(p) {} + m_params(p) { + } - void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} + void set_is_variable_proc(is_variable_proc& proc) { + m_is_variable = &proc; + m_solvers.reset(); + m_solvers.register_plugin(qe::mk_arith_solve_plugin(m, proc)); + m_solvers.register_plugin(qe::mk_basic_solve_plugin(m, proc)); + } void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { TRACE("qe_lite", tout << mk_pp(q, m) << "\n";); diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp index bbaf15325..ad4a03b5d 100644 --- a/src/qe/qe_solve_plugin.cpp +++ b/src/qe/qe_solve_plugin.cpp @@ -19,6 +19,7 @@ Revision History: --*/ #include "ast/arith_decl_plugin.h" +#include "ast/datatype_decl_plugin.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "qe/qe_solve_plugin.h" @@ -65,7 +66,7 @@ namespace qe { /** * \brief return true if lhs = rhs can be solved as v = t, where v is a variable. */ - bool solve_arith(expr* lhs, expr* rhs, expr_ref& v, expr_ref& t) { + bool solve(expr* lhs, expr* rhs, expr_ref& v, expr_ref& t) { if (!a.is_int(lhs) && !a.is_real(rhs)) { return false; } @@ -83,6 +84,16 @@ namespace qe { todo.push_back(std::make_pair(sign, e)); } } + else if (a.is_sub(e)) { + app* sub = to_app(e); + todo.push_back(std::make_pair(sign, sub->get_arg(0))); + for (unsigned i = 1; i < sub->get_num_args(); ++i) { + todo.push_back(std::make_pair(!sign, sub->get_arg(i))); + } + } + else if (a.is_uminus(e)) { + todo.push_back(std::make_pair(!sign, to_app(e)->get_arg(0))); + } else if (is_invertible_mul(is_int, e, a_val)) { done.append(todo); v = e; @@ -98,7 +109,7 @@ namespace qe { return false; } - // can we solve for a variable by ... + // is x a constant and can we safely divide by x to solve for a variable? bool is_invertible_const(bool is_int, expr* x, rational& a_val) { expr* y; if (a.is_uminus(x, y) && is_invertible_const(is_int, y, a_val)) { @@ -113,6 +124,8 @@ namespace qe { return false; } + // is arg of the form a_val * v, where a_val + // is a constant that we can safely divide by. bool is_invertible_mul(bool is_int, expr*& arg, rational& a_val) { if (is_variable(arg)) { a_val = rational(1); @@ -133,10 +146,11 @@ namespace qe { } - expr_ref mk_eq_core (expr *_e1, expr *_e2) { - expr *e1, *e2; - e1 = _e1; - e2 = _e2; + expr_ref mk_eq_core (expr *e1, expr *e2) { + expr_ref v(m), t(m); + if (solve(e1, e2, v, t)) { + return expr_ref(m.mk_eq(v, t), m); + } if (a.is_zero(e1)) { std::swap(e1, e2); @@ -257,6 +271,90 @@ namespace qe { } }; + class basic_solve_plugin : public solve_plugin { + public: + basic_solve_plugin(ast_manager& m, is_variable_proc& is_var): + solve_plugin(m, m.get_basic_family_id(), is_var) {} + + expr_ref solve(expr *atom, bool is_pos) override { + expr_ref res(atom, m); + expr* lhs = nullptr, *rhs = nullptr, *n = nullptr; + if (m.is_eq(atom, lhs, rhs)) { + if (m.is_not(lhs, n) && is_variable(n)) { + res = m.mk_eq(n, mk_not(m, rhs)); + } + else if (m.is_not(rhs, n) && is_variable(n)) { + res = m.mk_eq(n, mk_not(m, lhs)); + } + else if (is_variable(rhs) && !is_variable(lhs)) { + res = m.mk_eq(rhs, lhs); + } + } + // (ite cond (= VAR t) (= VAR t2)) case + expr* cond = nullptr, *th = nullptr, *el = nullptr; + if (m.is_ite(atom, cond, th, el)) { + expr_ref r1 = solve(th, true); + expr_ref r2 = solve(el, true); + expr* v1 = nullptr, *t1 = nullptr, *v2 = nullptr, *t2 = nullptr; + if (m.is_eq(r1, v1, t1) && m.is_eq(r2, v2, t2) && v1 == v2) { + res = m.mk_eq(v1, m.mk_ite(cond, t1, t2)); + } + } + + if (is_variable(atom) && m.is_bool(atom)) { + res = m.mk_eq(atom, m.mk_bool_val(is_pos)); + return res; + } + + return is_pos ? res : mk_not(res); + } + }; + + class dt_solve_plugin : public solve_plugin { + datatype_util dt; + public: + dt_solve_plugin(ast_manager& m, is_variable_proc& is_var): + solve_plugin(m, m.get_family_id("datatype"), is_var), + dt(m) {} + + expr_ref solve(expr *atom, bool is_pos) override { + expr_ref res(atom, m); + expr* lhs = nullptr, *rhs = nullptr; + if (m.is_eq(atom, lhs, rhs)) { + if (dt.is_constructor(rhs)) { + std::swap(lhs, rhs); + } + if (dt.is_constructor(lhs) && dt.is_constructor(rhs)) { + app* l = to_app(lhs), *r = to_app(rhs); + if (l->get_decl() == r->get_decl()) { + expr_ref_vector eqs(m); + for (unsigned i = 0, sz = l->get_num_args(); i < sz; ++i) { + eqs.push_back(m.mk_eq(l->get_arg(i), r->get_arg(i))); + } + res = mk_and(eqs); + } + else { + res = m.mk_false(); + } + } + else if (dt.is_constructor(lhs)) { + app* l = to_app(lhs); + func_decl* d = l->get_decl(); + expr_ref_vector conjs(m); + conjs.push_back(dt.mk_is(d, rhs)); + ptr_vector const& acc = *dt.get_constructor_accessors(d); + for (unsigned i = 0; i < acc.size(); ++i) { + conjs.push_back(m.mk_eq(l->get_arg(i), m.mk_app(acc[i], rhs))); + } + res = mk_and(conjs); + } + } + // TBD: can also solve for is_nil(x) by x = nil + // + return is_pos ? res : mk_not(res); + } + }; + class bv_solve_plugin : public solve_plugin { public: bv_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("bv"), is_var) {} @@ -266,15 +364,6 @@ namespace qe { } }; - class dt_solve_plugin : public solve_plugin { - public: - dt_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("dt"), is_var) {} - expr_ref solve(expr *atom, bool is_pos) override { - expr_ref res(atom, m); - return is_pos ? res : mk_not(res); - } - }; - class array_solve_plugin : public solve_plugin { public: array_solve_plugin(ast_manager& m, is_variable_proc& is_var): solve_plugin(m, m.get_family_id("array"), is_var) {} @@ -284,6 +373,9 @@ namespace qe { } }; + solve_plugin* mk_basic_solve_plugin(ast_manager& m, is_variable_proc& is_var) { + return alloc(basic_solve_plugin, m, is_var); + } solve_plugin* mk_arith_solve_plugin(ast_manager& m, is_variable_proc& is_var) { return alloc(arith_solve_plugin, m, is_var); @@ -293,6 +385,7 @@ namespace qe { return alloc(dt_solve_plugin, m, is_var); } +#if 0 solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var) { return alloc(bv_solve_plugin, m, is_var); } @@ -300,4 +393,6 @@ namespace qe { solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var) { return alloc(array_solve_plugin, m, is_var); } +#endif + } diff --git a/src/qe/qe_solve_plugin.h b/src/qe/qe_solve_plugin.h index 064d3b84d..571d568f1 100644 --- a/src/qe/qe_solve_plugin.h +++ b/src/qe/qe_solve_plugin.h @@ -42,11 +42,13 @@ namespace qe { expr_ref operator() (expr *lit); }; + solve_plugin* mk_basic_solve_plugin(ast_manager& m, is_variable_proc& is_var); + solve_plugin* mk_arith_solve_plugin(ast_manager& m, is_variable_proc& is_var); solve_plugin* mk_dt_solve_plugin(ast_manager& m, is_variable_proc& is_var); - solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var); + // solve_plugin* mk_bv_solve_plugin(ast_manager& m, is_variable_proc& is_var); - solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var); + // solve_plugin* mk_array_solve_plugin(ast_manager& m, is_variable_proc& is_var); } diff --git a/src/util/plugin_manager.h b/src/util/plugin_manager.h index c8908fd57..2c4223eeb 100644 --- a/src/util/plugin_manager.h +++ b/src/util/plugin_manager.h @@ -27,7 +27,12 @@ class plugin_manager { ptr_vector m_plugins; public: ~plugin_manager() { + reset(); + } + + void reset() { std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc()); + release(); } /**