diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index 862fc8ba675..943c7df545d 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -6,6 +6,8 @@ cmake_minimum_required(VERSION 3.2) set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9") set(CMAKE_OSX_ARCHITECTURES "i386;x86_64") set(CMAKE_BUILD_TYPE RelWithDebInfo) +set(CMAKE_CXX_STANDARD 11) +set(CMAKE_CXX_STANDARD_REQUIRED true) add_library(glucose-condensed simp/SimpSolver.cc diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt index c749d0e4c8f..7ad80ad1278 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -6,6 +6,8 @@ cmake_minimum_required(VERSION 3.2) set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9") set(CMAKE_OSX_ARCHITECTURES "i386;x86_64") set(CMAKE_BUILD_TYPE RelWithDebInfo) +set(CMAKE_CXX_STANDARD 11) +set(CMAKE_CXX_STANDARD_REQUIRED true) add_library(minisat2-condensed minisat/simp/SimpSolver.cc diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3af2d574f4b..476b3174189 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -89,56 +89,6 @@ set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern) set(extern_include_directory ${extern_location}/include) file(MAKE_DIRECTORY ${extern_include_directory}) -################################################################################ - -set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX}) - -# minisat download: This downloads minisat2, then patches it. Then, it -# injects a minimal CMakeLists.txt so that we can build just the bits we -# actually want, without having to update the provided makefile. - -ExternalProject_Add(minisat2-extern - PREFIX ${extern_location} - URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz - PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch - COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt - CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH= -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR} - BUILD_BYPRODUCTS ${minisat_lib} -) - -add_library(minisat2-condensed STATIC IMPORTED) -set_target_properties(minisat2-condensed PROPERTIES - IMPORTED_LOCATION ${minisat_lib} - INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}" -) -add_dependencies(minisat2-condensed minisat2-extern) - -################################################################################ - -set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX}) - -# glucose download: This downloads glucose, then patches it. Then, it -# injects a minimal CMakeLists.txt so that we can build just the bits we -# actually want, without having to update the provided makefile. - -ExternalProject_Add(glucose-extern - PREFIX ${extern_location} - URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz - PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose-syrup-patch - COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt - CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH= - BUILD_BYPRODUCTS ${glucose_lib} -) - -add_library(glucose-condensed STATIC IMPORTED) -set_target_properties(glucose-condensed PROPERTIES - IMPORTED_LOCATION ${glucose_lib} - INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}" -) -add_dependencies(glucose-condensed glucose-extern) - -################################################################################ - # Override add_executable to automatically sign the target on OSX. function(add_executable name) _add_executable(${name} ${ARGN}) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 910b39f7c6e..0599ab1ab56 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -66,15 +66,64 @@ list(REMOVE_ITEM sources add_library(solvers ${sources} ${headers}) if("${sat_impl}" STREQUAL "minisat2") + set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX}) + + # minisat download: This downloads minisat2, then patches it. Then, it + # injects a minimal CMakeLists.txt so that we can build just the bits we + # actually want, without having to update the provided makefile. + + ExternalProject_Add(minisat2-extern + PREFIX ${extern_location} + URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt + CMAKE_ARGS + "-DCMAKE_INSTALL_PREFIX:PATH=" + "-DCBMC_INCLUDE_DIR:path=${CBMC_SOURCE_DIR}" + "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}" + "-DCMAKE_CXX_FLAGS=${CMAKE_CXX_FLAGS}" + BUILD_BYPRODUCTS ${minisat_lib} + ) + + add_library(minisat2-condensed STATIC IMPORTED) + set_target_properties(minisat2-condensed PROPERTIES + IMPORTED_LOCATION ${minisat_lib} + INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}" + ) + add_dependencies(minisat2-condensed minisat2-extern) + message(STATUS "Building solvers with minisat2") target_sources(solvers PRIVATE ${minisat2_source}) - add_dependencies(solvers minisat2-extern) target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS) target_link_libraries(solvers minisat2-condensed) elseif("${sat_impl}" STREQUAL "glucose") + set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX}) + + # glucose download: This downloads glucose, then patches it. Then, it + # injects a minimal CMakeLists.txt so that we can build just the bits we + # actually want, without having to update the provided makefile. + + ExternalProject_Add(glucose-extern + PREFIX ${extern_location} + URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt + CMAKE_ARGS + "-DCMAKE_INSTALL_PREFIX:PATH=" + "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}" + "-DCMAKE_CXX_FLAGS=${CMAKE_CXX_FLAGS}" + BUILD_BYPRODUCTS ${glucose_lib} + ) + + add_library(glucose-condensed STATIC IMPORTED) + set_target_properties(glucose-condensed PROPERTIES + IMPORTED_LOCATION ${glucose_lib} + INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}" + ) + add_dependencies(glucose-condensed glucose-extern) + message(STATUS "Building solvers with glucose") target_sources(solvers PRIVATE ${glucose_source}) - add_dependencies(solvers glucose-extern) target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS) target_link_libraries(solvers glucose-condensed) endif()