more fixes for mutexes in shell

src/api/ml/z3native_stubs.h

@@ -26,14 +26,11 @@ Notes:
   #else
     #define DLL_PUBLIC __declspec(dllexport)
   #endif
-  #define DLL_LOCAL
 #else
   #if __GNUC__ >= 4
     #define DLL_PUBLIC __attribute__ ((visibility ("default")))
-    #define DLL_LOCAL  __attribute__ ((visibility ("hidden")))
   #else
     #define DLL_PUBLIC
-    #define DLL_LOCAL
   #endif
 #endif
     

src/muz/base/dl_context.h

@@ -19,10 +19,6 @@ Revision History:
 #ifndef DL_CONTEXT_H_
 #define DL_CONTEXT_H_
 
-#ifdef _CYGWIN
-#undef min
-#undef max
-#endif
 #include "ast/arith_decl_plugin.h"
 #include "util/map.h"
 #include "ast/rewriter/th_rewriter.h"

src/muz/spacer/spacer_context.h

@@ -23,10 +23,6 @@ Notes:
 #ifndef _SPACER_CONTEXT_H_
 #define _SPACER_CONTEXT_H_
 
-#ifdef _CYGWIN
-#undef min
-#undef max
-#endif
 #include <queue>
 #include "util/scoped_ptr_vector.h"
 #include "muz/spacer/spacer_manager.h"

src/sat/sat_ddfw.cpp

