Skip to content

CMake build system: support system-provided MiniSat #7644

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

Merged
merged 2 commits into from
May 31, 2023
Merged

CMake build system: support system-provided MiniSat #7644

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3246c2b
CMake build system: support system-provided MiniSat
tautschnig Apr 3, 2023
d8646ca
Add warning message in case static library is missing
tautschnig May 31, 2023
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
11 changes: 10 additions & 1 deletion src/libcprover-cpp/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,16 @@ target_link_libraries(cprover-api-cpp
# Here we prepare a space-separated list of cmake generators that will resolved in absolute paths.
set(DEPENDENCY_TARGETS "")
foreach(dep ${LIBRARY_DEPENDENCIES})
list(APPEND DEPENDENCY_TARGETS "$<TARGET_FILE:${dep}>")
if(TARGET ${dep})
list(APPEND DEPENDENCY_TARGETS "$<TARGET_FILE:${dep}>")
else()
find_library(dep_path ${dep})
string(REGEX REPLACE "[.]so$" ".a" dep_static_path ${dep_path})
if (NOT EXISTS "${dep_static_path}")
message(FATAL_ERROR "libcprover-cpp cannot be linked as dependency ${dep_path} does not have a static correspondent file (${dep_static_path})")
endif()
list(APPEND DEPENDENCY_TARGETS ${dep_static_path})
endif()
endforeach(dep LIBRARY_DEPENDENCIES)
string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}")

Expand Down
14 changes: 14 additions & 0 deletions src/solvers/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,20 @@ foreach(SOLVER ${sat_impl})
target_sources(solvers PRIVATE ${minisat2_source})

target_link_libraries(solvers minisat2-condensed)
elseif("${SOLVER}" STREQUAL "system-minisat2")
include(CheckIncludeFileCXX)
# if/when we move to CMake 3.12 (or later) we could also check for the
# library via CMAKE_REQUIRED_LIBRARIES
find_path(minisat_header_found "minisat/simp/SimpSolver.h")
if(minisat_header_found)
message(STATUS "Building solvers with minisat2 (${minisat_header_found})")
target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2)
target_sources(solvers PRIVATE ${minisat2_source})
target_include_directories(solvers PRIVATE ${minisat_header_found})
target_link_libraries(solvers minisat)
else()
message(FATAL_ERROR "Unable to find header file for preinstalled minisat2")
endif()
elseif("${SOLVER}" STREQUAL "glucose")
message(STATUS "Building solvers with glucose")

Expand Down