From 76417fa3b6a26cdbe83e98caa040f1d7d59f4180 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Jun 2018 17:06:56 -0700 Subject: [PATCH] fleshing out reduce-invertible tactic Signed-off-by: Nikolaj Bjorner --- src/tactic/core/CMakeLists.txt | 1 + src/tactic/core/reduce_invertible_tactic.cpp | 185 ++++++++++++++++--- 2 files changed, 156 insertions(+), 30 deletions(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 9611fa513..44284b625 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -43,6 +43,7 @@ z3_add_component(core_tactics pb_preprocess_tactic.h propagate_values_tactic.h reduce_args_tactic.h + reduce_invertible_tactic.h simplify_tactic.h solve_eqs_tactic.h split_clause_tactic.h diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 26d10b9f8..f08892be3 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -22,6 +22,7 @@ Notes: #include "util/cooperate.h" #include "ast/bv_decl_plugin.h" +#include "ast/ast_pp.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/rewriter_def.h" #include "tactic/tactic.h" @@ -48,28 +49,29 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override { TRACE("reduce_invertible", g->display(tout);); tactic_report report("reduce-invertible", *g); + m_inverted.reset(); + m_parents.reset(); collect_parents(g); collect_occs occs; obj_hashtable vars; generic_model_converter_ref mc; - //occs(*g, vars); + occs(*g, vars); expr_safe_replace sub(m); - expr_ref p(m); + expr_ref p(m), new_v(m); for (expr* v : vars) { - if (is_invertible(v, p, &mc)) { - sub.insert(v, p); + if (is_invertible(v, p, new_v, &mc)) { + mark_inverted(p); + sub.insert(p, new_v); } } - if (sub.empty()) { - result.push_back(g.get()); - return; - } + reduce_q_rw rw(*this); unsigned sz = g->size(); for (unsigned idx = 0; idx < sz; idx++) { checkpoint(); expr* f = g->form(idx); expr_ref f_new(m); sub(f, f_new); + rw(f_new, f_new); proof_ref new_pr(m); if (f == f_new) continue; if (g->proofs_enabled()) { @@ -77,7 +79,8 @@ public: new_pr = m.mk_modus_ponens(pr, new_pr); } g->update(idx, f_new, new_pr, g->dep(idx)); - } + } + if (mc) g->add(mc.get()); result.push_back(g.get()); g->inc_depth(); } @@ -93,6 +96,27 @@ private: cooperate("reduce-invertible"); } + expr_mark m_inverted; + void mark_inverted(expr *p) { + ptr_buffer todo; + todo.push_back(p); + while (!todo.empty()) { + p = todo.back(); + todo.pop_back(); + if (!m_inverted.is_marked(p)) { + m_inverted.mark(p, true); + if (is_app(p)) { + for (expr* arg : *to_app(p)) { + todo.push_back(arg); + } + } + else if (is_quantifier(p)) { + todo.push_back(to_quantifier(p)->get_expr()); + } + } + } + } + // store up to two parents of expression. struct parents { parents(): m_p1(nullptr), m_p2(nullptr) {} @@ -105,8 +129,8 @@ private: parent_collector(reduce_invertible_tactic& c):c(c) {} void operator()(app* n) { for (expr* arg : *n) { - c.m_parents.reserve(n->get_id() + 1, parents()); - parents& p = c.m_parents[n->get_id()]; + c.m_parents.reserve(arg->get_id() + 1, parents()); + parents& p = c.m_parents[arg->get_id()]; if (!p.m_p1) p.m_p1 = n; else p.m_p2 = n; } } @@ -114,7 +138,6 @@ private: }; void collect_parents(goal_ref const& g) { - m_parents.reset(); parent_collector proc(*this); expr_fast_mark1 visited; unsigned sz = g->size(); @@ -130,17 +153,18 @@ private: // TBD: could be made to be recursive, by walking multiple layers of parents. - bool is_invertible(expr* v, expr_ref& new_v, generic_model_converter_ref* mc) { - expr* p1 = m_parents[v->get_id()].m_p1; - if (m_parents[v->get_id()].m_p2 || !p1) return false; - - if (m_bv.is_bv_add(p1)) { + bool is_invertible(expr* v, expr_ref& p, expr_ref& new_v, generic_model_converter_ref* mc) { + p = m_parents[v->get_id()].m_p1; + if (m_parents[v->get_id()].m_p2 || !p) return false; + if (m_inverted.is_marked(p)) return false; + if (mc && !is_ground(p)) return false; + if (m_bv.is_bv_add(p)) { if (mc) { ensure_mc(mc); // if we solve for v' := v + t // then the value for v is v' - t expr_ref def(v, m); - for (expr* arg : *to_app(p1)) { + for (expr* arg : *to_app(p)) { if (arg != v) def = m_bv.mk_bv_sub(def, arg); } (*mc)->add(v, def); @@ -148,23 +172,96 @@ private: new_v = v; return true; } - if (m_bv.is_bv_mul(p1)) { + if (m_bv.is_bv_mul(p)) { + + expr_ref rest(m); + for (expr* arg : *to_app(p)) { + if (arg != v) + if (rest) + rest = m_bv.mk_bv_mul(rest, arg); + else + rest = arg; + } + if (!rest) return false; + // if multiplier by odd number, then just return division. // if general multiplier, then create case split on // divisbility of 2 // v * t -> if (t & 0x1) v / t (if (!(t & 0x1) && (t & 0x3)) .. + + unsigned sz = m_bv.get_bv_size(p); + expr_ref bit1(m_bv.mk_numeral(1, 1), m); + new_v = m_bv.mk_numeral(0, sz); + for (unsigned i = sz; i-- > 0; ) { + expr_ref extr_i(m_bv.mk_extract(i, i, rest), m); + expr_ref cond(m.mk_eq(extr_i, bit1), m); + expr_ref part(v, m); + if (i > 0) { + part = m_bv.mk_concat(m_bv.mk_extract(sz-1, i, v), m_bv.mk_numeral(0, i)); + } + new_v = m.mk_ite(cond, part, new_v); + } + + if (mc) { + ensure_mc(mc); + // TBD: represent inverse + } + return true; } - if (m_bv.is_bv_xor(p1)) { + if (m_bv.is_bv_xor(p)) { + if (mc) { + ensure_mc(mc); + (*mc)->add(v, p); + } + new_v = v; + return true; + } + if (m_bv.is_bv_sub(p)) { + + } + if (m_bv.is_bv_neg(p)) { + + } + if (m_bv.is_bv_udivi(p)) { + } + // sdivi, sremi, uremi, smodi + + expr* e1 = nullptr, *e2 = nullptr; + if (m.is_eq(p, e1, e2)) { + if (mc && m_bv.is_bv(e1)) { + if (!is_ground(p)) return false; + ensure_mc(mc); + new_v = m.mk_fresh_const("eq", m.mk_bool_sort()); + expr* other = (v == e1) ? e2 : e1; + (*mc)->hide(new_v); + (*mc)->add(v, m.mk_ite(new_v, other, m_bv.mk_bv_neg(other))); + return true; + } + else if (mc) { + // diagonal functions for other types depend on theory. + return false; + } + else if (is_var(v) && non_singleton_sort(m.get_sort(v))) { + new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort()); + return true; + } } return false; } - struct reduce_q_cfg : public default_rewriter_cfg { + bool non_singleton_sort(sort* s) { + if (m_bv.is_bv_sort(s) && m_bv.get_bv_size(s) > 0) return true; + if (m.is_bool(s)) return true; + // TBD: add arithmetic and other relevant theories. + return false; + } + + struct reduce_q_rw_cfg : public default_rewriter_cfg { ast_manager& m; reduce_invertible_tactic& t; - reduce_q_cfg(reduce_invertible_tactic& t): m(t.m), t(t) {} + reduce_q_rw_cfg(reduce_invertible_tactic& t): m(t.m), t(t) {} bool reduce_quantifier(quantifier * old_q, expr * new_body, @@ -172,30 +269,49 @@ private: expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { + if (is_lambda(old_q)) return false; + if (has_quantifiers(new_body)) return false; ref_buffer vars(m); + ptr_buffer new_sorts; unsigned n = old_q->get_num_decls(); for (unsigned i = 0; i < n; ++i) { - vars.push_back(m.mk_var(n - i - 1, old_q->get_decl_sort(i))); + sort* srt = old_q->get_decl_sort(i); + vars.push_back(m.mk_var(n - i - 1, srt)); + new_sorts.push_back(srt); } // for each variable, collect parents, // ensure they are in uniqe location and not under other quantifiers. // if they are invertible, then produce inverting expression. // expr_safe_replace sub(m); + t.m_parents.reset(); + t.m_inverted.reset(); + expr_ref p(m), new_v(m); + { - t.m_parents.reset(); - expr_ref p(m); parent_collector proc(t); expr_fast_mark1 visited; quick_for_each_expr(proc, visited, new_body); - for (var* v : vars) { - if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, nullptr)) { - sub.insert(v, p); - } + } + bool has_new_var = false; + for (unsigned i = 0; i < vars.size(); ++i) { + var* v = vars[i]; + if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr)) { + t.mark_inverted(p); + sub.insert(p, new_v); + new_sorts[i] = m.get_sort(new_v); + has_new_var |= new_v != v; } } + if (has_new_var) { + sub(new_body, result); + result = m.mk_quantifier(old_q->get_kind(), new_sorts.size(), new_sorts.c_ptr(), old_q->get_decl_names(), result); + result_pr = nullptr; + return true; + } if (!sub.empty()) { sub(new_body, result); + result = m.update_quantifier(old_q, old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns, result); result_pr = nullptr; return true; } @@ -203,10 +319,19 @@ private: } bool occurs_under_nested_q(var* v, expr* body) { - return !has_quantifiers(body); + return has_quantifiers(body); } }; + struct reduce_q_rw : rewriter_tpl { + reduce_q_rw_cfg m_cfg; + public: + reduce_q_rw(reduce_invertible_tactic& t): + rewriter_tpl(t.m, false, m_cfg), + m_cfg(t) {} + }; + + }; tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const &) {