tune hoist-rewriter

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

src/ast/ast.cpp

@@ -1826,7 +1826,7 @@ ast * ast_manager::register_node_core(ast * n) {
         SASSERT(m_ast_table.contains(n));
     }
 
-    n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
+    n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();        
 
 //    track_id(*this, n, 77);
     

src/ast/rewriter/hoist_rewriter.cpp

@@ -20,12 +20,12 @@ Notes:
 
 #include "ast/rewriter/hoist_rewriter.h"
 #include "ast/ast_util.h"
-#include "ast/rewriter/expr_safe_replace.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 
 
 hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
-    m_manager(m), m_args1(m), m_args2(m) { 
+    m_manager(m), m_args1(m), m_args2(m), m_subst(m) { 
     updt_params(p); 
 }
 
@@ -108,44 +108,37 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
             while (u != v);
         }
         reset((*uf)[turn]);
-        for (auto const& p : m_eqs) {
+        for (auto const& p : m_eqs) 
             (*uf)[turn].merge(mk_var(p.first), mk_var(p.second));
-        }
+        if ((*preds)[turn].empty() && m_eqs.empty()) 
-        if ((*preds)[turn].empty() && m_eqs.empty()) {
             return BR_FAILED;
-        }
+    }
+    if (m_eqs.empty()) {
+        result = hoist_predicates((*preds)[turn], num_args, es);
+        return BR_DONE;
     }
     // p & eqs & (or fmls)
-    expr_ref_vector fmls(m()), ors(m());
+    expr_ref_vector fmls(m());
-    expr_safe_replace subst(m());
+    m_subst.reset();
     for (expr * p : (*preds)[turn]) {
         expr* q = nullptr;
         if (m().is_not(p, q)) {
-            subst.insert(q, m().mk_false());
+            m_subst.insert(q, m().mk_false());
         }
         else {
-            subst.insert(p, m().mk_true());
+            m_subst.insert(p, m().mk_true());
         }
         fmls.push_back(p);
     }
     for (auto const& p : m_eqs) {
-        subst.insert(p.first, p.second);
+        m_subst.insert(p.first, p.second);
         fmls.push_back(m().mk_eq(p.first, p.second));
-    }
+    }    
-
+    expr_ref ors(::mk_or(m(), num_args, es), m());
-    for (unsigned i = 0; i < num_args; ++i) {
+    m_subst(ors);
-        expr_ref tmp(m());
+    fmls.push_back(ors);
-        subst(es[i], tmp);
+    result = mk_and(fmls);
-        ors.push_back(tmp);
+    TRACE("hoist", tout << ors << " => " << result << "\n";);
-    }
-    fmls.push_back(m().mk_or(ors.size(), ors.c_ptr()));
-    result = m().mk_and(fmls.size(), fmls.c_ptr());
-    TRACE("hoist", 
-          for (unsigned i = 0; i < num_args; ++i) {
-              tout << mk_pp(es[i], m()) << "\n";
-          }
-          tout << "=>\n";
-          tout << result << "\n";);
     return BR_DONE;
 }
 
@@ -162,6 +155,27 @@ unsigned hoist_rewriter::mk_var(expr* e) {
     return v;
 }
 
+expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
+    expr_ref result(m());
+    expr_ref_vector args(m()), fmls(m());
+    for (unsigned i = 0; i < num_args; ++i) {
+        VERIFY(is_and(es[i], &m_args1));
+        fmls.reset();
+        for (expr* e : m_args1) {
+            if (!preds.contains(e))
+                fmls.push_back(e);
+        }
+        args.push_back(::mk_and(fmls));
+    }
+    fmls.reset();
+    fmls.push_back(::mk_or(args));
+    for (auto* p : preds) 
+        fmls.push_back(p);
+    result = ::mk_and(fmls);
+    return result;
+}
+
+
 br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     switch (f->get_decl_kind()) {
     case OP_OR:

src/ast/rewriter/hoist_rewriter.h

@@ -20,6 +20,7 @@ Notes:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/expr_safe_replace.h"
 #include "util/params.h"
 #include "util/union_find.h"
 #include "util/obj_hashtable.h"
@@ -32,6 +33,7 @@ class hoist_rewriter {
     ptr_vector<expr>                m_es;
     svector<std::pair<expr*,expr*>> m_eqs;
     u_map<expr*>                    m_roots;
+    expr_safe_replace               m_subst;
     obj_map<expr, unsigned> m_expr2var;
     ptr_vector<expr>        m_var2expr;
     expr_mark               m_mark;
@@ -46,6 +48,8 @@ class hoist_rewriter {
 
     void reset(basic_union_find& uf);
 
+    expr_ref hoist_predicates(obj_hashtable<expr> const& p, unsigned num_args, expr* const* args);
+
 public:
     hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
     ast_manager& m() const { return m_manager; }

src/tactic/core/solve_eqs_tactic.cpp

@@ -690,6 +690,7 @@ class solve_eqs_tactic : public tactic {
                 expr* f = g.form(idx);
                 proof_ref pr1(m()), pr2(m());
                 thrw(f, tmp, pr1);
+                tmp2 = tmp;
                 rw(tmp, tmp2, pr2);
                 TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp << "\n" << tmp2 
                       << "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);