From 61d79500435f3215f611602cbb499e4ed716ca17 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 18 Sep 2017 21:05:37 +0100 Subject: [PATCH 1/3] Ensure cxx11 is used in solver libraries --- scripts/glucose_CMakeLists.txt | 2 ++ scripts/minisat2_CMakeLists.txt | 2 ++ 2 files changed, 4 insertions(+) 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 From ad8a0eabba50502920bac091035ced9141d8e3c8 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 18 Sep 2017 21:10:38 +0100 Subject: [PATCH 2/3] Pass cxx compiler and flags to solver libraries --- src/CMakeLists.txt | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3af2d574f4b..7db3a84bc21 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -101,8 +101,12 @@ 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} + 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}" + "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}" + "-DCMAKE_CXX_FLAGS=${CMAKE_CXX_FLAGS}" BUILD_BYPRODUCTS ${minisat_lib} ) @@ -125,8 +129,11 @@ 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= + COMMAND cmake -E copy ${CMAKE_CURRENT_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} ) From bceb3758813750119f15d060a71696bab2ccac96 Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 19 Sep 2017 18:09:53 +0100 Subject: [PATCH 3/3] Move external project import to solvers CMakeLists --- src/CMakeLists.txt | 57 -------------------------------------- src/solvers/CMakeLists.txt | 53 +++++++++++++++++++++++++++++++++-- 2 files changed, 51 insertions(+), 59 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7db3a84bc21..476b3174189 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -89,63 +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}" - "-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) - -################################################################################ - -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=" - "-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) - -################################################################################ - # 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()