remove hoist functionality

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

src/ast/rewriter/CMakeLists.txt

@@ -23,7 +23,6 @@ z3_add_component(rewriter
     factor_rewriter.cpp
     fpa_rewriter.cpp
     func_decl_replace.cpp
-    hoist_rewriter.cpp
     inj_axiom.cpp
     label_rewriter.cpp
     macro_replacer.cpp

src/ast/rewriter/bool_rewriter.cpp

@@ -34,7 +34,6 @@ 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) {
@@ -270,28 +269,6 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 return BR_DONE;
         }
 
-#if 0
-        br_status st;
-        expr_ref r(m());
-        st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
-        if (st != BR_FAILED) {
-            m_counts1.reserve(m().get_num_asts() + 1);
-            m_counts2.reserve(m().get_num_asts() + 1);
-            get_num_internal_exprs(m_counts1, m_todo1, r);
-            for (unsigned i = 0; i < num_args; ++i)
-                get_num_internal_exprs(m_counts2, m_todo2, args[i]);
-            unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
-            unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
-            if (count1 > count2)
-                st = BR_FAILED;
-        }
-        if (st != BR_FAILED)
-            result = r;
-        if (st == BR_DONE)
-            return BR_REWRITE1;
-        if (st != BR_FAILED)
-            return st;
-#endif
         if (s) {
             if (m_sort_disjunctions) {
                 ast_lt lt;

src/ast/rewriter/bool_rewriter.h

@@ -20,7 +20,6 @@ Module Name:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/hoist_rewriter.h"
 #include "util/params.h"
 
 /**
@@ -51,7 +50,6 @@ Module Name:
 */
 class bool_rewriter {
     ast_manager &  m_manager;
-    hoist_rewriter m_hoist;
     bool           m_flat_and_or = false;
     bool           m_sort_disjunctions = true;
     bool           m_local_ctx = false;
@@ -84,7 +82,7 @@ class bool_rewriter {
     void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
 
 public:
-    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { 
+    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { 
         updt_params(p); 
     }
     ast_manager & m() const { return m_manager; }