trying to get rid of last simplifier dependency in macros

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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;

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),
+macro_manager::macro_manager(ast_manager & m):
-    m_simplifier(s),
+    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) {
+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(m, m_manager) << "\n";);
+    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);
+    m_macros.push_back(q);
-    if (m_manager.proofs_enabled()) {
+    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<expr> 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_manager::macro_expander_cfg> {
+    macro_expander_cfg m_cfg;
+    macro_expander_rw(ast_manager& m, macro_manager& mm):
+        rewriter_tpl<macro_manager::macro_expander_cfg>(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);
+        expr_ref old_n(m);
-        proof_ref old_pr(m_manager);
+        proof_ref old_pr(m);
         old_n  = n;
         old_pr = pr;
+        bool change = false;
         for (;;) {
-            macro_expander proc(m_manager, *this, m_simplifier);
+            macro_expander_rw proc(m, *this);
-            proof_ref n_eq_r_pr(m_manager);
+            proof_ref n_eq_r_pr(m);
-            TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m_manager) << "\n";);
+            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 {

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;
+    ast_manager &                    m;
-    simplifier  &                    m_simplifier;
     macro_util                       m_util;
 
     obj_map<func_decl, quantifier *> 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(); }

src/ast/rewriter/poly_rewriter_def.h

@@ -118,6 +118,9 @@ expr * poly_rewriter<Config>::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<Config>::mk_sub(unsigned num_args, expr * const * args,
     ptr_buffer<expr> 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));
     }

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"

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) {

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);

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){

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);

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;