CMake build system: support system-provided MiniSat

Some operating systems provide packaged versions of MiniSat. When
building distribution packages it may then be preferable to use the
pre-installed library instead of building the solver object from
scratch. With this patch it is now possible to select "system-minisat2"
as a solver, alongside any other solvers that may be built from scratch.

Author: tautschnig

src/libcprover-cpp/CMakeLists.txt

@@ -61,7 +61,9 @@ 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}>")
+    endif()
 endforeach(dep LIBRARY_DEPENDENCIES)
 string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}")
 

src/solvers/CMakeLists.txt

@@ -87,6 +87,17 @@ 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
+        CHECK_INCLUDE_FILE_CXX("minisat/simp/SimpSolver.h" minisat_header_found)
+        if(${minisat_header_found})
+            message(STATUS "Building solvers with minisat2 (pre-built)")
+            target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2)
+            target_sources(solvers PRIVATE ${minisat2_source})
+            target_link_libraries(solvers minisat)
+        endif()
     elseif("${SOLVER}" STREQUAL "glucose")
         message(STATUS "Building solvers with glucose")