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.

The required support for external libraries also addresses #7641.

Fixes: #7641

Author: tautschnig

src/libcprover-cpp/CMakeLists.txt

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

src/solvers/CMakeLists.txt

@@ -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")