diff --git a/CMakeLists.txt b/CMakeLists.txt index fb0fc6a87..5c82c1c00 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -272,41 +272,6 @@ else() message(STATUS "Not using libgmp") endif() -################################################################################ -# OpenMP support -################################################################################ -find_package(OpenMP) -if (OPENMP_FOUND) - set(USE_OPENMP_DEFAULT ON) -else() - set(USE_OPENMP_DEFAULT OFF) -endif() -# By setting `USE_OPENMP` this way configuration will fail during the first -# configure if the user explicitly passes `-DUSE_OPENMP=ON` and the compiler -# does not support OpenMP. However if the option is not set explicitly during -# the first configure OpenMP support will be automatically enabled/disabled -# depending on whether OpenMP is available. -option(USE_OPENMP "Use OpenMP" ${USE_OPENMP_DEFAULT}) - -if (USE_OPENMP) - if (NOT OPENMP_FOUND) - message(FATAL_ERROR "USE_OPENMP is ON but your compiler does not support OpenMP") - endif() - - list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) - # GCC and Clang need to have additional flags passed to the linker. - # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})`` - # because ``/openmp`` is interpreted as file name rather than a linker - # flag by MSVC and breaks the build - if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR - ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) - endif() - message(STATUS "Using OpenMP") -else() - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_") - message(STATUS "Not using OpenMP") -endif() ################################################################################ # API Log sync @@ -316,15 +281,26 @@ option(API_LOG_SYNC OFF ) if (API_LOG_SYNC) - if (NOT USE_OPENMP) - message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP") - endif() list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC") message(STATUS "Using API_LOG_SYNC") else() message(STATUS "Not using API_LOG_SYNC") endif() +################################################################################ +# Thread safe or not? +################################################################################ +option(SINGLE_THREADED + "Non-thread-safe build" + OFF +) +if (SINGLE_THREADED) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-DSINGLE_THREAD") + message(STATUS "Non-thread-safe build") +else() + message(STATUS "Thread-safe build") +endif() + ################################################################################ # FP math ################################################################################ diff --git a/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake index 3eb1e2d34..6e1378270 100644 --- a/cmake/z3_append_linker_flag_list_to_target.cmake +++ b/cmake/z3_append_linker_flag_list_to_target.cmake @@ -3,7 +3,7 @@ # them to append them as strings to the ``LINK_FLAGS`` property of # the specified target. # E.g. -# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static") +# z3_append_linker_flag_list_to_target(mytarget "-static") function(z3_append_linker_flag_list_to_target target) if (NOT (TARGET "${target}")) message(FATAL_ERROR "Specified target \"${target}\" is not a target") diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml deleted file mode 100644 index 05815b31f..000000000 --- a/scripts/azure-pipeline.vs.yaml +++ /dev/null @@ -1,17 +0,0 @@ -pool: - vmImage: "vs2017-win2016" - - -steps: -- task: DotNetCoreInstaller@0 - displayName: 'Use .NET Core sdk 2.1' - inputs: - version: 2.1.300 - - -- task: BatchScript@1 - displayName: 'run windist' - inputs: - filename: 'scripts/mk_win_dist.cmd' - - diff --git a/scripts/mk_util.py b/scripts/mk_util.py index eda7ac6fb..8aaec3360 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -110,8 +110,8 @@ GPROF=False GIT_HASH=False GIT_DESCRIBE=False SLOW_OPTIMIZE=False -USE_OMP=True LOG_SYNC=False +SINGLE_THREADED=False GUARD_CF=False ALWAYS_DYNAMIC_BASE=False @@ -136,7 +136,7 @@ def git_hash(): raise MKException("Failed to retrieve git hash") ls = r.split(' ') if len(ls) != 2: - raise MKException("Unexpected git output") + raise MKException("Unexpected git output " + r) return ls[0] def is_windows(): @@ -272,24 +272,6 @@ def test_gmp(cc): return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0 -def test_openmp(cc): - if not USE_OMP: - return False - if is_verbose(): - print("Testing OpenMP...") - t = TempFile('tstomp.cpp') - t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') - t.commit() - if IS_WINDOWS: - r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 - try: - rmf('tstomp.obj') - rmf('tstomp.exe') - except: - pass - return r - else: - return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 def test_fpmath(cc): global FPMATH_FLAGS @@ -664,8 +646,8 @@ def display_help(exit_code): if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") - print(" --noomp disable OpenMP and all features that require it.") print(" --log-sync synchronize access to API log files to enable multi-thread API logging.") + print(" --single-threaded non-thread-safe build") print("") print("Some influential environment variables:") if not IS_WINDOWS: @@ -692,14 +674,14 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED, ESRP_SIGN - global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC + global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'esrp', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', - 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) + 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded']) except: print("ERROR: Invalid command line option") display_help(1) @@ -763,10 +745,10 @@ def parse_options(): ML_ENABLED = True elif opt == "--js": JS_ENABLED = True - elif opt in ('', '--noomp'): - USE_OMP = False elif opt in ('', '--log-sync'): LOG_SYNC = True + elif opt == '--single-threaded': + SINGLE_THREADED = True elif opt in ('--python'): PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True @@ -2426,7 +2408,7 @@ def mk_config(): if ONLY_MAKEFILES: return config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') - global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC + global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED if IS_WINDOWS: config.write( 'CC=cl\n' @@ -2446,13 +2428,10 @@ def mk_config(): 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' link_extra_opt = '' - HAS_OMP = test_openmp('cl') - if HAS_OMP: - extra_opt = ' /openmp' - else: - extra_opt = ' /D_NO_OMP_' - if HAS_OMP and LOG_SYNC: + if LOG_SYNC: extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt + if SINGLE_THREADED: + extra_opt = '%s /DSINGLE_THREAD' % extra_opt if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if GUARD_CF: @@ -2515,7 +2494,6 @@ def mk_config(): # End of Windows VS config.mk if is_verbose(): print('64-bit: %s' % is64()) - print('OpenMP: %s' % HAS_OMP) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -2551,15 +2529,10 @@ def mk_config(): CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS FPMATH = test_fpmath(CXX) CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) - HAS_OMP = test_openmp(CXX) - if HAS_OMP: - CXXFLAGS = '%s -fopenmp' % CXXFLAGS - LDFLAGS = '%s -fopenmp' % LDFLAGS - SLIBEXTRAFLAGS = '%s -fopenmp' % SLIBEXTRAFLAGS - else: - CXXFLAGS = '%s -D_NO_OMP_' % CXXFLAGS - if HAS_OMP and LOG_SYNC: + if LOG_SYNC: CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS + if SINGLE_THREADED: + CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS if DEBUG_MODE: CXXFLAGS = '%s -g -Wall' % CXXFLAGS EXAMP_DEBUG_FLAG = '-g' @@ -2661,7 +2634,6 @@ def mk_config(): print('MinGW32 cross: %s' % (is_cygwin_mingw())) print('Archive Tool: %s' % AR) print('Arithmetic: %s' % ARITH) - print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) print('FP math: %s' % FPMATH) @@ -3166,10 +3138,6 @@ def mk_vs_proj_cl_compile(f, name, components, debug): f.write(' MultiThreadedDebugDLL\n') else: f.write(' MultiThreadedDLL\n') - if USE_OMP: - f.write(' true\n') - else: - f.write(' false\n') f.write(' ProgramDatabase\n') f.write(' ') deps = find_all_deps(name, components) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index 22ee71e17..e3c24da2f 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,4 +1,9 @@ + call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" -python scripts\mk_win_dist.py +python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk + +call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" + +python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index c685f4bd8..e4a0c0542 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -89,6 +89,7 @@ def parse_options(): 'x86-only', 'x64-only' ]) + print(options) for opt, arg in options: if opt in ('-b', '--build'): if arg == 'src': diff --git a/scripts/nightly-macos.yaml b/scripts/nightly-macos.yaml new file mode 100644 index 000000000..37b7169df --- /dev/null +++ b/scripts/nightly-macos.yaml @@ -0,0 +1,35 @@ +pool: + vmImage: "macOS-10.14" + +steps: + +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk + +- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. + +- task: GitHubRelease@0 + inputs: + gitHubConnection: Z3GitHub + repositoryName: 'Z3Prover/z3' + action: 'edit' + target: '$(Build.SourceVersion)' + tagSource: 'manual' + tag: 'NightlyMacOs' + title: 'Nightly MacOs' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: false + isPreRelease: true + + + + diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml new file mode 100644 index 000000000..53fbc4b70 --- /dev/null +++ b/scripts/nightly-ubuntu.yaml @@ -0,0 +1,35 @@ +pool: + vmImage: "ubuntu-16.04" + +steps: + +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk + +- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. + +- task: GitHubRelease@0 + inputs: + gitHubConnection: Z3GitHub + repositoryName: 'Z3Prover/z3' + action: 'edit' + target: '$(Build.SourceVersion)' + tagSource: 'manual' + tag: 'NightlyUbuntu' + title: 'Nightly Ubuntu' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: false + isPreRelease: true + + + + diff --git a/scripts/nightly-windows.yaml b/scripts/nightly-windows.yaml new file mode 100644 index 000000000..fccf6a877 --- /dev/null +++ b/scripts/nightly-windows.yaml @@ -0,0 +1,35 @@ +pool: + vmImage: "vs2017-win2016" + +steps: + +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: scripts\mk_win_dist.cmd + +- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)\* /y + +- task: GitHubRelease@0 + inputs: + gitHubConnection: Z3GitHub + repositoryName: 'Z3Prover/z3' + action: 'edit' + target: '$(Build.SourceVersion)' + tagSource: 'manual' + tag: 'NightlyWindows' + title: 'Nightly Windows' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: true + isPreRelease: true + + + + diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 7fbbd965e..abc02fc68 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -119,28 +119,22 @@ namespace api { context::set_interruptable::set_interruptable(context & ctx, event_handler & i): m_ctx(ctx) { - #pragma omp critical (set_interruptable) - { - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; - } + lock_guard lock(ctx.m_mux); + SASSERT(m_ctx.m_interruptable == 0); + m_ctx.m_interruptable = &i; } context::set_interruptable::~set_interruptable() { - #pragma omp critical (set_interruptable) - { - m_ctx.m_interruptable = nullptr; - } + lock_guard lock(m_ctx.m_mux); + m_ctx.m_interruptable = nullptr; } void context::interrupt() { - #pragma omp critical (set_interruptable) - { - if (m_interruptable) - (*m_interruptable)(API_INTERRUPT_EH_CALLER); - m_limit.cancel(); - m().limit().cancel(); - } + lock_guard lock(m_mux); + if (m_interruptable) + (*m_interruptable)(API_INTERRUPT_EH_CALLER); + m_limit.cancel(); + m().limit().cancel(); } void context::set_error_code(Z3_error_code err, char const* opt_msg) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 917d3f0af..8d240f3de 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -42,6 +42,7 @@ Revision History: #include "ast/rewriter/seq_rewriter.h" #include "smt/smt_solver.h" #include "solver/solver.h" +#include "util/mutex.h" namespace smtlib { class parser; @@ -79,6 +80,7 @@ namespace api { scoped_ptr m_manager; scoped_ptr m_cmd; add_plugins m_plugins; + mutex m_mux; arith_util m_arith_util; bv_util m_bv_util; diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index d338407bf..5f2d8f8af 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -16,6 +16,7 @@ Revision History: --*/ #include +#include #include "api/z3.h" #include "api/api_log_macros.h" #include "util/util.h" @@ -24,6 +25,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 lock(g_log_mux) +#else +#define SCOPED_LOCK() {} +#endif + extern "C" { void Z3_close_log_unsafe(void) { if (g_z3_log != nullptr) { @@ -36,26 +44,20 @@ extern "C" { bool Z3_API Z3_open_log(Z3_string filename) { bool res = true; -#ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) - { -#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; } @@ -63,27 +65,15 @@ extern "C" { void Z3_API Z3_append_log(Z3_string str) { if (g_z3_log == nullptr) return; -#ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) - { -#endif - if (g_z3_log != nullptr) - _Z3_append_log(static_cast(str)); -#ifdef Z3_LOG_SYNC - } -#endif + SCOPED_LOCK(); + if (g_z3_log != nullptr) + _Z3_append_log(static_cast(str)); } void Z3_API Z3_close_log(void) { if (g_z3_log != nullptr) { -#ifdef Z3_LOG_SYNC - #pragma omp critical (z3_log) - { -#endif - Z3_close_log_unsafe(); -#ifdef Z3_LOG_SYNC - } -#endif + SCOPED_LOCK(); + Z3_close_log_unsafe(); } } } diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index c95c07f63..196750a46 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -436,11 +436,8 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr void der_rewriter::cleanup() { ast_manager & m = m_imp->m(); - #pragma omp critical (th_rewriter) - { - dealloc(m_imp); - m_imp = alloc(imp, m); - } + dealloc(m_imp); + m_imp = alloc(imp, m); } void der_rewriter::reset() { diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp index 1ea556bef..d722b9351 100644 --- a/src/cmd_context/echo_tactic.cpp +++ b/src/cmd_context/echo_tactic.cpp @@ -29,12 +29,9 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { - #pragma omp critical (echo_tactic) - { - m_ctx.regular_stream() << m_msg; - if (m_newline) - m_ctx.regular_stream() << std::endl; - } + m_ctx.regular_stream() << m_msg; + if (m_newline) + m_ctx.regular_stream() << std::endl; skip_tactic::operator()(in, result); } }; @@ -61,14 +58,11 @@ public: void operator()(goal_ref const & in, goal_ref_buffer & result) override { double val = (*m_p)(*(in.get())).get_value(); - #pragma omp critical (probe_value_tactic) - { - if (m_msg) - m_ctx.diagnostic_stream() << m_msg << " "; - m_ctx.diagnostic_stream() << val; - if (m_newline) - m_ctx.diagnostic_stream() << std::endl; - } + if (m_msg) + m_ctx.diagnostic_stream() << m_msg << " "; + m_ctx.diagnostic_stream() << val; + if (m_newline) + m_ctx.diagnostic_stream() << std::endl; skip_tactic::operator()(in, result); } }; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 77a5f973d..c66552ac5 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -129,8 +129,8 @@ namespace sat { void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); if (limit < m_units.size()) { // this might repeat some literals. out.append(m_units.size() - limit, m_units.c_ptr() + limit); @@ -150,8 +150,8 @@ namespace sat { if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";); - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_pool.begin_add_vector(s.m_par_id, 2); m_pool.add_vector_elem(l1.index()); m_pool.add_vector_elem(l2.index()); @@ -165,23 +165,19 @@ namespace sat { unsigned n = c.size(); unsigned owner = s.m_par_id; IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); - #pragma omp critical (par_solver) - { - m_pool.begin_add_vector(owner, n); - for (unsigned i = 0; i < n; ++i) { - m_pool.add_vector_elem(c[i].index()); - } - m_pool.end_add_vector(); + std::lock_guard lock(m_mux); + m_pool.begin_add_vector(owner, n); + for (unsigned i = 0; i < n; ++i) { + m_pool.add_vector_elem(c[i].index()); } + m_pool.end_add_vector(); } void parallel::get_clauses(solver& s) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) - { - _get_clauses(s); - } + std::lock_guard lock(m_mux); + _get_clauses(s); } void parallel::_get_clauses(solver& s) { @@ -241,17 +237,13 @@ namespace sat { } void parallel::set_phase(solver& s) { - #pragma omp critical (par_solver) - { - _set_phase(s); - } + std::lock_guard lock(m_mux); + _set_phase(s); } void parallel::get_phase(solver& s) { - #pragma omp critical (par_solver) - { - _get_phase(s); - } + std::lock_guard lock(m_mux); + _get_phase(s); } void parallel::_get_phase(solver& s) { @@ -269,8 +261,8 @@ namespace sat { bool parallel::get_phase(local_search& s) { bool copied = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_consumer_ready = true; if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) { copied = true; @@ -288,8 +280,8 @@ namespace sat { bool parallel::copy_solver(solver& s) { bool copied = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(m_mux); m_consumer_ready = true; if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) { s.copy(*m_solver_copy, true); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index afb148ed4..a55cc17da 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -23,6 +23,8 @@ Revision History: #include "util/hashtable.h" #include "util/map.h" #include "util/rlimit.h" +#include "util/scoped_ptr_vector.h" +#include namespace sat { @@ -60,6 +62,7 @@ namespace sat { index_set m_unit_set; literal_vector m_lits; vector_pool m_pool; + std::mutex m_mux; // for exchange with local search: svector m_phase; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9241c4eaa..8a5da7531 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -19,6 +19,7 @@ Revision History: #include +#include #include "sat/sat_solver.h" #include "sat/sat_integrity_checker.h" #include "sat/sat_lookahead.h" @@ -1243,8 +1244,9 @@ namespace sat { unsigned error_code = 0; lbool result = l_undef; bool canceled = false; - #pragma omp parallel for - for (int i = 0; i < num_threads; ++i) { + std::mutex mux; + + auto worker_thread = [&](int i) { try { lbool r = l_undef; if (IS_AUX_SOLVER(i)) { @@ -1260,8 +1262,8 @@ namespace sat { r = check(num_lits, lits); } bool first = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(mux); if (finished_id == -1) { finished_id = i; first = true; @@ -1296,6 +1298,14 @@ namespace sat { ex_msg = ex.msg(); ex_kind = DEFAULT_EX; } + }; + + vector threads(num_threads); + for (int i = 0; i < num_threads; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); + } + for (auto & th : threads) { + th.join(); } if (IS_AUX_SOLVER(finished_id)) { @@ -1731,18 +1741,6 @@ namespace sat { } if (m_par) m_par->set_phase(*this); - -#if 0 - static unsigned file_no = 0; - #pragma omp critical (print_sat) - { - ++file_no; - std::ostringstream ostrm; - ostrm << "s" << file_no << ".txt"; - std::ofstream ous(ostrm.str()); - display(ous); - } -#endif } bool solver::set_root(literal l, literal r) { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 718f59854..96284230d 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -17,6 +17,8 @@ Author: #include "util/gparams.h" #include +static std::mutex display_stats_mux; + static lp::lp_solver* g_solver = nullptr; static void display_statistics() { @@ -27,19 +29,17 @@ static void display_statistics() { static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); } static void on_timeout() { - #pragma omp critical (g_display_stats) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + exit(0); } struct front_end_resource_limit : public lp::lp_resource_limit { @@ -92,7 +92,6 @@ void run_solver(lp_params & params, char const * mps_file_name) { solver->print_model(std::cout); } -// #pragma omp critical (g_display_stats) { display_statistics(); register_on_timeout_proc(nullptr); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index afa7b79c5..e9e294eb9 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -25,6 +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; @@ -68,8 +69,8 @@ static void STD_CALL on_ctrl_c(int) { } else { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); @@ -77,11 +78,11 @@ static void STD_CALL on_ctrl_c(int) { } static void on_timeout() { - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); - exit(0); } + exit(0); } static unsigned parse_opt(std::istream& in, opt_format f) { @@ -131,8 +132,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) { catch (z3_exception & ex) { std::cerr << ex.msg() << "\n"; } - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); register_on_timeout_proc(nullptr); g_opt = nullptr; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 0f156bced..ca0cbfaab 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -32,6 +32,8 @@ Revision History: #include "tactic/portfolio/smt_strategic_solver.h" #include "smt/smt_solver.h" +static std::mutex display_stats_mux; + extern bool g_display_statistics; static clock_t g_start_time; static cmd_context * g_cmd_context = nullptr; @@ -49,17 +51,15 @@ static void display_statistics() { } static void on_timeout() { - #pragma omp critical (g_display_stats) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + exit(0); } static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); } raise(SIGINT); @@ -98,8 +98,8 @@ unsigned read_smtlib2_commands(char const * file_name) { } - #pragma omp critical (g_display_stats) { + std::lock_guard lock(display_stats_mux); display_statistics(); g_cmd_context = nullptr; } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26d8df0ab..b1e89f72e 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -435,12 +435,9 @@ void asserted_formulas::commit(unsigned new_qhead) { TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";); m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead); m_expr2depth.reset(); - bool new_sub = false; for (unsigned i = m_qhead; i < new_qhead; ++i) { justified_expr const& j = m_formulas[i]; - if (update_substitution(j.get_fml(), j.get_proof())) { - new_sub = true; - } + update_substitution(j.get_fml(), j.get_proof()); } m_qhead = new_qhead; } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 323efeb12..9c8e08d3d 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -295,11 +295,8 @@ namespace smt { ast_manager & _m = m(); smt_params & fps = m_imp->fparams(); params_ref ps = m_imp->params(); - #pragma omp critical (smt_kernel) - { - m_imp->~imp(); - m_imp = new (m_imp) imp(_m, fps, ps); - } + m_imp->~imp(); + m_imp = new (m_imp) imp(_m, fps, ps); } bool kernel::inconsistent() { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index dea1a6c0b..0796471b1 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -59,7 +59,7 @@ public: } ~smt_tactic() override { - SASSERT(m_ctx == 0); + SASSERT(m_ctx == nullptr); } smt_params & fparams() { @@ -132,7 +132,6 @@ public: new_ctx->set_progress_callback(o.m_callback); } o.m_ctx = new_ctx; - } ~scoped_init_ctx() { @@ -208,6 +207,7 @@ public: m_ctx->collect_statistics(m_stats); throw; } + SASSERT(m_ctx); m_ctx->collect_statistics(m_stats); proof * pr = m_ctx->get_proof(); TRACE("smt_tactic", tout << r << " " << pr << "\n";); diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 6d790b68d..ab53a0ca9 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -321,7 +321,6 @@ namespace smt { sz_info& i = *kv.m_value; if (is_leaf(&i) && (i.m_literal == null_literal || !is_true(i.m_literal))) { rational value; - expr* set = k->get_arg(0); expr* sz = k->get_arg(1); if (!m_arith_value.get_value(sz, value)) { return l_undef; diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 053a584c1..1dbb5c090 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -337,7 +337,7 @@ private: void init() { parallel_params pp(m_params); - m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max()); + m_num_threads = std::min((unsigned) std::thread::hardware_concurrency(), pp.threads_max()); m_progress = 0; m_has_undef = false; m_allsat = false; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 00ea59869..ea89c6642 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -20,8 +20,9 @@ Notes: #include "util/cancel_eh.h" #include "util/cooperate.h" #include "util/scoped_ptr_vector.h" -#include "util/z3_omp.h" #include "tactic/tactical.h" +#include +#include class binary_tactical : public tactic { protected: @@ -369,20 +370,20 @@ enum par_exception_kind { class par_tactical : public or_else_tactical { + std::string ex_msg; + unsigned error_code; public: - par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {} + par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) { + error_code = 0; + } ~par_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; -#ifdef _NO_OMP_ - use_seq = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; if (use_seq) { // execute tasks sequentially or_else_tactical::operator()(in, result); @@ -407,21 +408,19 @@ public: unsigned finished_id = UINT_MAX; par_exception_kind ex_kind = DEFAULT_EX; - std::string ex_msg; - unsigned error_code = 0; - - #pragma omp parallel for - for (int i = 0; i < static_cast(sz); i++) { - goal_ref_buffer _result; - + + std::mutex mux; + + auto worker_thread = [&](unsigned i) { + goal_ref_buffer _result; goal_ref in_copy = in_copies[i]; tactic & t = *(ts.get(i)); try { t(in_copy, _result); bool first = false; - #pragma omp critical (par_tactical) { + std::lock_guard lock(mux); if (finished_id == UINT_MAX) { finished_id = i; first = true; @@ -429,10 +428,11 @@ public: } if (first) { for (unsigned j = 0; j < sz; j++) { - if (static_cast(i) != j) { + if (i != j) { managers[j]->limit().cancel(); } } + ast_translation translator(*(managers[i]), m, false); for (goal* g : _result) { result.push_back(g->translate(translator)); @@ -459,7 +459,17 @@ public: ex_msg = z3_ex.msg(); } } + }; + + vector threads(sz); + + for (unsigned i = 0; i < sz; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); } + for (unsigned i = 0; i < sz; ++i) { + threads[i].join(); + } + if (finished_id == UINT_MAX) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); @@ -499,11 +509,7 @@ public: void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; -#ifdef _NO_OMP_ - use_seq = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; if (use_seq) { // execute tasks sequentially and_then_tactical::operator()(in, result); @@ -554,9 +560,9 @@ public: par_exception_kind ex_kind = DEFAULT_EX; unsigned error_code = 0; std::string ex_msg; + std::mutex mux; - #pragma omp parallel for - for (int i = 0; i < static_cast(r1_size); i++) { + auto worker_thread = [&](unsigned i) { ast_manager & new_m = *(managers[i]); goal_ref new_g = g_copies[i]; @@ -568,8 +574,8 @@ public: ts2[i]->operator()(new_g, r2); } catch (tactic_exception & ex) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -579,8 +585,8 @@ public: } } catch (z3_error & err) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -590,8 +596,8 @@ public: } } catch (z3_exception & z3_ex) { - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!failed && !found_solution) { curr_failed = true; failed = true; @@ -614,8 +620,8 @@ public: if (is_decided_sat(r2)) { // found solution... bool first = false; - #pragma omp critical (par_and_then_tactical) { + std::lock_guard lock(mux); if (!found_solution) { failed = false; found_solution = true; @@ -655,6 +661,14 @@ public: } } } + }; + + vector threads(r1_size); + for (unsigned i = 0; i < r1_size; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); + } + for (unsigned i = 0; i < r1_size; ++i) { + threads[i].join(); } if (failed) { diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp index df8f67968..fa9ac7986 100644 --- a/src/util/cooperate.cpp +++ b/src/util/cooperate.cpp @@ -17,48 +17,35 @@ Notes: --*/ -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD + #include "util/cooperate.h" #include "util/trace.h" #include "util/debug.h" -#include "util/z3_omp.h" +#include +#include +#include -struct cooperation_lock { - omp_nest_lock_t m_lock; - char const * m_task; - volatile int m_owner_thread; - cooperation_lock() { - omp_set_nested(1); - omp_init_nest_lock(&m_lock); - m_task = nullptr; - m_owner_thread = -1; - } - ~cooperation_lock() { - omp_destroy_nest_lock(&m_lock); - } -}; - -static cooperation_lock g_lock; +static std::mutex lock; +static std::atomic owner_thread; bool cooperation_ctx::g_cooperate = false; void cooperation_ctx::checkpoint(char const * task) { SASSERT(cooperation_ctx::enabled()); - int tid = omp_get_thread_num(); - if (g_lock.m_owner_thread == tid) { - g_lock.m_owner_thread = -1; - omp_unset_nest_lock(&(g_lock.m_lock)); + std::thread::id tid = std::this_thread::get_id(); + if (owner_thread == tid) { + owner_thread = std::thread::id(); + lock.unlock(); } + // this critical section is used to force the owner thread to give a chance to // another thread to get the lock - #pragma omp critical (z3_cooperate) - { - omp_set_nest_lock(&(g_lock.m_lock)); - TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); - CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); - g_lock.m_owner_thread = tid; - } + std::this_thread::yield(); + lock.lock(); + TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); + owner_thread = tid; } #endif diff --git a/src/util/cooperate.h b/src/util/cooperate.h index 6220c4c51..7e75a50c3 100644 --- a/src/util/cooperate.h +++ b/src/util/cooperate.h @@ -16,10 +16,9 @@ Author: Notes: --*/ -#ifndef COOPERATE_H_ -#define COOPERATE_H_ +#pragma once -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD class cooperation_ctx { static bool g_cooperate; @@ -35,5 +34,3 @@ inline void cooperate(char const * task) { #else inline void cooperate(char const *) {} #endif - -#endif diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index ea9b3603c..0983189da 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -19,6 +19,9 @@ Notes: #include "util/gparams.h" #include "util/dictionary.h" #include "util/trace.h" +#include "util/mutex.h" + +static mutex gparams_mux; extern void gparams_register_modules(); @@ -110,14 +113,12 @@ public: } void reset() { - #pragma omp critical (gparams) - { - m_params.reset(); - for (auto & kv : m_module_params) { - dealloc(kv.m_value); - } - m_module_params.reset(); + lock_guard lock(gparams_mux); + m_params.reset(); + for (auto & kv : m_module_params) { + dealloc(kv.m_value); } + m_module_params.reset(); } // ----------------------------------------------- @@ -327,8 +328,8 @@ public: void set(char const * name, char const * value) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -379,8 +380,8 @@ public: std::string r; bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -426,8 +427,8 @@ public: params_ref get_module(symbol const & module_name) { params_ref result; params_ref * ps = nullptr; - #pragma omp critical (gparams) { + lock_guard lock(gparams_mux); if (m_module_params.find(module_name, ps)) { result.copy(*ps); } @@ -446,8 +447,8 @@ public: // ----------------------------------------------- void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { - #pragma omp critical (gparams) { + lock_guard lock(gparams_mux); out << "Global parameters\n"; get_param_descrs().display(out, indent + 4, smt2_style, include_descr); out << "\n"; @@ -469,44 +470,40 @@ public: } void display_modules(std::ostream & out) { - #pragma omp critical (gparams) - { - for (auto & kv : get_module_param_descrs()) { - out << "[module] " << kv.m_key; - char const * descr = nullptr; - if (get_module_descrs().find(kv.m_key, descr)) { - out << ", description: " << descr; - } - out << "\n"; + lock_guard lock(gparams_mux); + for (auto & kv : get_module_param_descrs()) { + out << "[module] " << kv.m_key; + char const * descr = nullptr; + if (get_module_descrs().find(kv.m_key, descr)) { + out << ", description: " << descr; } + out << "\n"; } } void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) - { - try { - param_descrs * d = nullptr; - if (!get_module_param_descrs().find(module_name, d)) { - std::stringstream strm; - strm << "unknown module '" << module_name << "'"; - throw exception(strm.str()); - } - out << "[module] " << module_name; - char const * descr = nullptr; - if (get_module_descrs().find(module_name, descr)) { - out << ", description: " << descr; - } - out << "\n"; - d->display(out, 4, false); + lock_guard lock(gparams_mux); + try { + param_descrs * d = nullptr; + if (!get_module_param_descrs().find(module_name, d)) { + std::stringstream strm; + strm << "unknown module '" << module_name << "'"; + throw exception(strm.str()); } - catch (z3_exception & ex) { - // Exception cannot cross critical section boundaries. - error = true; - error_msg = ex.msg(); + out << "[module] " << module_name; + char const * descr = nullptr; + if (get_module_descrs().find(module_name, descr)) { + out << ", description: " << descr; } + out << "\n"; + d->display(out, 4, false); + } + catch (z3_exception & ex) { + // Exception cannot cross critical section boundaries. + error = true; + error_msg = ex.msg(); } if (error) throw exception(std::move(error_msg)); @@ -515,8 +512,8 @@ public: void display_parameter(std::ostream & out, char const * name) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) { + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 6ef94e880..ffb664b6e 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -7,10 +7,10 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include +#include "util/mutex.h" #include "util/trace.h" #include "util/memory_manager.h" #include "util/error_codes.h" -#include "util/z3_omp.h" #include "util/debug.h" // The following two function are automatically generated by the mk_make.py script. // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files. @@ -35,7 +35,8 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) { } -static volatile bool g_memory_out_of_memory = false; +static mutex g_memory_mux; +static atomic g_memory_out_of_memory(false); static bool g_memory_initialized = false; static long long g_memory_alloc_size = 0; static long long g_memory_max_size = 0; @@ -54,10 +55,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) { } static void throw_out_of_memory() { - #pragma omp critical (z3_memory_manager) - { - g_memory_out_of_memory = true; - } + g_memory_out_of_memory = true; if (g_exit_when_out_of_memory) { std::cerr << g_out_of_memory_msg << "\n"; @@ -90,8 +88,8 @@ mem_usage_report g_info; void memory::initialize(size_t max_size) { bool initialize = false; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); // only update the maximum size if max_size != UINT_MAX if (max_size != UINT_MAX) g_memory_max_size = max_size; @@ -115,12 +113,7 @@ void memory::initialize(size_t max_size) { } bool memory::is_out_of_memory() { - bool r = false; - #pragma omp critical (z3_memory_manager) - { - r = g_memory_out_of_memory; - } - return r; + return g_memory_out_of_memory; } void memory::set_high_watermark(size_t watermark) { @@ -131,12 +124,8 @@ void memory::set_high_watermark(size_t watermark) { bool memory::above_high_watermark() { if (g_memory_watermark == 0) return false; - bool r; - #pragma omp critical (z3_memory_manager) - { - r = g_memory_watermark < g_memory_alloc_size; - } - return r; + lock_guard lock(g_memory_mux); + return g_memory_watermark < g_memory_alloc_size; } // The following methods are only safe to invoke at @@ -163,8 +152,8 @@ void memory::finalize() { unsigned long long memory::get_allocation_size() { long long r; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); r = g_memory_alloc_size; } if (r < 0) @@ -174,8 +163,8 @@ unsigned long long memory::get_allocation_size() { unsigned long long memory::get_max_used_memory() { unsigned long long r; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); r = g_memory_max_used_size; } return r; @@ -258,8 +247,8 @@ static void synchronize_counters(bool allocating) { bool out_of_mem = false; bool counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); g_memory_alloc_size += g_memory_thread_alloc_size; g_memory_alloc_count += g_memory_thread_alloc_count; if (g_memory_alloc_size > g_memory_max_used_size) @@ -339,8 +328,8 @@ void memory::deallocate(void * p) { size_t * sz_p = reinterpret_cast(p) - 1; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); g_memory_alloc_size -= sz; } free(real_p); @@ -349,8 +338,8 @@ void memory::deallocate(void * p) { void * memory::allocate(size_t s) { s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); g_memory_alloc_size += s; g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) @@ -379,8 +368,8 @@ void* memory::reallocate(void *p, size_t s) { void * real_p = reinterpret_cast(sz_p); s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; - #pragma omp critical (z3_memory_manager) { + lock_guard lock(g_memory_mux); g_memory_alloc_size += s - sz; g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 8ca2e983f..a46757059 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -376,7 +376,7 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) { set_core(n, m, v); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) { set_core(n, m, v); } @@ -399,7 +399,7 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) { set_core(n, m, v); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) { set_core(n, m, v); } @@ -1081,7 +1081,7 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t) significand_core(n, m, t); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) { significand_core(n, m, t); } @@ -1115,7 +1115,7 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) { to_mpz_core(n, m, t); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) { to_mpz_core(n, m, t); } @@ -1162,7 +1162,7 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } diff --git a/src/util/mpff.h b/src/util/mpff.h index 6f1e9d23c..c7d14bac4 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -58,7 +58,7 @@ class mpz; class mpq; template class mpz_manager; template class mpq_manager; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; typedef mpq_manager synch_mpq_manager; #else @@ -218,7 +218,7 @@ public: \brief Return the significand as a mpz numeral. */ void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void significand(mpff const & n, synch_mpz_manager & m, mpz & r); #endif @@ -386,7 +386,7 @@ public: void set(mpff & n, mpff const & v); void set(mpff & n, unsynch_mpz_manager & m, mpz const & v); void set(mpff & n, unsynch_mpq_manager & m, mpq const & v); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void set(mpff & n, synch_mpq_manager & m, mpq const & v); void set(mpff & n, synch_mpz_manager & m, mpz const & v); #endif @@ -429,7 +429,7 @@ public: */ void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD /** \brief Convert n into a mpz numeral. @@ -447,7 +447,7 @@ public: */ void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD /** \brief Convert n into a mpq numeral. diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index 8ed16ec68..4769ab24a 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -272,7 +272,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) { set_core(n, m, v); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) { set_core(n, m, v); } @@ -311,7 +311,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) { set_core(n, m, v); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) { set_core(n, m, v); } @@ -718,7 +718,7 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) { to_mpz_core(n, m, t); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) { to_mpz_core(n, m, t); } @@ -744,7 +744,7 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } diff --git a/src/util/mpfx.h b/src/util/mpfx.h index 6de3f251b..ddaf6f89a 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -51,7 +51,7 @@ class mpz; class mpq; template class mpz_manager; template class mpq_manager; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; typedef mpq_manager synch_mpq_manager; #else @@ -318,7 +318,7 @@ public: void set(mpfx & n, mpfx const & v); void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v); void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void set(mpfx & n, synch_mpz_manager & m, mpz const & v); void set(mpfx & n, synch_mpq_manager & m, mpq const & v); #endif @@ -366,7 +366,7 @@ public: */ void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD /** \brief Convert n into a mpz numeral. @@ -380,7 +380,7 @@ public: */ void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t); -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD /** \brief Convert n into a mpq numeral. */ diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 25445bc89..7142fbad1 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -29,11 +29,9 @@ static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment const mpn_digit mpn_manager::zero = 0; mpn_manager::mpn_manager() { - omp_init_nest_lock(&m_lock); } mpn_manager::~mpn_manager() { - omp_destroy_nest_lock(&m_lock); } int mpn_manager::compare(mpn_digit const * a, size_t const lnga, diff --git a/src/util/mpn.h b/src/util/mpn.h index bae972b0c..f871adda1 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -20,18 +20,21 @@ Revision History: #define MPN_H_ #include +#include #include "util/util.h" #include "util/buffer.h" -#include "util/z3_omp.h" typedef unsigned int mpn_digit; class mpn_manager { -#ifndef _NO_OMP_ - omp_nest_lock_t m_lock; +#ifndef SINGLE_THREAD + std::recursive_mutex m_lock; +#define MPN_BEGIN_CRITICAL() m_lock.lock() +#define MPN_END_CRITICAL() m_lock.unlock() +#else +#define MPN_BEGIN_CRITICAL() {} +#define MPN_END_CRITICAL() {} #endif -#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock); -#define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock); public: mpn_manager(); diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index b126f4c5d..e3f7292e4 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -428,7 +428,7 @@ void mpq_manager::rat_sub(mpq const & a, mpq const & b, mpq & c) { } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpq_manager; #endif template class mpq_manager; diff --git a/src/util/mpq.h b/src/util/mpq.h index 20802f786..ac96b8b7c 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -816,7 +816,7 @@ public: bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } }; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpq_manager synch_mpq_manager; #else typedef mpq_manager synch_mpq_manager; diff --git a/src/util/mpq_inf.cpp b/src/util/mpq_inf.cpp index 69de425cf..f8d5ff4f0 100644 --- a/src/util/mpq_inf.cpp +++ b/src/util/mpq_inf.cpp @@ -39,7 +39,7 @@ std::string mpq_inf_manager::to_string(mpq_inf const & a) { } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpq_inf_manager; #endif template class mpq_inf_manager; diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h index c7bd261e6..69ad655df 100644 --- a/src/util/mpq_inf.h +++ b/src/util/mpq_inf.h @@ -279,7 +279,7 @@ public: mpq_manager& get_mpq_manager() { return m; } }; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpq_inf_manager synch_mpq_inf_manager; #else typedef mpq_inf_manager synch_mpq_inf_manager; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 1e74c2e9e..cda4b599a 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -139,8 +139,6 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) { template mpz_manager::mpz_manager(): m_allocator("mpz_manager") { - if (SYNCH) - omp_init_nest_lock(&m_lock); #ifndef _MP_GMP if (sizeof(digit_t) == sizeof(uint64_t)) { // 64-bit machine @@ -197,8 +195,6 @@ mpz_manager::~mpz_manager() { mpz_clear(m_int64_max); mpz_clear(m_int64_min); #endif - if (SYNCH) - omp_destroy_nest_lock(&m_lock); } #ifndef _MP_GMP @@ -2470,7 +2466,7 @@ bool mpz_manager::divides(mpz const & a, mpz const & b) { return r; } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpz_manager; #endif template class mpz_manager; diff --git a/src/util/mpz.h b/src/util/mpz.h index 0faf13d18..4c927b206 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -20,12 +20,12 @@ Revision History: #define MPZ_H_ #include +#include #include "util/util.h" #include "util/small_object_allocator.h" #include "util/trace.h" #include "util/scoped_numeral.h" #include "util/scoped_numeral_vector.h" -#include "util/z3_omp.h" #include "util/mpn.h" unsigned u_gcd(unsigned u, unsigned v); @@ -135,9 +135,14 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { mutable small_object_allocator m_allocator; - mutable omp_nest_lock_t m_lock; -#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); -#define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock); +#ifndef SINGLE_THREAD + mutable std::recursive_mutex m_lock; +#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock() +#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock() +#else +#define MPZ_BEGIN_CRITICAL() {} +#define MPZ_END_CRITICAL() {} +#endif mutable mpn_manager m_mpn_manager; #ifndef _MP_GMP @@ -702,7 +707,7 @@ public: bool decompose(mpz const & n, svector & digits); }; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; #else typedef mpz_manager synch_mpz_manager; diff --git a/src/util/mutex.h b/src/util/mutex.h new file mode 100644 index 000000000..36d06f9a2 --- /dev/null +++ b/src/util/mutex.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + mutex.h + +Abstract: + + Auxiliary macros for mutual exclusion + +--*/ +#pragma once + +#ifdef SINGLE_THREAD + +template using atomic = T; + +struct mutex { + void lock() {} + void unlock() {} +}; + +struct lock_guard { + lock_guard(mutex &) {} +}; + +#else +#include +#include + +template using atomic = std::atomic; +typedef std::mutex mutex; +typedef std::lock_guard lock_guard; +#endif diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 9d3936edf..c659403ca 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "util/prime_generator.h" +#include "util/mutex.h" #define PRIME_LIST_MAX_SIZE 1<<20 @@ -109,6 +110,8 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } +static mutex g_prime_iterator; + uint64_t prime_iterator::next() { unsigned idx = m_idx; m_idx++; @@ -117,7 +120,7 @@ uint64_t prime_iterator::next() { } else { uint64_t r; - #pragma omp critical (prime_iterator) + lock_guard lock(g_prime_iterator); { r = (*m_generator)(idx); } @@ -128,4 +131,3 @@ uint64_t prime_iterator::next() { void prime_iterator::finalize() { g_prime_generator.finalize(); } - diff --git a/src/util/rational.cpp b/src/util/rational.cpp index e8c2d52d1..5e5ebe9e0 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -17,11 +17,9 @@ Revision History: --*/ #include +#include "util/mutex.h" #include "util/util.h" #include "util/rational.h" -#ifdef _WINDOWS -#include -#endif synch_mpq_manager * rational::g_mpq_manager = nullptr; rational rational::m_zero; @@ -42,9 +40,11 @@ static void mk_power_up_to(vector & pws, unsigned n) { } } +static mutex g_powers_of_two; + rational rational::power_of_two(unsigned k) { rational result; - #pragma omp critical (powers_of_two) + lock_guard lock(g_powers_of_two); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index e3afd0d92..ac596a118 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -18,6 +18,10 @@ Revision History: --*/ #include "util/rlimit.h" #include "util/common_msgs.h" +#include "util/mutex.h" + + +static mutex g_rlimit_mux; reslimit::reslimit(): m_cancel(0), @@ -69,48 +73,34 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - #pragma omp critical (reslimit_cancel) - { - m_children.push_back(r); - } + lock_guard lock(g_rlimit_mux); + m_children.push_back(r); } void reslimit::pop_child() { - #pragma omp critical (reslimit_cancel) - { - m_children.pop_back(); - } + lock_guard lock(g_rlimit_mux); + m_children.pop_back(); } void reslimit::cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + lock_guard lock(g_rlimit_mux); + set_cancel(m_cancel+1); } - void reslimit::reset_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(0); - } + lock_guard lock(g_rlimit_mux); + set_cancel(0); } void reslimit::inc_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + lock_guard lock(g_rlimit_mux); + set_cancel(m_cancel+1); } - void reslimit::dec_cancel() { - #pragma omp critical (reslimit_cancel) - { - if (m_cancel > 0) { - set_cancel(m_cancel-1); - } + lock_guard lock(g_rlimit_mux); + if (m_cancel > 0) { + set_cancel(m_cancel-1); } } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 77fab7b6b..18124717a 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -16,11 +16,11 @@ Author: Revision History: --*/ -#ifndef RLIMIT_H_ -#define RLIMIT_H_ +#pragma once #include "util/vector.h" + class reslimit { volatile unsigned m_cancel; bool m_suspend; @@ -88,6 +88,3 @@ struct scoped_limits { ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); } void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; } }; - - -#endif diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 3f0e7c967..36ea344fa 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -17,12 +17,14 @@ Revision History: --*/ #include "util/symbol.h" +#include "util/mutex.h" #include "util/str_hashtable.h" #include "util/region.h" #include "util/string_buffer.h" -#include "util/z3_omp.h" #include +static mutex g_symbol_lock; + symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -36,8 +38,7 @@ public: char const * get_str(char const * d) { const char * result; - #pragma omp critical (cr_symbol) - { + lock_guard lock(g_symbol_lock); str_hashtable::entry * e; if (m_table.insert_if_not_there_core(d, e)) { // new entry @@ -55,7 +56,6 @@ public: result = e->get_data(); } SASSERT(m_table.contains(result)); - } return result; } }; diff --git a/src/util/util.cpp b/src/util/util.cpp index 4fb361475..714c947a9 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -17,12 +17,17 @@ Revision History: --*/ -#ifdef _WINDOWS -#include -#endif -#include #include "util/util.h" +#ifndef SINGLE_THREAD +#include +#include + +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; void set_verbosity_level(unsigned lvl) { @@ -39,23 +44,13 @@ void set_verbose_stream(std::ostream& str) { g_verbose_stream = &str; } -#ifndef _NO_OMP_ -#ifdef _WINDOWS -static int g_thread_id = 0; -#else +#ifndef SINGLE_THREAD static std::thread::id g_thread_id = std::this_thread::get_id(); -#endif static bool g_is_threaded = false; bool is_threaded() { if (g_is_threaded) return true; -#ifdef _WINDOWS - int thid = GetCurrentThreadId(); - g_is_threaded = g_thread_id != thid && g_thread_id != 0; - g_thread_id = thid; -#else g_is_threaded = std::this_thread::get_id() != g_thread_id; -#endif return g_is_threaded; } #endif diff --git a/src/util/util.h b/src/util/util.h index 9bc4f8a41..5860382c6 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -16,12 +16,10 @@ Author: Revision History: --*/ -#ifndef UTIL_H_ -#define UTIL_H_ +#pragma once #include "util/debug.h" #include "util/memory_manager.h" -#include "util/z3_omp.h" #include #include #include @@ -47,14 +45,10 @@ static_assert(sizeof(int64_t) == 8, "64 bits"); #endif #ifdef _WINDOWS -#define SSCANF sscanf_s -// #define SPRINTF sprintf_s #define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_) #define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_) #define _Exit exit #else -#define SSCANF sscanf -// #define SPRINTF sprintf #define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_) #define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_) #endif @@ -174,7 +168,7 @@ void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str); -#ifdef _NO_OMP_ +#ifdef SINGLE_THREAD # define is_threaded() false #else bool is_threaded(); @@ -191,24 +185,19 @@ bool is_threaded(); } \ } } ((void) 0) -#ifdef _MSC_VER -#define DO_PRAGMA(x) __pragma(x) -#define PRAGMA_LOCK __pragma(omp critical (verbose_lock)) -#else -#define DO_PRAGMA(x) _Pragma(#x) -#define PRAGMA_LOCK _Pragma("omp critical (verbose_lock)") -#endif -#ifdef _NO_OMP_ +#ifdef SINGLE_THREAD #define LOCK_CODE(CODE) CODE; #else -#define LOCK_CODE(CODE) \ - { \ - PRAGMA_LOCK \ - { \ - CODE; \ - } \ - } +void verbose_lock(); +void verbose_unlock(); + +#define LOCK_CODE(CODE) \ + { \ + verbose_lock(); \ + CODE; \ + verbose_unlock(); \ + } #endif template @@ -292,20 +281,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair const & p return out; } -template -bool has_duplicates(const IT & begin, const IT & end) { - for (IT it1 = begin; it1 != end; ++it1) { - IT it2 = it1; - ++it2; - for (; it2 != end; ++it2) { - if (*it1 == *it2) { - return true; - } - } - } - return false; -} - #ifndef _WINDOWS #ifndef __declspec #define __declspec(X) @@ -376,12 +351,6 @@ void shuffle(unsigned sz, T * array, random_gen & gen) { } } -#ifdef _EXTERNAL_RELEASE -#define INTERNAL_CODE(CODE) ((void) 0) -#else -#define INTERNAL_CODE(CODE) { CODE } ((void) 0) -#endif - void fatal_error(int error_code); void set_fatal_error_handler(void (*pfn)(int error_code)); @@ -420,7 +389,3 @@ inline size_t megabytes_to_bytes(unsigned mb) { r = SIZE_MAX; return r; } - - -#endif /* UTIL_H_ */ - diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp index 585313024..6b9e16a5d 100644 --- a/src/util/z3_exception.cpp +++ b/src/util/z3_exception.cpp @@ -16,7 +16,6 @@ Author: Notes: --*/ -#include #include #include #include "util/z3_exception.h" diff --git a/src/util/z3_omp.h b/src/util/z3_omp.h deleted file mode 100644 index 6c618192e..000000000 --- a/src/util/z3_omp.h +++ /dev/null @@ -1,38 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - z3_omp.h - -Abstract: - - Wrapper for OMP functions and data-structures - -Author: - - Leonardo (leonardo) 2012-01-05 - -Notes: - ---*/ -#ifndef Z3_OMP_H_ -#define Z3_OMP_H_ - -#ifndef _NO_OMP_ -#include -#else -#define omp_in_parallel() false -#define omp_set_num_threads(SZ) ((void)0) -#define omp_get_thread_num() 0 -#define omp_get_num_procs() 1 -#define omp_set_nested(V) ((void)0) -#define omp_init_nest_lock(L) ((void) 0) -#define omp_destroy_nest_lock(L) ((void) 0) -#define omp_set_nest_lock(L) ((void) 0) -#define omp_unset_nest_lock(L) ((void) 0) -struct omp_nest_lock_t { -}; -#endif - -#endif