From c2fe76569fdb118101e8131f982cc5bfd7cc4438 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Feb 2023 17:48:02 -0800
Subject: [PATCH] remove dependency on bool-rewriter in hoist rewriter

deal with regression reported in
https://github.com/Z3Prover/z3/commit/cac5052685eedb9dca304b623616fc9b8659bf58#commitcomment-100606067
and unit tests doc.cpp
---
 src/ast/rewriter/bool_rewriter.cpp  |  1 +
 src/ast/rewriter/bool_rewriter.h    |  1 -
 src/ast/rewriter/hoist_rewriter.cpp | 25 ++++++++++++++++---------
 src/ast/rewriter/hoist_rewriter.h   |  4 ++--
 4 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 392b2e681c7..378c794cd13 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -32,6 +32,7 @@ void bool_rewriter::updt_params(params_ref const & _p) {
     m_blast_distinct       = p.blast_distinct();
     m_blast_distinct_threshold = p.blast_distinct_threshold();
     m_ite_extra_rules      = p.ite_extra_rules();
+    m_hoist.set_elim_and(m_elim_and);
 }
 
 void bool_rewriter::get_param_descrs(param_descrs & r) {
diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h
index 48894908452..e02bf86d38f 100644
--- a/src/ast/rewriter/bool_rewriter.h
+++ b/src/ast/rewriter/bool_rewriter.h
@@ -83,7 +83,6 @@ class bool_rewriter {
 public:
     bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { 
         updt_params(p); 
-        m_hoist.set(*this);
     }
     ast_manager & m() const { return m_manager; }
     family_id get_fid() const { return m().get_basic_family_id(); }
diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp
index 2329fd527d1..d3f5af2b573 100644
--- a/src/ast/rewriter/hoist_rewriter.cpp
+++ b/src/ast/rewriter/hoist_rewriter.cpp
@@ -28,17 +28,23 @@ hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
 }
 
 expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) {
-    if (m_rewriter)
-        return m_rewriter->mk_and(args);
+    if (m_elim_and) {
+        expr_ref_vector negs(m);
+        for (expr* a : args)
+            if (m.is_false(a))
+                return expr_ref(m.mk_false(), m);
+            else if (m.is_true(a))
+                continue;
+            else
+                negs.push_back(::mk_not(m, a));
+        return expr_ref(::mk_not(m, mk_or(negs)), m);
+    }
     else
         return ::mk_and(args);
 }
 
 expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) {
-    if (false && m_rewriter)
-        return m_rewriter->mk_or(args);
-    else
-        return ::mk_or(args);
+    return ::mk_or(args);
 }
 
 br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
@@ -159,11 +165,11 @@ unsigned hoist_rewriter::mk_var(expr* e) {
 
 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);
+    expr_ref_vector args(m), args1(m), fmls(m);
     for (unsigned i = 0; i < num_args; ++i) {
-        VERIFY(is_and(es[i], &m_args1));
+        VERIFY(is_and(es[i], &args1));
         fmls.reset();
-        for (expr* e : m_args1) 
+        for (expr* e : args1) 
             if (!preds.contains(e))
                 fmls.push_back(e);
         args.push_back(mk_and(fmls));
@@ -199,6 +205,7 @@ bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
             args->reset();
             for (expr* arg : *to_app(e)) 
                 args->push_back(::mk_not(m, arg));
+            TRACE("hoist", tout << args << " " <<  * args << "\n");
         }
         return true;
     }
diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h
index 72d44d0bce1..ae7dff3bc51 100644
--- a/src/ast/rewriter/hoist_rewriter.h
+++ b/src/ast/rewriter/hoist_rewriter.h
@@ -29,7 +29,6 @@ class bool_rewriter;
 
 class hoist_rewriter {
     ast_manager &                   m;
-    bool_rewriter*                  m_rewriter = nullptr;
     expr_ref_vector                 m_args1, m_args2;
     obj_hashtable<expr>             m_preds1, m_preds2;
     basic_union_find                m_uf1, m_uf2, m_uf0;
@@ -40,6 +39,7 @@ class hoist_rewriter {
     obj_map<expr, unsigned>         m_expr2var;
     ptr_vector<expr>                m_var2expr;
     expr_mark                       m_mark;
+    bool                            m_elim_and = false;
 
     bool is_and(expr* e, expr_ref_vector* args);
     expr_ref mk_and(expr_ref_vector const& args);
@@ -62,7 +62,7 @@ class hoist_rewriter {
     static void get_param_descrs(param_descrs & r) {}
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);    
     br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);    
-    void set(bool_rewriter& r) { m_rewriter = &r; }
+    void set_elim_and(bool b) { m_elim_and = b; }
 };
 
 struct hoist_rewriter_cfg : public default_rewriter_cfg {