add parameter for scenario from #4743

src/ast/rewriter/array_rewriter.cpp

@@ -30,6 +30,7 @@ void array_rewriter::updt_params(params_ref const & _p) {
     m_expand_select_store = p.expand_select_store();
     m_expand_store_eq = p.expand_store_eq();
     m_expand_nested_stores = p.expand_nested_stores();
+    m_blast_select_store = p.blast_select_store();
     m_expand_select_ite = false;
 }
 
@@ -179,7 +180,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
             return BR_REWRITE1;
         }
         default:
-            if (m_expand_select_store && to_app(args[0])->get_arg(0)->get_ref_count() == 1) {
+            if (m_blast_select_store || (m_expand_select_store && to_app(args[0])->get_arg(0)->get_ref_count() == 1)) {
                 // select(store(a, I, v), J) --> ite(I=J, v, select(a, J))
                 ptr_buffer<expr> new_args;
                 new_args.push_back(to_app(args[0])->get_arg(0));

src/ast/rewriter/array_rewriter.h

@@ -28,11 +28,12 @@ Notes:
 */
 class array_rewriter {
     array_util    m_util;
-    bool          m_sort_store;
+    bool          m_sort_store { false };
-    bool          m_expand_select_store;
+    bool          m_blast_select_store { false };
-    bool          m_expand_store_eq;
+    bool          m_expand_select_store { false };
-    bool          m_expand_select_ite;
+    bool          m_expand_store_eq { false };
-    bool          m_expand_nested_stores;
+    bool          m_expand_select_ite { false };
+    bool          m_expand_nested_stores { false };
     template<bool CHECK_DISEQ>
     lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
     void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls);
@@ -48,7 +49,6 @@ public:
     array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m) {
         updt_params(p);
-
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }

src/ast/rewriter/th_rewriter.cpp

@@ -789,8 +789,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 };
 }
 
-template class rewriter_tpl<th_rewriter_cfg>;
-
 struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
     th_rewriter_cfg m_cfg;
     imp(ast_manager & m, params_ref const & p):

src/params/array_rewriter_params.pyg

@@ -1,7 +1,8 @@
 def_module_params(module_name='rewriter',
                   class_name='array_rewriter_params',
                   export=True,
-                  params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"),
+                  params=(("expand_select_store", BOOL, False, "conservatively replace a (select (store ...) ...) term by an if-then-else term"),
+                          ("blast_select_store", BOOL, False, "eagerly replace all (select (store ..) ..) term by an if-then-else term"),
                           ("expand_nested_stores", BOOL, False, "replace nested stores by a lambda expression"),
                           ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
                           ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))

src/util/scoped_timer.cpp

@@ -20,17 +20,19 @@ Revision History:
 --*/
 
 #include "util/scoped_timer.h"
-#include "util/mutex.h"
 #include "util/util.h"
-#include "util/vector.h"
 #include <chrono>
 #include <climits>
 #include <condition_variable>
 #include <mutex>
 #include <thread>
 #include <vector>
+#include <atomic>
 
-struct state {
+
+
+
+struct scoped_timer_state {
     std::thread * m_thread { nullptr };
     std::timed_mutex m_mutex;
     event_handler * eh;
@@ -39,11 +41,11 @@ struct state {
     std::condition_variable_any cv;
 };
 
-static std::vector<state*> available_workers;
+static std::vector<scoped_timer_state*> available_workers;
 static std::mutex workers;
-static atomic<unsigned> num_workers(0);
+static std::atomic<unsigned> num_workers(0);
 
-static void thread_func(state *s) {
+static void thread_func(scoped_timer_state *s) {
     workers.lock();
     while (true) {
         s->cv.wait(workers, [=]{ return s->work > 0; });
@@ -71,16 +73,17 @@ static void thread_func(state *s) {
     }
 }
 
+
 struct scoped_timer::imp {
 private:
-    state *s;
+    scoped_timer_state *s;
 
 public:
     imp(unsigned ms, event_handler * eh) {
         workers.lock();
         if (available_workers.empty()) {
             workers.unlock();
-            s = new state;
+            s = new scoped_timer_state;
             ++num_workers;
         } 
         else {