From 1827f98851e1866187abe743afd2d80bc786412f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 19 Jun 2019 16:42:00 +0100 Subject: [PATCH] more fixes for mutexes in shell --- src/api/ml/z3native_stubs.h | 3 --- src/muz/base/dl_context.h | 4 ---- src/muz/spacer/spacer_context.h | 4 ---- src/sat/sat_ddfw.cpp | 2 -- src/shell/datalog_frontend.cpp | 8 ++++---- src/shell/lp_frontend.cpp | 19 ++++++++----------- src/shell/opt_frontend.cpp | 23 +++++++---------------- src/shell/smtlib_frontend.cpp | 16 +++++----------- src/util/trace.h | 9 +-------- 9 files changed, 25 insertions(+), 63 deletions(-) diff --git a/src/api/ml/z3native_stubs.h b/src/api/ml/z3native_stubs.h index ec498dafe..ceeaac17a 100644 --- a/src/api/ml/z3native_stubs.h +++ b/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 diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index b20e2813e..20f40fb22 100644 --- a/src/muz/base/dl_context.h +++ b/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" diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 54eb1befa..cb9063c52 100644 --- a/src/muz/spacer/spacer_context.h +++ b/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 #include "util/scoped_ptr_vector.h" #include "muz/spacer/spacer_manager.h" diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index 3986de214..64a7d8ae7 100644 --- a/src/sat/sat_ddfw.cpp +++ b/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; diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 6596cc3b7..b8461622d 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -18,13 +18,10 @@ Revision History: --*/ #include +#include #include #include #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 lock(*display_stats_mux); g_piece_timer.stop(); unsigned t_other = static_cast(g_piece_timer.get_seconds()*1000); g_overall_time.stop(); diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 96284230d..48a6879fe 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -17,11 +17,13 @@ Author: #include "util/gparams.h" #include -static std::mutex display_stats_mux; +namespace { +static std::mutex *display_stats_mux = new std::mutex; static lp::lp_solver* g_solver = nullptr; static void display_statistics() { + std::lock_guard 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); - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - } + display_statistics(); raise(SIGINT); } static void on_timeout() { - std::lock_guard 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(); - register_on_timeout_proc(nullptr); - g_solver = nullptr; - } + display_statistics(); + register_on_timeout_proc(nullptr); + g_solver = nullptr; delete solver; } +} unsigned read_mps_file(char const * mps_file_name) { signal(SIGINT, on_ctrl_c); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index e9e294eb9..155ef724c 100644 --- a/src/shell/opt_frontend.cpp +++ b/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 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); - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - } + display_statistics(); raise(SIGINT); } } static void on_timeout() { - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - } + 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"; } - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - register_on_timeout_proc(nullptr); - g_opt = nullptr; - } + display_statistics(); + register_on_timeout_proc(nullptr); + g_opt = nullptr; return 0; } diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index f6bcf8b82..ab6316aeb 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/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 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 lock(display_stats_mux); display_statistics(); exit(0); } static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - } + display_statistics(); raise(SIGINT); } @@ -97,11 +94,8 @@ unsigned read_smtlib2_commands(char const * file_name) { } - { - std::lock_guard lock(display_stats_mux); - display_statistics(); - g_cmd_context = nullptr; - } + display_statistics(); + g_cmd_context = nullptr; return result ? 0 : 1; } diff --git a/src/util/trace.h b/src/util/trace.h index 77c66afd4..1805f5657 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -17,13 +17,8 @@ Revision History: --*/ -#ifndef TRACE_H_ -#define TRACE_H_ +#pragma once -#ifdef _CYGWIN -#undef max -#undef min -#endif #include #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_ */