add sat-smt-preprocess module

self-contained pre-processing initialization

src/ast/simplifiers/rewriter_simplifier.h

@@ -25,10 +25,12 @@ class rewriter_simplifier : public dependent_expr_simplifier {
 
     unsigned               m_num_steps = 0;
     params_ref             m_params;
+    th_rewriter            m_rewriter;
 
 public:
     rewriter_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
-        dependent_expr_simplifier(m, fmls) {
+        dependent_expr_simplifier(m, fmls),
+        m_rewriter(m) {
         updt_params(p);
     }
         
@@ -39,15 +41,15 @@ public:
         for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) {
             if (m_fmls.inconsistent())
                 break;
-            auto [f, d] = m_fmls[i]();
+            auto d = m_fmls[idx];
-            m_rewriter(f, new_curr, new_pr);
+            m_rewriter(d.fml(), new_curr, new_pr);
             m_num_steps += m_rewriter.get_num_steps();
-            m_fmls.update(idx, dependent_expr(m, new_curr, d));            
+            m_fmls.update(idx, dependent_expr(m, new_curr, d.dep()));            
         }
-        advance_qhead(m_fmls.size());
+        advance_qhead();
     }
     void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); }
-    void reset_statistics() override { m_stats.reset(); }
+    void reset_statistics() override { m_num_steps = 0; }
     void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); }
     void collect_param_descrs(param_descrs& r) override { th_rewriter::get_param_descrs(r); }
 };

src/ast/simplifiers/seq_simplifier.h

@@ -48,7 +48,7 @@ public:
     
     void reset_statistics() override {
         for (auto* s : m_simplifiers)
-            s->reset_statistics(st);
+            s->reset_statistics();
     }
     
     void updt_params(params_ref const& p) override {

src/sat/sat_solver/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(sat_solver
   SOURCES
     inc_sat_solver.cpp
+    sat_smt_preprocess.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
     arith_tactics

src/sat/sat_solver/sat_smt_preprocess.cpp

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    sat_smt_preprocess.cpp
+
+Abstract:
+
+    SAT pre-process
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-28
+
+--*/
+
+#include "sat/sat_params.hpp"
+#include "sat/sat_solver/sat_smt_preprocess.h"
+#include "ast/simplifiers/bit_blaster.h"
+#include "ast/simplifiers/max_bv_sharing.h"
+#include "ast/simplifiers/card2bv.h"
+#include "ast/simplifiers/propagate_values.h"
+#include "ast/simplifiers/rewriter_simplifier.h"
+#include "ast/simplifiers/solve_eqs.h"
+#include "ast/simplifiers/eliminate_predicates.h"
+
+void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
+    params_ref simp1_p = p;
+    simp1_p.set_bool("som", true);
+    simp1_p.set_bool("pull_cheap_ite", true);
+    simp1_p.set_bool("push_ite_bv", false);
+    simp1_p.set_bool("local_ctx", true);
+    simp1_p.set_uint("local_ctx_limit", 10000000);
+    simp1_p.set_bool("flat", true); // required by som
+    simp1_p.set_bool("hoist_mul", false); // required by som
+    simp1_p.set_bool("elim_and", true);
+    simp1_p.set_bool("blast_distinct", true);
+    simp1_p.set_bool("flat_and_or", false);
+    
+    params_ref simp2_p = p;
+    simp2_p.set_bool("flat", false);
+    simp2_p.set_bool("flat_and_or", false);
+    
+    sat_params sp(p);
+    if (sp.euf()) {
+        s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
+        s.add_simplifier(alloc(propagate_values, m, p, st));
+        //
+        // add: 
+        // solve_eqs
+        // elim_predicates
+        // elim_uncnstr
+        // euf_completion?
+        //
+        // add: make it externally configurable
+        // 
+    }
+    else {
+        s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
+        s.add_simplifier(alloc(propagate_values, m, p, st));
+        s.add_simplifier(alloc(card2bv, m, p, st));
+        s.add_simplifier(alloc(rewriter_simplifier, m, simp1_p, st));
+        s.add_simplifier(mk_max_bv_sharing(m, p, st));
+        s.add_simplifier(alloc(bit_blaster, m, p, st));
+        s.add_simplifier(alloc(rewriter_simplifier, m, simp2_p, st));
+    }    
+}
+

src/sat/sat_solver/sat_smt_preprocess.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    sat_smt_preprocess.h
+
+Abstract:
+
+    SAT pre-process initialization
+    It collects the functionality associated with 
+    initializing pre-processing for the sat-smt solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-28
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/seq_simplifier.h"
+
+void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st);
+