inherit solver parameters in asserted formulas rewriter. #1511

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

src/smt/asserted_formulas.cpp

@@ -117,6 +117,10 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
     }
 }
 
+void asserted_formulas::updt_params(params_ref const& p) {
+    m_rewriter.updt_params(p);
+}
+
 void asserted_formulas::set_eliminate_and(bool flag) {
     if (flag == m_elim_and) return;
     m_elim_and = flag;

src/smt/asserted_formulas.h

@@ -223,6 +223,7 @@ public:
     asserted_formulas(ast_manager & m, smt_params & p);
     ~asserted_formulas();
 
+    void updt_params(params_ref const& p);
     bool has_quantifiers() const { return m_has_quantifiers; }
     void setup();
     void assert_expr(expr * e, proof * in_pr);

src/smt/params/preprocessor_params.cpp

@@ -25,6 +25,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     m_quasi_macros            = p.quasi_macros();
     m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
+//    m_pull_cheap_ite          = _p.get_bool("pull_cheap_ite", m_pull_cheap_ite);
     m_refine_inj_axiom        = p.refine_inj_axioms();
 }
 

src/smt/smt_context.cpp

@@ -132,6 +132,10 @@ namespace smt {
         return !m_manager.limit().inc();
     }
 
+    void context::updt_params(params_ref const& p) {
+        m_params.append(p);
+        m_asserted_formulas.updt_params(p);
+    }
 
     void context::copy(context& src_ctx, context& dst_ctx) {
         ast_manager& dst_m = dst_ctx.get_manager();

src/smt/smt_context.h

@@ -262,6 +262,8 @@ namespace smt {
             return m_params;
         }
 
+        void updt_params(params_ref const& p);
+
         bool get_cancel_flag();
 
         region & get_region() {

src/smt/smt_kernel.cpp

@@ -123,7 +123,6 @@ namespace smt {
             return m_kernel.preferred_sat(asms, cores);
         }
 
-
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
             return m_kernel.find_mutexes(vars, mutexes);
         }
@@ -196,9 +195,7 @@ namespace smt {
         }
 
         void updt_params(params_ref const & p) {
-            // We don't need params2smt_params anymore. smt_params has support for reading params_ref.
+            m_kernel.updt_params(p);
-            // The update is performed at smt_kernel "users".
-            // params2smt_params(p, fparams());
         }
     };
 
@@ -218,7 +215,6 @@ namespace smt {
         imp::copy(*src.m_imp, *dst.m_imp);
     }
 
-
     bool kernel::set_logic(symbol logic) {
         return m_imp->set_logic(logic);
     }
@@ -263,9 +259,9 @@ namespace smt {
     }
 
     void kernel::reset() {
-        ast_manager & _m       = m();
+        ast_manager & _m = m();
         smt_params & fps = m_imp->fparams();
-        params_ref ps          = m_imp->params();
+        params_ref ps    = m_imp->params();
         #pragma omp critical (smt_kernel)
         {
             m_imp->~imp();

src/test/heap.cpp

@@ -21,16 +21,19 @@ Revision History:
 #include "util/heap.h"
 #include "util/trace.h"
 #include "util/uint_set.h"
+// include "util/hashtable.h"
 
 struct lt_proc { bool operator()(int v1, int v2) const { return v1 < v2; } };
+//struct int_hash_proc { unsigned operator()(int v) const { std::cout << "hash " << v << "\n"; VERIFY(v >= 0); return v; }};  
+//typedef int_hashtable<int_hash_proc, default_eq<int> > int_set; 
 typedef heap<lt_proc> int_heap;
-struct int_hash_proc { unsigned operator()(int v) const { return v * 17; }};
 #define N 10000
 
 static random_gen heap_rand(1);
 
 static void tst1() {
     int_heap h(N);
+//    int_set t;
     uint_set  t;
     for (int i = 0; i < N * 3; i++) {
         int val = heap_rand() % N;