port bit-blaster to simplifiers

inc_sat_solver uses bit-blaster, card2bv and max_bv_sharing.
By turning these into simplifiers it will be possible to remove
dependencies on tactics and goals in inc_sat_simplifier and instead use a modular and general incremental pre-processing infrastructure.

src/ast/simplifiers/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(simplifiers
   SOURCES
+    bit_blaster.cpp
     bv_slice.cpp
     card2bv.cpp
     elim_unconstrained.cpp

src/ast/simplifiers/bit_blaster.cpp

@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bit_blaster.cpp
+
+Abstract:
+
+    Apply bit-blasting
+
+Author:
+
+    Leonardo (leonardo) 2011-10-25
+
+--*/
+
+#include "ast/simplifiers/bit_blaster.h"
+
+
+void bit_blaster::updt_params(params_ref const & p) {
+    m_params.append(p);
+    m_rewriter.updt_params(m_params);
+}
+
+void bit_blaster::collect_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    insert_max_steps(r);
+    r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders).");
+    r.insert("blast_add", CPK_BOOL, "(default: true) bit-blast adders.");
+    r.insert("blast_quant", CPK_BOOL, "(default: false) bit-blast quantified variables.");
+    r.insert("blast_full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.");
+}
+
+void bit_blaster::reduce() {                            
+    m_rewriter.start_rewrite();
+    expr_ref   new_curr(m);
+    proof_ref  new_pr(m);
+    bool change = false;
+    for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) {
+        if (m_fmls.inconsistent())
+            break;
+        auto [curr, d] = m_fmls[idx]();
+        m_rewriter(curr, new_curr, new_pr);
+        m_num_steps += m_rewriter.get_num_steps();
+        if (curr != new_curr) {
+            change = true;                    
+            TRACE("bit_blaster", tout << mk_pp(curr, m) << " -> " << new_curr << "\n";);
+            m_fmls.update(idx, dependent_expr(m, new_curr, d));
+        }
+    }
+
+    if (change) {
+        obj_map<func_decl, expr*> const2bits;
+        ptr_vector<func_decl> newbits;            
+        m_rewriter.end_rewrite(const2bits, newbits);
+        for (auto* f : newbits)
+            m_fmls.model_trail().hide(f);
+        for (auto const& [f, v] : const2bits) 
+            m_fmls.model_trail().push(f, v, nullptr, {});
+    }
+    m_rewriter.cleanup();
+
+    advance_qhead(m_fmls.size());
+}
+
+
+void bit_blaster::collect_statistics(statistics& st) const {
+    st.update("bit-blaster-num-steps", m_num_steps);
+}
+
+void bit_blaster::push() {
+    m_rewriter.push();
+    dependent_expr_simplifier::push();
+}
+
+void bit_blaster::pop(unsigned n) {
+    dependent_expr_simplifier::pop(n);
+    m_rewriter.pop(n);
+}

src/ast/simplifiers/bit_blaster.h

@@ -0,0 +1,51 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bit_blaster.h
+
+Abstract:
+
+    Apply bit-blasting
+
+Author:
+
+    Leonardo (leonardo) 2011-10-25
+
+--*/
+#include "ast/rewriter/bit_blaster/bit_blaster_rewriter.h"
+#include "ast/ast_pp.h"
+#include "model/model_pp.h"
+#include "ast/rewriter/rewriter_types.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+
+
+class bit_blaster : public dependent_expr_simplifier {
+
+    bit_blaster_rewriter   m_rewriter;
+    unsigned               m_num_steps = 0;
+    params_ref             m_params;
+
+public:
+    bit_blaster(ast_manager & m, params_ref const & p, dependent_expr_state& s):
+        dependent_expr_simplifier(m, s),
+        m_rewriter(m, p) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p) override;
+    void collect_param_descrs(param_descrs & r) override;
+    void reduce() override;
+    void collect_statistics(statistics& st) const override;
+    void push() override;
+    void pop(unsigned n) override;
+
+    /*
+    * Expose the bit-blaster rewriter so that assumptions and implied bit-vectors can be reconstructed
+    * after bit-blasting.
+    */
+    bit_blaster_rewriter& rewriter() { return m_rewriter; }
+
+};
+