support threading for TRACE mode

src/math/simplex/bit_matrix.cpp

@@ -15,6 +15,7 @@ Notes:
 
 #include "math/simplex/bit_matrix.h"
 #include "util/stopwatch.h"
+#include "util/trace.h"
 #include <cstring>
 
 

src/solver/assertions/asserted_formulas.cpp

@@ -213,13 +213,13 @@ void asserted_formulas::force_push() {
 }
 
 void asserted_formulas::pop_scope(unsigned num_scopes) {
-    if (m_lazy_scopes > 0) {
+    if (num_scopes <= m_lazy_scopes) {
-        unsigned n = std::min(num_scopes, m_lazy_scopes);
+        m_lazy_scopes -= num_scopes;
-        m_lazy_scopes -= n;
+        return;
-        num_scopes -= n;
-        if (num_scopes == 0)
-            return;
     }
+    num_scopes -= m_lazy_scopes;
+    m_lazy_scopes = 0;
+    
     TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
     m_bv_sharing.pop_scope(num_scopes);
     m_macro_manager.pop_scope(num_scopes);

src/util/small_object_allocator.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "util/machine.h"
 #include "util/debug.h"
+#include "util/trace.h"
 
 class small_object_allocator {
     static const unsigned CHUNK_SIZE     = (8192 - sizeof(void*)*2);

src/util/trace.cpp

@@ -19,6 +19,25 @@ Revision History:
 #include "util/trace.h"
 #include "util/str_hashtable.h"
 
+#ifndef SINGLE_THREAD
+#include <mutex>
+#include <thread>
+
+static std::mutex g_verbose_mux;
+void verbose_lock() { g_verbose_mux.lock(); }
+void verbose_unlock() { g_verbose_mux.unlock(); }
+
+static std::thread::id g_thread_id = std::this_thread::get_id();
+static bool g_is_threaded = false;
+
+bool is_threaded() {
+    if (g_is_threaded) return true;
+    g_is_threaded = std::this_thread::get_id() != g_thread_id;
+    return g_is_threaded;
+}
+
+#endif
+
 #ifdef _TRACE
 
 std::ofstream tout(".z3-trace"); 

src/util/trace.h

@@ -21,6 +21,33 @@ Revision History:
 
 #include<fstream>
 
+#ifdef SINGLE_THREAD
+# define is_threaded() false
+#else
+bool is_threaded();
+#endif
+
+#ifdef SINGLE_THREAD
+#define LOCK_CODE(CODE) CODE;
+#define THREAD_LOCK(CODE) CODE
+
+#else
+void verbose_lock();
+void verbose_unlock();
+
+#define LOCK_CODE(CODE)                                         \
+    {                                                           \
+        verbose_lock();                                         \
+        CODE;                                                   \
+        verbose_unlock();                                       \
+    }
+
+#define THREAD_LOCK(CODE) if (is_threaded()) { LOCK_CODE(CODE); } else { CODE; }
+
+#endif
+
+
+
 #ifdef _TRACE
 extern std::ofstream tout; 
 #define TRACE_CODE(CODE) { CODE } ((void) 0 )
@@ -48,10 +75,15 @@ static inline void open_trace() {}
 static inline void finalize_trace() {}
 #endif
 
-#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
+#define TRACEH(TAG)  tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"
+#define TRACEEND tout << "------------------------------------------------\n"
+#define TRACEBODY(TAG, CODE) TRACEH(TAG); CODE; TRACEEND; tout.flush()
+#define STRACEBODY(CODE) CODE; tout.flush()
 
-#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
+#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })
 
-#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { CODE tout.flush(); })
+#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(STRACEBODY(CODE)); })
 
-#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
+#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { THREAD_LOCK(STRACEBODY(CODE)); })
+
+#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })

src/util/util.cpp

@@ -19,14 +19,6 @@ Revision History:
 
 #include "util/util.h"
 
-#ifndef SINGLE_THREAD
-#include <mutex>
-#include <thread>
-
-static std::mutex g_verbose_mux;
-void verbose_lock() { g_verbose_mux.lock(); }
-void verbose_unlock() { g_verbose_mux.unlock(); }
-#endif
 
 static unsigned g_verbosity_level = 0;
 
@@ -44,16 +36,6 @@ void set_verbose_stream(std::ostream& str) {
     g_verbose_stream = &str;
 }
 
-#ifndef SINGLE_THREAD
-static std::thread::id g_thread_id = std::this_thread::get_id();
-static bool g_is_threaded = false;
-
-bool is_threaded() {
-    if (g_is_threaded) return true;
-    g_is_threaded = std::this_thread::get_id() != g_thread_id;
-    return g_is_threaded;
-}
-#endif
 
 std::ostream& verbose_stream() {
     return *g_verbose_stream;

src/util/util.h

@@ -169,37 +169,11 @@ void set_verbosity_level(unsigned lvl);
 unsigned get_verbosity_level();
 std::ostream& verbose_stream();
 void set_verbose_stream(std::ostream& str);
-#ifdef SINGLE_THREAD
-# define is_threaded() false
-#else
-bool is_threaded();
-#endif
 
   
-#define IF_VERBOSE(LVL, CODE) {                                 \
+#define IF_VERBOSE(LVL, CODE) { if (get_verbosity_level() >= LVL) { THREAD_LOCK(CODE); } } ((void) 0)              
-    if (get_verbosity_level() >= LVL) {                         \
-        if (is_threaded()) {                                    \
-            LOCK_CODE(CODE);                                    \
-        }                                                       \
-        else {                                                  \
-            CODE;                                               \
-        }                                                       \
-    } } ((void) 0)              
 
 
-#ifdef SINGLE_THREAD
-#define LOCK_CODE(CODE) CODE;
-#else
-void verbose_lock();
-void verbose_unlock();
-
-#define LOCK_CODE(CODE)                                         \
-    {                                                           \
-        verbose_lock();                                         \
-        CODE;                                                   \
-        verbose_unlock();                                       \
-    }
-#endif
 
 template<typename T>
 struct default_eq {