Skip to content

Solver CMake improvements #1402

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 3 commits into from
Closed

Solver CMake improvements #1402

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
61d7950
Ensure cxx11 is used in solver libraries
reuk Sep 18, 2017
ad8a0ea
Pass cxx compiler and flags to solver libraries
reuk Sep 18, 2017
bceb375
Move external project import to solvers CMakeLists
reuk Sep 19, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions scripts/glucose_CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions scripts/minisat2_CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
50 changes: 0 additions & 50 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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=<INSTALL_DIR> -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=<INSTALL_DIR>
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})
Expand Down
53 changes: 51 additions & 2 deletions src/solvers/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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=<INSTALL_DIR>"
"-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=<INSTALL_DIR>"
"-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()
Expand Down