From ce04c18a7a8965ffc1642e56779e1e5db9c6d750 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Aug 2017 22:14:13 -0700 Subject: [PATCH] trying to get rid of last simplifier dependency in macros Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/fpa2bv_converter.h | 4 +- src/ast/macros/macro_manager.cpp | 159 ++++++++++++++++++++---- src/ast/macros/macro_manager.h | 14 ++- src/ast/rewriter/poly_rewriter_def.h | 4 + src/muz/pdr/pdr_util.h | 2 +- src/muz/rel/dl_bound_relation.cpp | 2 +- src/muz/rel/dl_bound_relation.h | 3 +- src/smt/asserted_formulas.cpp | 2 +- src/tactic/ufbv/macro_finder_tactic.cpp | 2 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 2 +- 10 files changed, 158 insertions(+), 36 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 19a52dd23..1e3e5d9b3 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -29,7 +29,7 @@ Notes: #include "ast/dl_decl_plugin.h" #include "ast/pb_decl_plugin.h" #include "ast/seq_decl_plugin.h" -#include "ast/simplifier/basic_simplifier_plugin.h" +#include "ast/rewriter/bool_rewriter.h" class fpa2bv_converter { public: @@ -39,7 +39,7 @@ public: protected: ast_manager & m; - basic_simplifier_plugin m_simp; + bool_rewriter m_simp; fpa_util m_util; bv_util m_bv_util; arith_util m_arith_util; diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index f26a87445..70434435b 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -22,12 +22,14 @@ Revision History: #include "ast/macros/macro_manager.h" #include "ast/for_each_expr.h" #include "ast/rewriter/var_subst.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" #include "ast/recurse_expr_def.h" -macro_manager::macro_manager(ast_manager & m, simplifier & s): - m_manager(m), - m_simplifier(s), + +macro_manager::macro_manager(ast_manager & m): + m(m), m_util(m), m_decls(m), m_macros(m), @@ -60,12 +62,12 @@ void macro_manager::restore_decls(unsigned old_sz) { for (unsigned i = old_sz; i < sz; i++) { m_decl2macro.erase(m_decls.get(i)); m_deps.erase(m_decls.get(i)); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_decl2macro_pr.erase(m_decls.get(i)); } m_decls.shrink(old_sz); m_macros.shrink(old_sz); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_macro_prs.shrink(old_sz); } @@ -88,8 +90,8 @@ void macro_manager::reset() { m_deps.reset(); } -bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) { - TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(m, m_manager) << "\n";); +bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr) { + TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(q, m) << "\n";); // if we already have a macro for f then return false; if (m_decls.contains(f)) { @@ -99,7 +101,7 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) { app * head; expr * definition; - get_head_def(m, f, head, definition); + get_head_def(q, f, head, definition); func_decl_set * s = m_deps.mk_func_decl_set(); m_deps.collect_func_decls(definition, s); @@ -108,10 +110,10 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) { } // add macro - m_decl2macro.insert(f, m); + m_decl2macro.insert(f, q); m_decls.push_back(f); - m_macros.push_back(m); - if (m_manager.proofs_enabled()) { + m_macros.push_back(q); + if (m.proofs_enabled()) { m_macro_prs.push_back(pr); m_decl2macro_pr.insert(f, pr); } @@ -152,7 +154,7 @@ void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) { void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const { app * body = to_app(q->get_expr()); - SASSERT(m_manager.is_eq(body) || m_manager.is_iff(body)); + SASSERT(m.is_eq(body) || m.is_iff(body)); expr * lhs = to_app(body)->get_arg(0); expr * rhs = to_app(body)->get_arg(1); SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d)); @@ -177,7 +179,7 @@ void macro_manager::display(std::ostream & out) { expr * def; get_head_def(q, f, head, def); SASSERT(q); - out << mk_pp(head, m_manager) << " ->\n" << mk_pp(def, m_manager) << "\n"; + out << mk_pp(head, m) << " ->\n" << mk_pp(def, m) << "\n"; } } @@ -188,12 +190,115 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter expr * def; get_head_def(q, f, head, def); TRACE("macro_bug", - tout << f->get_name() << "\n" << mk_pp(head, m_manager) << "\n" << mk_pp(q, m_manager) << "\n";); + tout << f->get_name() << "\n" << mk_pp(head, m) << "\n" << mk_pp(q, m) << "\n";); m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp); return f; } -macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm, simplifier & s): +struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { + ast_manager& m; + macro_manager& mm; + expr_ref_vector m_trail; + + macro_expander_cfg(ast_manager& m, macro_manager& mm): + m(m), + mm(mm), + m_trail(m) + {} + + bool rewrite_patterns() const { return false; } + bool flat_assoc(func_decl * f) const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result_pr = 0; + return BR_FAILED; + } + + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + + // If a macro was expanded in a pattern, we must erase it since it may not be a valid pattern anymore. + // The MAM assumes valid patterns, and it crashes if invalid patterns are provided. + // For example, it will crash if the pattern does not contain all variables. + // + // Alternative solution: use pattern_validation to check if the pattern is still valid. + // I'm not sure if this is a good solution, since the pattern may be meaningless after the macro expansion. + // So, I'm just erasing them. + + bool erase_patterns = false; + for (unsigned i = 0; !erase_patterns && i < old_q->get_num_patterns(); i++) { + if (old_q->get_pattern(i) != new_patterns[i]) + erase_patterns = true; + } + for (unsigned i = 0; !erase_patterns && i < old_q->get_num_no_patterns(); i++) { + if (old_q->get_no_pattern(i) != new_no_patterns[i]) + erase_patterns = true; + } + if (erase_patterns) { + result = m.update_quantifier(old_q, 0, 0, 0, 0, new_body); + } + return erase_patterns; + } + + bool get_subst(expr * _n, expr* & r, proof* & p) { + if (!is_app(_n)) + return false; + app * n = to_app(_n); + quantifier * q = 0; + func_decl * d = n->get_decl(); + TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); + if (mm.m_decl2macro.find(d, q)) { + TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";); + app * head = 0; + expr * def = 0; + mm.get_head_def(q, d, head, def); + unsigned num = n->get_num_args(); + SASSERT(head && def); + ptr_buffer subst_args; + subst_args.resize(num, 0); + for (unsigned i = 0; i < num; i++) { + var * v = to_var(head->get_arg(i)); + SASSERT(v->get_idx() < num); + unsigned nidx = num - v->get_idx() - 1; + SASSERT(subst_args[nidx] == 0); + subst_args[nidx] = n->get_arg(i); + } + var_subst s(m); + expr_ref rr(m); + s(def, num, subst_args.c_ptr(), rr); + m_trail.push_back(rr); + r = rr; + if (m.proofs_enabled()) { + expr_ref instance(m); + s(q->get_expr(), num, subst_args.c_ptr(), instance); + proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr()); + proof * q_pr = 0; + mm.m_decl2macro_pr.find(d, q_pr); + SASSERT(q_pr != 0); + proof * prs[2] = { qi_pr, q_pr }; + p = m.mk_unit_resolution(2, prs); + } + else { + p = 0; + } + return true; + } + return false; + } +}; + +struct macro_manager::macro_expander_rw : public rewriter_tpl { + macro_expander_cfg m_cfg; + macro_expander_rw(ast_manager& m, macro_manager& mm): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, mm) + {} +}; + +macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm): simplifier(m), m_macro_manager(mm) { // REMARK: theory simplifier should not be used by macro_expander... @@ -295,20 +400,30 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) { if (has_macros()) { // Expand macros with "real" proof production support (NO rewrite*) - expr_ref old_n(m_manager); - proof_ref old_pr(m_manager); + expr_ref old_n(m); + proof_ref old_pr(m); old_n = n; old_pr = pr; + bool change = false; for (;;) { - macro_expander proc(m_manager, *this, m_simplifier); - proof_ref n_eq_r_pr(m_manager); - TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m_manager) << "\n";); + macro_expander_rw proc(m, *this); + proof_ref n_eq_r_pr(m); + TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";); proc(old_n, r, n_eq_r_pr); - new_pr = m_manager.mk_modus_ponens(old_pr, n_eq_r_pr); + new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr); if (r.get() == old_n.get()) - return; + break; old_n = r; old_pr = new_pr; + change = true; + } + // apply th_rewrite to the result. + if (change) { + th_rewriter rw(m); + proof_ref rw_pr(m); + expr_ref r1(r, m); + rw(r1, r, rw_pr); + new_pr = m.mk_modus_ponens(new_pr, rw_pr); } } else { diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h index a0a42b790..98e242cd8 100644 --- a/src/ast/macros/macro_manager.h +++ b/src/ast/macros/macro_manager.h @@ -19,8 +19,8 @@ Revision History: #ifndef MACRO_MANAGER_H_ #define MACRO_MANAGER_H_ -#include "ast/ast_util.h" #include "util/obj_hashtable.h" +#include "ast/ast_util.h" #include "ast/simplifier/simplifier.h" #include "ast/recurse_expr.h" #include "ast/func_decl_dependencies.h" @@ -36,8 +36,7 @@ Revision History: It has support for backtracking and tagging declarations in an expression as forbidded for being macros. */ class macro_manager { - ast_manager & m_manager; - simplifier & m_simplifier; + ast_manager & m; macro_util m_util; obj_map m_decl2macro; // func-decl -> quantifier @@ -58,21 +57,24 @@ class macro_manager { void restore_decls(unsigned old_sz); void restore_forbidden(unsigned old_sz); + struct macro_expander_cfg; + struct macro_expander_rw; + class macro_expander : public simplifier { protected: macro_manager & m_macro_manager; virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p); virtual void reduce1_quantifier(quantifier * q); public: - macro_expander(ast_manager & m, macro_manager & mm, simplifier & s); + macro_expander(ast_manager & m, macro_manager & mm); ~macro_expander(); }; friend class macro_expander; public: - macro_manager(ast_manager & m, simplifier & s); + macro_manager(ast_manager & m); ~macro_manager(); - ast_manager & get_manager() const { return m_manager; } + ast_manager & get_manager() const { return m; } macro_util & get_util() { return m_util; } bool insert(func_decl * f, quantifier * m, proof * pr); bool has_macros() const { return !m_macros.empty(); } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index a8d115d64..6b747756c 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -118,6 +118,9 @@ expr * poly_rewriter::mk_mul_app(numeral const & c, expr * arg) { if (c.is_one()) { return arg; } + else if (is_zero(arg)) { + return arg; + } else { expr * new_args[2] = { mk_numeral(c), arg }; return mk_mul_app(2, new_args); @@ -654,6 +657,7 @@ br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, ptr_buffer new_args; new_args.push_back(args[0]); for (unsigned i = 1; i < num_args; i++) { + if (is_zero(args[i])) continue; expr * aux_args[2] = { minus_one, args[i] }; new_args.push_back(mk_mul_app(2, aux_args)); } diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h index fccb0c40f..51f6978ec 100644 --- a/src/muz/pdr/pdr_util.h +++ b/src/muz/pdr/pdr_util.h @@ -22,9 +22,9 @@ Revision History: #include "ast/ast.h" #include "ast/ast_pp.h" +#include "ast/ast_util.h" #include "util/obj_hashtable.h" #include "util/ref_vector.h" -#include "ast/simplifier/simplifier.h" #include "util/trace.h" #include "util/vector.h" #include "ast/arith_decl_plugin.h" diff --git a/src/muz/rel/dl_bound_relation.cpp b/src/muz/rel/dl_bound_relation.cpp index de6c76456..9dc0eb8d5 100644 --- a/src/muz/rel/dl_bound_relation.cpp +++ b/src/muz/rel/dl_bound_relation.cpp @@ -653,7 +653,7 @@ namespace datalog { void bound_relation::to_formula(expr_ref& fml) const { ast_manager& m = get_plugin().get_ast_manager(); arith_util& arith = get_plugin().m_arith; - basic_simplifier_plugin& bsimp = get_plugin().m_bsimp; + bool_rewriter& bsimp = get_plugin().m_bsimp; expr_ref_vector conjs(m); relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { diff --git a/src/muz/rel/dl_bound_relation.h b/src/muz/rel/dl_bound_relation.h index 456df737b..1678e23b8 100644 --- a/src/muz/rel/dl_bound_relation.h +++ b/src/muz/rel/dl_bound_relation.h @@ -27,6 +27,7 @@ Revision History: #include "muz/rel/dl_interval_relation.h" #include "ast/arith_decl_plugin.h" #include "ast/simplifier/basic_simplifier_plugin.h" +#include "ast/rewriter/bool_rewriter.h" namespace datalog { @@ -44,7 +45,7 @@ namespace datalog { class filter_interpreted_fn; class filter_intersection_fn; arith_util m_arith; - basic_simplifier_plugin m_bsimp; + bool_rewriter m_bsimp; public: bound_relation_plugin(relation_manager& m); virtual bool can_handle_signature(const relation_signature & s); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 2f55cd704..7eb189ebf 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -52,7 +52,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_asserted_formulas(m), m_asserted_formula_prs(m), m_asserted_qhead(0), - m_macro_manager(m, m_simplifier), + m_macro_manager(m), m_bit2int(m), m_bv_sharing(m), m_inconsistent(false){ diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 9b1835ff3..b3f258ba7 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -64,7 +64,7 @@ class macro_finder_tactic : public tactic { bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); simp.register_plugin(bvsimp); - macro_manager mm(m_manager, simp); + macro_manager mm(m_manager); macro_finder mf(m_manager, mm); expr_ref_vector forms(m_manager), new_forms(m_manager); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index f7312fd2e..8a91bde61 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -62,7 +62,7 @@ class quasi_macros_tactic : public tactic { bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); simp.register_plugin(bvsimp); - macro_manager mm(m_manager, simp); + macro_manager mm(m_manager); quasi_macros qm(m_manager, mm); bool more = true;