@@ -463,7 +463,6 @@ namespace sat {
 
     unsigned ddfw::select_max_same_sign(unsigned cf_idx) {
         clause const& c = get_clause(cf_idx);
-        unsigned sz = c.size();
         unsigned max_weight = 2;
         unsigned max_trues = 0;
         unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause.
@@ -566,7 +565,6 @@ namespace sat {
             SASSERT(ci.m_weight > 0);
         }
         for (unsigned i = 0; i < m_clauses.size(); ++i) {
-            clause_info const& ci = m_clauses[i];
             bool found = false;
             for (literal lit : get_clause(i)) {
                 if (is_true(lit)) found = true;

src/shell/datalog_frontend.cpp

@@ -18,13 +18,10 @@ Revision History:
 --*/
 
 #include<iostream>
+#include<mutex>
 #include<time.h>
 #include<signal.h>
 #include "util/stopwatch.h"
-#ifdef _CYGWIN
-#undef min
-#undef max
-#endif
 #include "smt/params/smt_params.h"
 #include "ast/arith_decl_plugin.h"
 #include "muz/rel/dl_compiler.h"
@@ -46,6 +43,8 @@ static datalog::rule_set * g_orig_rules;
 static datalog::instruction_block * g_code;
 static datalog::execution_context * g_ectx;
 
+static std::mutex *display_stats_mux = new std::mutex;
+
 
 static void display_statistics(
     std::ostream& out,
@@ -56,6 +55,7 @@ static void display_statistics(
     bool verbose
     ) 
 {
+    std::lock_guard<std::mutex> lock(*display_stats_mux);
     g_piece_timer.stop();
     unsigned t_other = static_cast<int>(g_piece_timer.get_seconds()*1000);
     g_overall_time.stop();

src/shell/lp_frontend.cpp

@@ -17,11 +17,13 @@ Author:
 #include "util/gparams.h"
 #include <signal.h>
 
-static std::mutex display_stats_mux;
+namespace {
+static std::mutex *display_stats_mux = new std::mutex;
 
 static lp::lp_solver<double, double>* g_solver = nullptr;
 
 static void display_statistics() {
+    std::lock_guard<std::mutex> lock(*display_stats_mux);
     if (g_solver && g_solver->settings().print_statistics) {
         // TBD display relevant information about statistics
     }
@@ -29,15 +31,11 @@ static void display_statistics() {
 
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
-    {
+    display_statistics();
-        std::lock_guard<std::mutex> lock(display_stats_mux);
-        display_statistics();
-    }
     raise(SIGINT);
 }
 
 static void on_timeout() {
-    std::lock_guard<std::mutex> lock(display_stats_mux);
     display_statistics();
     exit(0);    
 }
@@ -92,13 +90,12 @@ void run_solver(lp_params & params, char const * mps_file_name) {
         solver->print_model(std::cout);
     }
 
-    {
+    display_statistics();
-        display_statistics();
+    register_on_timeout_proc(nullptr);
-        register_on_timeout_proc(nullptr);
+    g_solver = nullptr;
-        g_solver = nullptr;
-    }
     delete solver;
 }
+}
 
 unsigned read_mps_file(char const * mps_file_name) {
     signal(SIGINT, on_ctrl_c);

src/shell/opt_frontend.cpp

@@ -25,8 +25,7 @@ static bool g_first_interrupt = true;
 static opt::context* g_opt = nullptr;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
-static std::mutex display_stats_mux;
+static std::mutex *display_stats_mux = new std::mutex;
-
 
 
 static void display_results() {
@@ -51,6 +50,7 @@ static void display_results() {
 }
 
 static void display_statistics() {
+    std::lock_guard<std::mutex> lock(*display_stats_mux);
     if (g_display_statistics && g_opt) {
         ::statistics stats;
         g_opt->collect_statistics(stats);
@@ -69,19 +69,13 @@ static void STD_CALL on_ctrl_c(int) {
     }
     else {
         signal (SIGINT, SIG_DFL);
-        {
+        display_statistics();
-            std::lock_guard<std::mutex> lock(display_stats_mux);
-            display_statistics();
-        }
         raise(SIGINT);
     }
 }
 
 static void on_timeout() {
-    {
+    display_statistics();
-        std::lock_guard<std::mutex> lock(display_stats_mux);
-        display_statistics();
-    }
     exit(0);
 }
 
@@ -132,12 +126,9 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
     catch (z3_exception & ex) {
         std::cerr << ex.msg() << "\n";
     }
-    {
+    display_statistics();
-        std::lock_guard<std::mutex> lock(display_stats_mux);
+    register_on_timeout_proc(nullptr);
-        display_statistics();
+    g_opt = nullptr;
-        register_on_timeout_proc(nullptr);
-        g_opt = nullptr;
-    }    
     return 0;
 }
 

src/shell/smtlib_frontend.cpp

@@ -32,13 +32,14 @@ Revision History:
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 
-static std::mutex display_stats_mux;
+static std::mutex *display_stats_mux = new std::mutex;
 
 extern bool g_display_statistics;
 static clock_t             g_start_time;
 static cmd_context *       g_cmd_context = nullptr;
 
 static void display_statistics() {
+    std::lock_guard<std::mutex> lock(*display_stats_mux);
     clock_t end_time = clock();
     if (g_cmd_context && g_display_statistics) {
         std::cout.flush();
@@ -51,17 +52,13 @@ static void display_statistics() {
 }
 
 static void on_timeout() {
-    std::lock_guard<std::mutex> lock(display_stats_mux);
     display_statistics();
     exit(0);    
 }
 
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
-    {
+    display_statistics();
-        std::lock_guard<std::mutex> lock(display_stats_mux);
-        display_statistics();
-    }
     raise(SIGINT);
 }
 
@@ -97,11 +94,8 @@ unsigned read_smtlib2_commands(char const * file_name) {
     }
 
 
-    {
+    display_statistics();
-        std::lock_guard<std::mutex> lock(display_stats_mux);
+    g_cmd_context = nullptr;
-        display_statistics();
-        g_cmd_context = nullptr;
-    }
     return result ? 0 : 1;
 }
 

src/util/trace.h

@@ -17,13 +17,8 @@ Revision History:
 
 --*/
 
-#ifndef TRACE_H_
+#pragma once
-#define TRACE_H_
 
-#ifdef _CYGWIN
-#undef max
-#undef min
-#endif
 #include<fstream>
 
 #ifdef _TRACE
@@ -58,5 +53,3 @@ static inline void finalize_trace() {}
 #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
 
 #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
-
-#endif /* TRACE_H_ */