From c5542734baba00acf27d013e1d549e4dd0903916 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 1 Apr 2015 22:09:23 +0200 Subject: [PATCH 01/19] Fixing problems with compilation with C++11 compilers --- minisat/utils/Options.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h index 4e71a18c..9b470e00 100644 --- a/minisat/utils/Options.h +++ b/minisat/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); From 4d9462ed1c692dfae4f1b5fcd42cfc1b03ad71dd Mon Sep 17 00:00:00 2001 From: Jeroen Bransen Date: Thu, 19 Jun 2014 09:45:33 +0200 Subject: [PATCH 02/19] Remove illegal (and not neccesary) friend definition to fix compilation under clang. --- minisat/core/SolverTypes.h | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 89986d1e..5f387d84 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -51,16 +51,13 @@ typedef int Var; struct Lit { int x; - // Use this as a constructor: - friend Lit mkLit(Var var, bool sign = false); - bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering. }; -inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } +inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } inline bool sign (Lit p) { return p.x & 1; } From 3db58943b6ffe855d3b8c9a959300d9a148ab554 Mon Sep 17 00:00:00 2001 From: Ryan Govostes Date: Mon, 22 Jun 2015 08:36:06 +0200 Subject: [PATCH 03/19] Fix declaration of Minisat::memUsedPeak for non-Linux systems --- minisat/utils/System.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index 21aa4ff4..649f4a2c 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -87,11 +87,11 @@ double Minisat::memUsed() { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } -double Minisat::memUsedPeak() { return memUsed(); } +double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); } #else -double Minisat::memUsed() { return 0; } -double Minisat::memUsedPeak() { return 0; } +double Minisat::memUsed() { return 0; } +double Minisat::memUsedPeak(bool strictlyPeak) { return 0; } #endif From 26b58cf1c7ffcb6c3916a4cd3c851586c1185e92 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sat, 19 Mar 2016 23:42:57 +0000 Subject: [PATCH 04/19] Specify default argument in the declaration not the friend declaration --- minisat/core/SolverTypes.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 89986d1e..aa45ddb2 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -52,7 +52,7 @@ struct Lit { int x; // Use this as a constructor: - friend Lit mkLit(Var var, bool sign = false); + friend Lit mkLit(Var var, bool sign); bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } @@ -60,7 +60,7 @@ struct Lit { }; -inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } +inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } inline bool sign (Lit p) { return p.x & 1; } From 25ac527f9b9a1a7928b5cd66c26f58ec72f3c6a7 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 23 Apr 2017 16:10:24 +0100 Subject: [PATCH 05/19] Fixing Visual Studio build issues --- minisat/core/Solver.cc | 10 +++++----- minisat/utils/System.cc | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 0b4f77ad..699a5402 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -992,11 +992,11 @@ void Solver::printStats() const { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); + printf("restarts : %lu\n", starts); + printf("conflicts : %-12lu (%.0f /sec)\n", conflicts , conflicts /cpu_time); + printf("decisions : %-12lu (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); + printf("propagations : %-12lu (%.0f /sec)\n", propagations, propagations/cpu_time); + printf("conflict literals : %-12lu (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index 21aa4ff4..7aa22729 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -77,7 +77,7 @@ double Minisat::memUsed() { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } -double Minisat::memUsedPeak() { return memUsed(); } +double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); } #elif defined(__APPLE__) @@ -91,7 +91,7 @@ double Minisat::memUsedPeak() { return memUsed(); } #else double Minisat::memUsed() { return 0; } -double Minisat::memUsedPeak() { return 0; } +double Minisat::memUsedPeak(bool strictlyPeak) { return 0; } #endif From 7d4cb542bc4bdd1d1916a4f65a882ce79d95df6d Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 23 Apr 2017 16:14:54 +0100 Subject: [PATCH 06/19] Adding appveyor for minisat --- appveyor.yml | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) create mode 100644 appveyor.yml diff --git a/appveyor.yml b/appveyor.yml new file mode 100644 index 00000000..cbc9f261 --- /dev/null +++ b/appveyor.yml @@ -0,0 +1,94 @@ +# branches to build +branches: + # whitelist + only: + - master + - appveyor_debug + +# Operating system (build VM template) +os: Visual Studio 2015 + +# scripts that are called at very beginning, before repo cloning +init: + - git config --global core.autocrlf input + + +# clone directory +clone_folder: c:\projects\minisat + +platform: + - x64 +# - x86 + +environment: + global: + BOOST_ROOT: C:\projects\minisat\boost_1_59_0_install + ZLIB_ROOT: C:\projects\minisat\zlib\myinstall + BUILD_TYPE: Release + MSBUILD_FLAGS: /maxcpucount /nologo + +configuration: + - Release + +build_script: + #- IF "%PLATFORM%" == "x86" ( SET BOOST_LIBRARYDIR=C:/Libraries/boost_1_59_0/lib32-msvc-14.0) + - IF "%PLATFORM%" == "x86" ( SET CMAKE_GENERATOR="Visual Studio 14 2015") + + #- IF "%PLATFORM%" == "x64" ( SET BOOST_LIBRARYDIR=C:/Libraries/boost_1_59_0/lib64-msvc-14.0) + - IF "%PLATFORM%" == "x64" ( SET CMAKE_GENERATOR="Visual Studio 14 2015 Win64") + + - echo %PLATFORM% + - echo %BOOST_LIBRARYDIR% + - echo %CMAKE_GENERATOR% + - echo %configuration% + - echo %APPVEYOR_BUILD_FOLDER% + - echo %cd% + + # zlib + # TODO check out http://stackoverflow.com/questions/10507893/libzip-with-visual-studio-2010 + - cd C:\projects\minisat + - git clone https://github.com/madler/zlib + - cd zlib + - git checkout v1.2.8 + - echo %cd% + - mkdir build + - mkdir myinstall + - cd build + - cmake -G %CMAKE_GENERATOR% -DCMAKE_INSTALL_PREFIX=%ZLIB_ROOT% .. + - if %PLATFORM%==x86 call msbuild %MSBUILD_FLAGS% /t:Build /p:Configuration=%CONFIGURATION% /p:Platform="x86" zlib.sln + - if %PLATFORM%==x64 call msbuild %MSBUILD_FLAGS% /t:Build /p:Configuration=%CONFIGURATION% /p:Platform="x64" zlib.sln + - msbuild %MSBUILD_FLAGS% INSTALL.vcxproj + - dir ..\myinstall\ + + # minisat + - cd C:\projects\minisat + - cd minisat + - echo %cd% + - mkdir build + - mkdir myinstall + - cd build + - cmake -G %CMAKE_GENERATOR% -DCMAKE_INSTALL_PREFIX=%MINISAT_ROOT% -DZLIB_ROOT=%ZLIB_ROOT% .. + - cmake --build . --config %CONFIGURATION% + - dir ..\myinstall\ + + +build: + # project: INSTALL.vcxproj # path to Visual Studio solution or project + parallel: true + verbosity: minimal + + +# scripts to run after build +after_build: + - 7z a c:\projects\minisat\minisat.zip %APPVEYOR_BUILD_FOLDER%\build -tzip + - cd c:\projects\minisat + +artifacts: + - path: minisat.zip + name: minisat.zip + +deploy_script: + #- cd c:\projects\minisat + #- curl -T minisat.zip --user %ACCOUNT% https://someplace/ + +test: off From 5566d44ab433fa3efc3c827d318ffbc8f06b8e3d Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 23 Apr 2017 16:17:47 +0100 Subject: [PATCH 07/19] Fixing appveyor build --- appveyor.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/appveyor.yml b/appveyor.yml index cbc9f261..a352a37c 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -62,8 +62,6 @@ build_script: # minisat - cd C:\projects\minisat - - cd minisat - - echo %cd% - mkdir build - mkdir myinstall - cd build From a98e44fcbcf8817b83b7bb617df55e7a30dcb08d Mon Sep 17 00:00:00 2001 From: Robbepop Date: Thu, 27 Apr 2017 19:25:53 +0200 Subject: [PATCH 08/19] fixed GCC 6.3 warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix] --- minisat/utils/Options.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h index 4e71a18c..7d2e83a8 100644 --- a/minisat/utils/Options.h +++ b/minisat/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); From 1aa1e871aad1fe2f80510b42e93f28d4fb1286a0 Mon Sep 17 00:00:00 2001 From: MartinNowack Date: Sat, 30 Jun 2018 00:25:19 +0100 Subject: [PATCH 09/19] Fix linking of minisat as dependency library on MacOSX RPath needed by MacOSX was not correctly set for minisat. Therefore it was not correctly linked against STP. --- CMakeLists.txt | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index ae4da001..061a61ae 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -23,6 +23,13 @@ else() endif() set(MINISAT_SOVERSION ${MINISAT_SOMAJOR}) +# Reference specific library paths used during linking for install +if (POLICY CMP0042) + # Enable `MACOSX_RPATH` by default. + cmake_policy(SET CMP0042 NEW) +endif() +SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) + #-------------------------------------------------------------------------------------------------- # Dependencies: From dbef9787682557e40fcfe9b7eb527aecb4731feb Mon Sep 17 00:00:00 2001 From: Brian Foley Date: Tue, 11 Feb 2020 18:41:50 -0800 Subject: [PATCH 10/19] Quell some clang warnings --- minisat/core/Solver.cc | 10 +++++----- minisat/utils/System.cc | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 699a5402..6175cb4f 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -992,11 +992,11 @@ void Solver::printStats() const { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %lu\n", starts); - printf("conflicts : %-12lu (%.0f /sec)\n", conflicts , conflicts /cpu_time); - printf("decisions : %-12lu (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); - printf("propagations : %-12lu (%.0f /sec)\n", propagations, propagations/cpu_time); - printf("conflict literals : %-12lu (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); + printf("restarts : %" PRIu64 "\n", starts); + printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time); + printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); + printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time); + printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index c665357b..282f98ed 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -77,7 +77,7 @@ double Minisat::memUsed() { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } -double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); } +double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return memUsed(); } #elif defined(__APPLE__) @@ -87,11 +87,11 @@ double Minisat::memUsed() { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } -double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); } +double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return memUsed(); } #else double Minisat::memUsed() { return 0; } -double Minisat::memUsedPeak(bool strictlyPeak) { return 0; } +double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return 0; } #endif From 93da0f0799a2d70c4e17880799c2b34e818fd1b5 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 28 Feb 2019 21:09:08 +0100 Subject: [PATCH 11/19] Fixing static vs. dynamic compile --- CMakeLists.txt | 158 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 142 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 061a61ae..850eb1f7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -42,6 +42,140 @@ include_directories(${minisat_SOURCE_DIR}) add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS) + +#-------------------------------------------------------------------------------------------------- +option(STATICCOMPILE "Compile static library and executable" OFF) + +option(BUILD_SHARED_LIBS "Build the shared library" ON) +option(STATICCOMPILE "Compile to static executable" OFF) +if (STATICCOMPILE) + set(BUILD_SHARED_LIBS OFF) +endif() + +if (NOT BUILD_SHARED_LIBS) + if (NOT MSVC) + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static -Wl,--whole-archive -lpthread -Wl,--no-whole-archive -static ") + set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") + + # removing -rdynamic that's automatically added + foreach (language CXX C) + set(VAR_TO_MODIFY "CMAKE_SHARED_LIBRARY_LINK_${language}_FLAGS") + string(REGEX REPLACE "(^| )-rdynamic($| )" + " " + replacement + "${${VAR_TO_MODIFY}}") + #message("Original (${VAR_TO_MODIFY}) is ${${VAR_TO_MODIFY}} replacement is ${replacement}") + set(${VAR_TO_MODIFY} "${replacement}" CACHE STRING "Default flags for ${build_config} configuration" FORCE) + endforeach() + endif() +else () + # use, i.e. don't skip the full RPATH for the build tree + SET(CMAKE_SKIP_BUILD_RPATH FALSE) + + # when building, don't use the install RPATH already + # (but later on when installing) + SET(CMAKE_BUILD_WITH_INSTALL_RPATH FALSE) + + SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_LIBDIR}") + + # add the automatically determined parts of the RPATH + # which point to directories outside the build tree to the install RPATH + SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) + + # the RPATH to be used when installing, but only if it's not a system directory + LIST(FIND CMAKE_PLATFORM_IMPLICIT_LINK_DIRECTORIES "${CMAKE_INSTALL_LIBDIR}" isSystemDir) + IF("${isSystemDir}" STREQUAL "-1") + SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_LIBDIR}") + ENDIF("${isSystemDir}" STREQUAL "-1") + + if (APPLE) + set(CMAKE_MACOSX_RPATH ON) + set(CMAKE_INSTALL_RPATH "@loader_path/../lib") + message(STATUS "Using RPATH for dynamic linking") + endif() +endif() + +if (NOT MSVC) + add_compile_options( -g) + add_compile_options( -pthread ) + + add_compile_options("$<$:-O2>") + + add_compile_options("$<$:-O2>") + add_compile_options("$<$:-g0>") + + add_compile_options("$<$:-O0>") + + if(NOT CMAKE_BUILD_TYPE STREQUAL "Debug") + set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -O2") + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -O2") + endif() +else() + # see https://msdn.microsoft.com/en-us/library/fwkeyyhe.aspx for details + # /ZI = include debug info + # /Wall = all warnings + + add_compile_options("$<$:/O2>") + add_compile_options("$<$:/ZI>") + + add_compile_options("$<$:/O2>") + add_compile_options("$<$:/D>") + add_compile_options("$<$:/NDEBUG>") + + add_compile_options("$<$:/Od>") + + if (NOT BUILD_SHARED_LIBS) + # We statically link to reduce dependencies + foreach(flag_var CMAKE_CXX_FLAGS CMAKE_CXX_FLAGS_DEBUG CMAKE_CXX_FLAGS_RELEASE CMAKE_CXX_FLAGS_MINSIZEREL CMAKE_CXX_FLAGS_RELWITHDEBINFO) + # /MD -- Causes the application to use the multithread-specific + # and DLL-specific version of the run-time library. + # Defines _MT and _DLL and causes the compiler to place + # the library name MSVCRT.lib into the .obj file. + if(${flag_var} MATCHES "/MD") + string(REGEX REPLACE "/MD" "/MT" ${flag_var} "${${flag_var}}") + endif(${flag_var} MATCHES "/MD") + + # /MDd -- Defines _DEBUG, _MT, and _DLL and causes the application to use the debug multithread-specific and DLL-specific version of the run-time library. + # It also causes the compiler to place the library name MSVCRTD.lib into the .obj file. + if(${flag_var} MATCHES "/MDd") + string(REGEX REPLACE "/MDd" "/MTd" ${flag_var} "${${flag_var}}") + endif(${flag_var} MATCHES "/MDd") + endforeach(flag_var) + + # Creates a multithreaded executable (static) file using LIBCMT.lib. + add_compile_options(/MT) + endif() + + # buffers security check + add_compile_options(/GS) + + # Proper warning level + add_compile_options(/W1) + + # Disable STL used in DLL-boundary warning + add_compile_options(/wd4251) + add_compile_options(/D_CRT_SECURE_NO_WARNINGS) + + # Wall is MSVC's Weverything, so annoying unless used from the start + # and with judiciously used warning disables + # add_compile_options(/Wall) + + # /Za = only ansi C98 & C++11 + # /Za is not recommended for use, not tested, etc. + # see: http://stackoverflow.com/questions/5489326/za-compiler-directive-does-not-compile-system-headers-in-vs2010 + # add_compile_options(/Za) + + add_compile_options(/fp:precise) + + # exception handling. s = The exception-handling model that catches C++ exceptions only and tells the compiler to assume that functions declared as extern "C" may throw an exception. + # exception handling. c = If used with s (/EHsc), catches C++ exceptions only and tells the compiler to assume that functions declared as extern "C" never throw a C++ exception. + add_compile_options(/EHsc) + + #what does this do? + set(DEF_INSTALL_CMAKE_DIR CMake) +endif() + + #-------------------------------------------------------------------------------------------------- # Build Targets: @@ -51,27 +185,19 @@ set(MINISAT_LIB_SOURCES minisat/core/Solver.cc minisat/simp/SimpSolver.cc) -add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES}) -add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES}) - -target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY}) -target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY}) +add_library(minisat ${MINISAT_LIB_SOURCES}) +target_link_libraries(minisat ${ZLIB_LIBRARY}) add_executable(minisat_core minisat/core/Main.cc) add_executable(minisat_simp minisat/simp/Main.cc) -if(STATIC_BINARIES) - target_link_libraries(minisat_core minisat-lib-static) - target_link_libraries(minisat_simp minisat-lib-static) -else() - target_link_libraries(minisat_core minisat-lib-shared) - target_link_libraries(minisat_simp minisat-lib-shared) -endif() -set_target_properties(minisat-lib-static PROPERTIES OUTPUT_NAME "minisat") -set_target_properties(minisat-lib-shared +target_link_libraries(minisat_core minisat) +target_link_libraries(minisat_simp minisat) + +set_target_properties(minisat PROPERTIES - OUTPUT_NAME "minisat" + OUTPUT_NAME "minisat" VERSION ${MINISAT_VERSION} SOVERSION ${MINISAT_SOVERSION}) @@ -80,7 +206,7 @@ set_target_properties(minisat_simp PROPERTIES OUTPUT_NAME "minisat") #-------------------------------------------------------------------------------------------------- # Installation targets: -install(TARGETS minisat-lib-static minisat-lib-shared minisat_core minisat_simp +install(TARGETS minisat minisat_core minisat_simp RUNTIME DESTINATION bin LIBRARY DESTINATION lib ARCHIVE DESTINATION lib) From a2c6fe6830ae5550045acc02b226d4f54563012e Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 31 Aug 2020 20:53:38 +0200 Subject: [PATCH 12/19] Export minisat project for other cmake builds --- CMakeLists.txt | 46 ++++++++++++++++++++++++++++++++++++++++++ minisatConfig.cmake.in | 18 +++++++++++++++++ 2 files changed, 64 insertions(+) create mode 100644 minisatConfig.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 850eb1f7..54591fe9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -36,6 +36,7 @@ SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) find_package(ZLIB) include_directories(${ZLIB_INCLUDE_DIR}) include_directories(${minisat_SOURCE_DIR}) +include (GenerateExportHeader) #-------------------------------------------------------------------------------------------------- # Compile flags: @@ -174,6 +175,7 @@ else() #what does this do? set(DEF_INSTALL_CMAKE_DIR CMake) endif() +set(MINISAT_EXPORT_NAME "minisatTargets") #-------------------------------------------------------------------------------------------------- @@ -207,6 +209,7 @@ set_target_properties(minisat_simp PROPERTIES OUTPUT_NAME "minisat") # Installation targets: install(TARGETS minisat minisat_core minisat_simp + EXPORT ${MINISAT_EXPORT_NAME} RUNTIME DESTINATION bin LIBRARY DESTINATION lib ARCHIVE DESTINATION lib) @@ -214,3 +217,46 @@ install(TARGETS minisat minisat_core minisat_simp install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp DESTINATION include/minisat FILES_MATCHING PATTERN "*.h") + +# Setup for export +set(MINISAT_TARGETS_FILENAME "minisatTargets.cmake") +set(MINISAT_CONFIG_FILENAME "minisatConfig.cmake") + +# Export targets +export( + TARGETS minisat + FILE "${CMAKE_CURRENT_BINARY_DIR}/${MINISAT_TARGETS_FILENAME}" +) + +# Create minisatConfig file +set(EXPORT_TYPE "Build-tree") +set(CONF_INCLUDE_DIRS "${CMAKE_CURRENT_BINARY_DIR}/include") +configure_file(minisatConfig.cmake.in + "${CMAKE_CURRENT_BINARY_DIR}/${MINISAT_CONFIG_FILENAME}" @ONLY +) + +# Export this package to the CMake user package registry +# Now the user can just use find_package(minisat) on their system +export(PACKAGE minisat) + +set(DEF_INSTALL_CMAKE_DIR lib/cmake/minisat) +set(MINISAT_INSTALL_CMAKE_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH + "Installation directory for minisat CMake files") + +# Create minisatConfig file +set(EXPORT_TYPE "installed") +set(CONF_INCLUDE_DIRS "${CMAKE_INSTALL_PREFIX}/include") +configure_file(minisatConfig.cmake.in + "${CMAKE_CURRENT_BINARY_DIR}/${CMAKE_FILES_DIRECTORY}/${MINISAT_CONFIG_FILENAME}" @ONLY +) + +install(FILES + "${CMAKE_CURRENT_BINARY_DIR}/${CMAKE_FILES_DIRECTORY}/${MINISAT_CONFIG_FILENAME}" + DESTINATION "${MINISAT_INSTALL_CMAKE_DIR}" +) + +# Install the export set for use with the install-tree +install( + EXPORT ${MINISAT_EXPORT_NAME} + DESTINATION "${MINISAT_INSTALL_CMAKE_DIR}" +) diff --git a/minisatConfig.cmake.in b/minisatConfig.cmake.in new file mode 100644 index 00000000..82e95bbc --- /dev/null +++ b/minisatConfig.cmake.in @@ -0,0 +1,18 @@ +# Config file for the @EXPORT_TYPE@ cryptominisat Package +# It defines the following variables +# MINISAT_INCLUDE_DIR - include directories for minisat +# MINISAT_LIBRARY - libraries to link against +# MINISAT_EXECUTABLE - the cryptominisat executable + +# Compute paths +get_filename_component(MINISAT_CMAKE_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH) +set(MINISAT_INCLUDE_DIR "@CONF_INCLUDE_DIRS@") + +# Our library dependencies (contains definitions for IMPORTED targets) +include("${MINISAT_CMAKE_DIR}/@MINISAT_TARGETS_FILENAME@") + +# These are IMPORTED targets created by @MINISAT_TARGETS_FILENAME@ +set(MINISAT_LIBRARY minisat) +set(MINISAT_VERSION_MAJOR @PROJECT_VERSION_MAJOR@) +set(MINISAT_VERSION_MINOR @PROJECT_VERSION_MINOR@) +set(MINISAT_EXECUTABLE minisat) From dd3145082c4c5ef9d4976816f35e7b83db96fa75 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 31 Aug 2020 21:06:00 +0200 Subject: [PATCH 13/19] Updating to fix build --- CMakeLists.txt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 54591fe9..9d71306f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -230,7 +230,7 @@ export( # Create minisatConfig file set(EXPORT_TYPE "Build-tree") -set(CONF_INCLUDE_DIRS "${CMAKE_CURRENT_BINARY_DIR}/include") +set(CONF_INCLUDE_DIRS "${minisat_SOURCE_DIR}/") configure_file(minisatConfig.cmake.in "${CMAKE_CURRENT_BINARY_DIR}/${MINISAT_CONFIG_FILENAME}" @ONLY ) @@ -245,7 +245,6 @@ set(MINISAT_INSTALL_CMAKE_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH # Create minisatConfig file set(EXPORT_TYPE "installed") -set(CONF_INCLUDE_DIRS "${CMAKE_INSTALL_PREFIX}/include") configure_file(minisatConfig.cmake.in "${CMAKE_CURRENT_BINARY_DIR}/${CMAKE_FILES_DIRECTORY}/${MINISAT_CONFIG_FILENAME}" @ONLY ) From 1193f18c7b49e8f93d9f57a8beebbe6bd70cb1b0 Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Mon, 4 Nov 2019 09:56:20 +0100 Subject: [PATCH 14/19] CMakeLists: support different lib dirs On 64bit systems, the usual destination for libraries is /usr/lib64, not /usr/lib. So add CMAKE_INSTALL_LIBDIR and allow overriding the the default. --- CMakeLists.txt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9d71306f..82233a8f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -208,11 +208,12 @@ set_target_properties(minisat_simp PROPERTIES OUTPUT_NAME "minisat") #-------------------------------------------------------------------------------------------------- # Installation targets: +set(CMAKE_INSTALL_LIBDIR lib CACHE STRING "Output directory for libraries") install(TARGETS minisat minisat_core minisat_simp EXPORT ${MINISAT_EXPORT_NAME} RUNTIME DESTINATION bin - LIBRARY DESTINATION lib - ARCHIVE DESTINATION lib) + LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} + ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}) install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp DESTINATION include/minisat From 5f9111fdb64e635a3babd529ad985a862213667d Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 2 Sep 2020 19:38:10 +0200 Subject: [PATCH 15/19] Removing second STATICCOMPILE --- CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 82233a8f..b8a465e5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -48,7 +48,6 @@ add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS) option(STATICCOMPILE "Compile static library and executable" OFF) option(BUILD_SHARED_LIBS "Build the shared library" ON) -option(STATICCOMPILE "Compile to static executable" OFF) if (STATICCOMPILE) set(BUILD_SHARED_LIBS OFF) endif() From 5b16571e643cde5725d525f30675581de0d5c936 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 2 Sep 2020 21:59:19 +0200 Subject: [PATCH 16/19] Revert "CMakeLists: support different lib dirs" This reverts commit 1193f18c7b49e8f93d9f57a8beebbe6bd70cb1b0. --- CMakeLists.txt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index b8a465e5..d88c0006 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -207,12 +207,11 @@ set_target_properties(minisat_simp PROPERTIES OUTPUT_NAME "minisat") #-------------------------------------------------------------------------------------------------- # Installation targets: -set(CMAKE_INSTALL_LIBDIR lib CACHE STRING "Output directory for libraries") install(TARGETS minisat minisat_core minisat_simp EXPORT ${MINISAT_EXPORT_NAME} RUNTIME DESTINATION bin - LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} - ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}) + LIBRARY DESTINATION lib + ARCHIVE DESTINATION lib) install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp DESTINATION include/minisat From 5a38d3638453dbc23636fd23e998bbadc7c6c19d Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 2 Sep 2020 22:31:45 +0200 Subject: [PATCH 17/19] Adding uninstall capability --- CMakeLists.txt | 13 +++++++++++++ cmake_uninstall.cmake.in | 24 ++++++++++++++++++++++++ 2 files changed, 37 insertions(+) create mode 100644 cmake_uninstall.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index d88c0006..465fd913 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -176,6 +176,19 @@ else() endif() set(MINISAT_EXPORT_NAME "minisatTargets") +# ----------------------------------------------------------------------------- +# Add uninstall target for makefiles +# ----------------------------------------------------------------------------- +configure_file( + "${CMAKE_CURRENT_SOURCE_DIR}/cmake_uninstall.cmake.in" + "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" + IMMEDIATE @ONLY +) + +add_custom_target(uninstall + COMMAND ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake +) + #-------------------------------------------------------------------------------------------------- # Build Targets: diff --git a/cmake_uninstall.cmake.in b/cmake_uninstall.cmake.in new file mode 100644 index 00000000..13cedcc5 --- /dev/null +++ b/cmake_uninstall.cmake.in @@ -0,0 +1,24 @@ +cmake_policy(SET CMP0007 NEW) # Suppress warnings see `cmake --help-policy CMP0007` + +if (NOT EXISTS "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt") + message(FATAL_ERROR "Cannot find install manifest: \"@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt\"") +endif(NOT EXISTS "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt") + +file(READ "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt" files) +string(REGEX REPLACE "\n" ";" files "${files}") +list(REVERSE files) +foreach (file ${files}) + message(STATUS "Uninstalling \"$ENV{DESTDIR}${file}\"") + if (EXISTS "$ENV{DESTDIR}${file}") + execute_process( + COMMAND @CMAKE_COMMAND@ -E remove "$ENV{DESTDIR}${file}" + OUTPUT_VARIABLE rm_out + RESULT_VARIABLE rm_retval + ) + if(NOT ${rm_retval} EQUAL 0) + message(FATAL_ERROR "Problem when removing \"$ENV{DESTDIR}${file}\"") + endif (NOT ${rm_retval} EQUAL 0) + else (EXISTS "$ENV{DESTDIR}${file}") + message(STATUS "File \"$ENV{DESTDIR}${file}\" does not exist.") + endif (EXISTS "$ENV{DESTDIR}${file}") +endforeach(file) From 37158a35c62d448b3feccfa83006266e12e5acb7 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 2 Sep 2020 22:31:58 +0200 Subject: [PATCH 18/19] Fixing exported definitions --- minisatConfig.cmake.in | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/minisatConfig.cmake.in b/minisatConfig.cmake.in index 82e95bbc..90ef7da1 100644 --- a/minisatConfig.cmake.in +++ b/minisatConfig.cmake.in @@ -1,18 +1,18 @@ # Config file for the @EXPORT_TYPE@ cryptominisat Package # It defines the following variables -# MINISAT_INCLUDE_DIR - include directories for minisat -# MINISAT_LIBRARY - libraries to link against +# MINISAT_INCLUDE_DIRS - include directories for minisat +# MINISAT_LIBRARIES - libraries to link against # MINISAT_EXECUTABLE - the cryptominisat executable # Compute paths get_filename_component(MINISAT_CMAKE_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH) -set(MINISAT_INCLUDE_DIR "@CONF_INCLUDE_DIRS@") +set(MINISAT_INCLUDE_DIRS "@CONF_INCLUDE_DIRS@") # Our library dependencies (contains definitions for IMPORTED targets) include("${MINISAT_CMAKE_DIR}/@MINISAT_TARGETS_FILENAME@") # These are IMPORTED targets created by @MINISAT_TARGETS_FILENAME@ -set(MINISAT_LIBRARY minisat) +set(MINISAT_LIBRARIES minisat) set(MINISAT_VERSION_MAJOR @PROJECT_VERSION_MAJOR@) set(MINISAT_VERSION_MINOR @PROJECT_VERSION_MINOR@) set(MINISAT_EXECUTABLE minisat) From 4c8afcd6bfbf2cbdb5ebe271f20503a6d34d7d49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maciej=20Bar=C4=87?= Date: Mon, 6 Feb 2023 17:09:18 +0100 Subject: [PATCH 19/19] utils/System.*: use fpu_control only on glibc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bug: https://github.com/vprover/vampire/pull/432 Signed-off-by: Maciej Barć --- minisat/utils/System.cc | 2 +- minisat/utils/System.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index 282f98ed..112708f7 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -97,7 +97,7 @@ double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return 0; } void Minisat::setX86FPUPrecision() { -#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW) +#if defined(__GLIBC__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW) // Only correct FPU precision on Linux architectures that needs and supports it: fpu_control_t oldcw, newcw; _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); diff --git a/minisat/utils/System.h b/minisat/utils/System.h index a51d4c2e..189fcbff 100644 --- a/minisat/utils/System.h +++ b/minisat/utils/System.h @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_System_h #define Minisat_System_h -#if defined(__linux__) +#if defined(__GLIBC__) #include #endif