Skip to content

Commit 88c2f9c

Browse files
reukreuk
committed
Use DownloadProject method for integrating sat libraries
1 parent bc593c5 commit 88c2f9c

File tree

4 files changed

+33
-101
lines changed

4 files changed

+33
-101
lines changed

‎scripts/glucose_CMakeLists.txt

+1-19
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,12 @@
1-
cmake_minimum_required(VERSION 3.2)
2-
31
# CBMC only uses part of glucose.
42
# This CMakeLists is designed to build just the parts that are needed.
53

6-
set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
7-
set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
8-
set(CMAKE_BUILD_TYPE RelWithDebInfo)
9-
104
add_library(glucose-condensed
115
simp/SimpSolver.cc
126
core/Solver.cc
137
)
148

159
target_include_directories(glucose-condensed
1610
PUBLIC
17-
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
18-
$<INSTALL_INTERFACE:include>
19-
)
20-
21-
install(TARGETS glucose-condensed EXPORT glucose-condensed-targets
22-
LIBRARY DESTINATION lib
23-
ARCHIVE DESTINATION lib
24-
RUNTIME DESTINATION bin
25-
INCLUDES DESTINATION include
11+
${CMAKE_CURRENT_SOURCE_DIR}
2612
)
27-
28-
install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
29-
30-
install(EXPORT glucose-condensed-targets DESTINATION lib/cmake/glucose-condensed)

‎scripts/minisat2_CMakeLists.txt

+2-21
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,14 @@
1-
cmake_minimum_required(VERSION 3.2)
2-
31
# CBMC only uses part of minisat2.
42
# This CMakeLists is designed to build just the parts that are needed.
53

6-
set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
7-
set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
8-
set(CMAKE_BUILD_TYPE RelWithDebInfo)
9-
104
add_library(minisat2-condensed
115
minisat/simp/SimpSolver.cc
126
minisat/core/Solver.cc
137
)
148

15-
set(CBMC_INCLUDE_DIR "" CACHE PATH "The path to CBMC util headers")
16-
179
target_include_directories(minisat2-condensed
1810
PUBLIC
19-
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
20-
$<BUILD_INTERFACE:${CBMC_INCLUDE_DIR}>
21-
$<INSTALL_INTERFACE:include>
11+
${CMAKE_CURRENT_SOURCE_DIR}
2212
)
2313

24-
install(TARGETS minisat2-condensed EXPORT minisat-condensed-targets
25-
LIBRARY DESTINATION lib
26-
ARCHIVE DESTINATION lib
27-
RUNTIME DESTINATION bin
28-
INCLUDES DESTINATION include
29-
)
30-
31-
install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
32-
33-
install(EXPORT minisat-condensed-targets DESTINATION lib/cmake/minisat-condensed)
14+
target_link_libraries(minisat2-condensed util)

‎src/CMakeLists.txt

-57
Original file line numberDiff line numberDiff line change
@@ -82,63 +82,6 @@ macro(add_if_library target name)
8282
endif()
8383
endmacro(add_if_library)
8484

85-
# EXTERNAL PROJECTS
86-
include(ExternalProject)
87-
set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern)
88-
89-
set(extern_include_directory ${extern_location}/include)
90-
file(MAKE_DIRECTORY ${extern_include_directory})
91-
92-
################################################################################
93-
94-
set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
95-
96-
# minisat download: This downloads minisat2, then patches it. Then, it
97-
# injects a minimal CMakeLists.txt so that we can build just the bits we
98-
# actually want, without having to update the provided makefile.
99-
100-
ExternalProject_Add(minisat2-extern
101-
PREFIX ${extern_location}
102-
URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
103-
PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
104-
COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
105-
CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR> -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR}
106-
BUILD_BYPRODUCTS ${minisat_lib}
107-
)
108-
109-
add_library(minisat2-condensed STATIC IMPORTED)
110-
set_target_properties(minisat2-condensed PROPERTIES
111-
IMPORTED_LOCATION ${minisat_lib}
112-
INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
113-
)
114-
add_dependencies(minisat2-condensed minisat2-extern)
115-
116-
################################################################################
117-
118-
set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
119-
120-
# glucose download: This downloads glucose, then patches it. Then, it
121-
# injects a minimal CMakeLists.txt so that we can build just the bits we
122-
# actually want, without having to update the provided makefile.
123-
124-
ExternalProject_Add(glucose-extern
125-
PREFIX ${extern_location}
126-
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
127-
PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose-syrup-patch
128-
COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
129-
CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
130-
BUILD_BYPRODUCTS ${glucose_lib}
131-
)
132-
133-
add_library(glucose-condensed STATIC IMPORTED)
134-
set_target_properties(glucose-condensed PROPERTIES
135-
IMPORTED_LOCATION ${glucose_lib}
136-
INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
137-
)
138-
add_dependencies(glucose-condensed glucose-extern)
139-
140-
################################################################################
141-
14285
# Override add_executable to automatically sign the target on OSX.
14386
function(add_executable name)
14487
_add_executable(${name} ${ARGN})

‎src/solvers/CMakeLists.txt

+30-4
Original file line numberDiff line numberDiff line change
@@ -65,17 +65,43 @@ list(REMOVE_ITEM sources
6565

6666
add_library(solvers ${sources} ${headers})
6767

68+
include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
69+
6870
if("${sat_impl}" STREQUAL "minisat2")
6971
message(STATUS "Building solvers with minisat2")
72+
73+
download_project(PROJ minisat2
74+
URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
75+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
76+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
77+
)
78+
79+
add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
80+
81+
target_compile_definitions(solvers PUBLIC
82+
SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
83+
)
84+
7085
target_sources(solvers PRIVATE ${minisat2_source})
71-
add_dependencies(solvers minisat2-extern)
72-
target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
86+
7387
target_link_libraries(solvers minisat2-condensed)
7488
elseif("${sat_impl}" STREQUAL "glucose")
7589
message(STATUS "Building solvers with glucose")
90+
91+
download_project(PROJ glucose
92+
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
93+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
94+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
95+
)
96+
97+
add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
98+
99+
target_compile_definitions(solvers PUBLIC
100+
SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
101+
)
102+
76103
target_sources(solvers PRIVATE ${glucose_source})
77-
add_dependencies(solvers glucose-extern)
78-
target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
104+
79105
target_link_libraries(solvers glucose-condensed)
80106
endif()
81107

0 commit comments

Comments
 (0)