From 9f3089b098363babae1192f8c821225d58338af0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 4 Jun 2019 04:10:55 -0700
Subject: [PATCH] try with std::vector and ptr_vectors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_log.cpp     | 60 +++++++++++++++++------------------------
 src/sat/sat_solver.cpp  |  3 ++-
 src/tactic/tactical.cpp | 13 +++++----
 3 files changed, 34 insertions(+), 42 deletions(-)

diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp
index d6dccc670..5f2d8f8af 100644
--- a/src/api/api_log.cpp
+++ b/src/api/api_log.cpp
@@ -24,7 +24,13 @@ Revision History:
 
 std::ostream * g_z3_log = nullptr;
 bool g_z3_log_enabled   = false;
+
+#ifdef Z3_LOG_SYNC
 static std::mutex g_log_mux;
+#define SCOPED_LOCK() std::lock_guard<std::mutex> lock(g_log_mux)
+#else
+#define SCOPED_LOCK() {}
+#endif
 
 extern "C" {
     void Z3_close_log_unsafe(void) {
@@ -38,26 +44,20 @@ extern "C" {
     bool Z3_API Z3_open_log(Z3_string filename) {
         bool res = true;
 
-#ifdef Z3_LOG_SYNC
-        std::lock_guard<std::mutex> lock(g_log_mux);
-        {
-#endif
-            if (g_z3_log != nullptr)
-                Z3_close_log_unsafe();
-            g_z3_log = alloc(std::ofstream, filename);
-            if (g_z3_log->bad() || g_z3_log->fail()) {
-                dealloc(g_z3_log);
-                g_z3_log = nullptr;
-                res = false;
-            }
-            else {
-                *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
-                g_z3_log->flush();
-                g_z3_log_enabled = true;
-            }
-#ifdef Z3_LOG_SYNC
+        SCOPED_LOCK();
+        if (g_z3_log != nullptr)
+            Z3_close_log_unsafe();
+        g_z3_log = alloc(std::ofstream, filename);
+        if (g_z3_log->bad() || g_z3_log->fail()) {
+            dealloc(g_z3_log);
+            g_z3_log = nullptr;
+            res = false;
+        }
+        else {
+            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
+            g_z3_log->flush();
+            g_z3_log_enabled = true;
         }
-#endif
 
         return res;
     }
@@ -65,27 +65,15 @@ extern "C" {
     void Z3_API Z3_append_log(Z3_string str) {
         if (g_z3_log == nullptr)
             return;
-#ifdef Z3_LOG_SYNC
-        std::lock_guard<std::mutex> lock(g_log_mux);
-        {
-#endif
-            if (g_z3_log != nullptr)
-                _Z3_append_log(static_cast<char const *>(str));
-#ifdef Z3_LOG_SYNC
-        }
-#endif
+        SCOPED_LOCK();
+        if (g_z3_log != nullptr)
+            _Z3_append_log(static_cast<char const *>(str));
     }
 
     void Z3_API Z3_close_log(void) {
         if (g_z3_log != nullptr) {
-#ifdef Z3_LOG_SYNC
-            std::lock_guard<std::mutex> lock(g_log_mux);
-            {
-#endif
-                Z3_close_log_unsafe();
-#ifdef Z3_LOG_SYNC
-            }
-#endif
+            SCOPED_LOCK();
+            Z3_close_log_unsafe();
         }
     }
 }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 969a00e8a..604ec67c5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1302,7 +1302,8 @@ namespace sat {
 
         vector<std::thread> threads;
         for (int i = 0; i < num_threads; ++i) {
-            threads.push_back(std::thread([&]() { worker_thread(i); }));
+            int id = i;
+            threads.push_back(std::thread([&]() { worker_thread(id); }));
         }
         for (int i = 0; i < num_threads; ++i) {
             threads[i].join();
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 45e768198..82ecb819e 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -22,6 +22,7 @@ Notes:
 #include "util/scoped_ptr_vector.h"
 #include "tactic/tactical.h"
 #include <thread>
+#include <vector>
 
 class binary_tactical : public tactic {
 protected:
@@ -458,12 +459,13 @@ public:
             }
         };
 
-        vector<std::thread> threads;
+        scoped_ptr_vector<std::thread> threads;
         for (int i = 0; i < num_threads; ++i) {
-            threads.push_back(std::thread([&]() { worker_thread(i); }));
+            int id = i;
+            threads.push_back(alloc(std::thread, [&]() { worker_thread(id); }));
         }
         for (int i = 0; i < num_threads; ++i) {
-            threads[i].join();
+            threads[i]->join();
         }
         
         if (finished_id == UINT_MAX) {
@@ -659,10 +661,11 @@ public:
                 }
             };
 
-            vector<std::thread> threads;
+            std::vector<std::thread> threads;
             int num_threads = static_cast<int>(r1_size);
             for (int i = 0; i < num_threads; ++i) {
-                threads.push_back(std::thread([&]() { worker_thread(i); }));
+                int id = i;
+                threads.emplace_back([&]() { worker_thread(id); });
             }
             for (int i = 0; i < num_threads; ++i) {
                 threads[i].join();