From 534a31f74e81ab880fbb28dbf829e036d7a3957c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Mar 2018 05:06:36 -0800
Subject: [PATCH] inherit solver parameters in asserted formulas rewriter.
 #1511

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/asserted_formulas.cpp          |  4 ++++
 src/smt/asserted_formulas.h            |  1 +
 src/smt/params/preprocessor_params.cpp |  1 +
 src/smt/smt_context.cpp                |  4 ++++
 src/smt/smt_context.h                  |  2 ++
 src/smt/smt_kernel.cpp                 | 10 +++-------
 src/test/heap.cpp                      |  5 ++++-
 7 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 5903fefcb..444069d8c 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/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;
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index 275687adb..c2f2b6a97 100644
--- a/src/smt/asserted_formulas.h
+++ b/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);
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index ee4b7c2e4..57b11e7fd 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/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();
 }
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 9c95ac7c3..513bf7665 100644
--- a/src/smt/smt_context.cpp
+++ b/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();
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index a4581b020..abfc8c499 100644
--- a/src/smt/smt_context.h
+++ b/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() {
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index a7948725c..846d0235d 100644
--- a/src/smt/smt_kernel.cpp
+++ b/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.
-            // The update is performed at smt_kernel "users".
-            // params2smt_params(p, fparams());
+            m_kernel.updt_params(p);
         }
     };
 
@@ -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();
diff --git a/src/test/heap.cpp b/src/test/heap.cpp
index 08891ccaa..2c77b939e 100644
--- a/src/test/heap.cpp
+++ b/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;