Merge pull request #6075 from NlightNFotis/cmake_ipasir

Add CMake support for building and linking against CaDiCaL using the IPASIR interface

Author: TGWDB

CMakeLists.txt

@@ -81,7 +81,7 @@ set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
 
 set(sat_impl "minisat2" CACHE STRING
     "This setting controls the SAT library which is used. Valid values are
-    'minisat2', 'glucose', or 'cadical'"
+    'minisat2', 'glucose', 'cadical', 'ipasir-cadical' or 'ipasir-custom'"
 )
 
 if(${enable_cbmc_tests})

COMPILING.md

@@ -462,6 +462,27 @@ Note that at the time of writing this has been tested to work with the CaDiCaL
    the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
    compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
 
+---
+
+It's also possible to build CBMC using CaDiCaL through IPASIR via `cmake`,
+controlled with the flag `-Dsat_impl=ipasir-cadical`, like so:
+
+```sh
+$ cmake -Bbuild_ipasir -S. -Dsat_impl=ipasir-cadical
+```
+
+An advanced user may also take a more adventurous route, trying to link
+CBMC against any solver supporthing the IPASIR interface. To do that,
+an invocation like this is needed:
+
+```sh
+$ cmake -Bbuild_ipasir -S . -Dsat_impl=ipasir-custom -DIPASIR=<source_location> -DIPASIR_LIB=<lib_location>
+```
+
+with `<source_location>` being the absolute path to the folder containing
+the solver implementation and `<lib_location>` being the absolute path that
+contains a precompiled static library of the solver (`.a` file).
+
 #### Compiling with Riss via IPASIR
 
 The [Riss](https://github.com/conp-solutions/riss) solver supports the

src/solvers/CMakeLists.txt

@@ -38,6 +38,10 @@ set(booleforce_source
 set(minibdd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/bdd/miniBDD/example.cpp
 )
+set(ipasir_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_ipasir.cpp
+)
+
 
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
@@ -51,6 +55,7 @@ list(REMOVE_ITEM sources
     ${lingeling_source}
     ${booleforce_source}
     ${minibdd_source}
+    # ${ipasir_source}
 )
 
 add_library(solvers ${sources})
@@ -128,6 +133,65 @@ elseif("${sat_impl}" STREQUAL "cadical")
     )
 
     target_link_libraries(solvers cadical)
+elseif("${sat_impl}" STREQUAL "ipasir-cadical")
+    message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
+
+    download_project(PROJ cadical
+        URL https://github.com/arminbiere/cadical/archive/rel-1.4.0.tar.gz
+        PATCH_COMMAND true
+        COMMAND ./configure CXX=g++
+        URL_MD5 9bad586a82995a1d95d1197d445a353a
+    )
+
+    message(STATUS "Building CaDiCaL")
+    execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+
+    target_compile_definitions(solvers PUBLIC
+        SATCHECK_IPASIR HAVE_IPASIR IPASIR=${cadical_SOURCE_DIR}/src
+    )
+
+    add_library(cadical_ipasir STATIC IMPORTED)
+    set_property(TARGET cadical_ipasir
+        PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
+    )
+
+    target_include_directories(solvers
+        PUBLIC
+        ${cadical_SOURCE_DIR}/src
+    )
+    target_link_libraries(solvers cadical_ipasir)
+elseif("${sat_impl}" STREQUAL "ipasir-custom")
+    message(STATUS "Building with IPASIR solver linking: custom solver provided")
+
+    if (NOT DEFINED IPASIR)
+        message(FATAL_ERROR
+          "IPASIR solver source code not provided. Please use -DIPASIR=<location> "
+          "with <location> being the path to the IPASIR solver source code."
+        )
+    endif()
+
+    if (NOT DEFINED IPASIR_LIB)
+        message(FATAL_ERROR
+            "IPASIR solver library not provided. Please use -DIPASIR_LIB=<location> "
+            "with <location> being the path to the IPASIR solver precompiled static "
+            "library."
+        )
+    endif()
+
+    target_compile_definitions(solvers PUBLIC
+        SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR}
+    )
+
+    add_library(ipasir_custom STATIC IMPORTED)
+    set_property(TARGET ipasir_custom
+        PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
+    )
+
+    target_include_directories(solvers
+        PUBLIC
+        ${IPASIR}
+    )
+    target_link_libraries(solvers ipasir_custom pthread)
 endif()
 
 if(CMAKE_USE_CUDD)