Skip to content

Commit c15e99c

Browse files
committed
Add custom SAT-solver support through IPASIR to CMAKE.
This is allowing an advanced user to build and link CBMC with arbitrary SAT Solvers using the IPASIR interface.
1 parent 925e6dd commit c15e99c

File tree

1 file changed

+32
-0
lines changed

1 file changed

+32
-0
lines changed

src/solvers/CMakeLists.txt

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,38 @@ elseif("${sat_impl}" STREQUAL "ipasir-cadical")
160160
${cadical_SOURCE_DIR}/src
161161
)
162162
target_link_libraries(solvers cadical_ipasir)
163+
elseif("${sat_impl}" STREQUAL "ipasir-custom")
164+
message(STATUS "Building with IPASIR solver linking: custom solver provided")
165+
166+
if (NOT DEFINED IPASIR)
167+
message(FATAL_ERROR
168+
"IPASIR solver source code not provided. Please use -DIPASIR=<location> "
169+
"with <location> being the path to the IPASIR solver source code."
170+
)
171+
endif()
172+
173+
if (NOT DEFINED IPASIR_LIB)
174+
message(FATAL_ERROR
175+
"IPASIR solver library not provided. Please use -DIPASIR_LIB=<location> "
176+
"with <location> being the path to the IPASIR solver precompiled static "
177+
"library."
178+
)
179+
endif()
180+
181+
target_compile_definitions(solvers PUBLIC
182+
SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR}
183+
)
184+
185+
add_library(ipasir_custom STATIC IMPORTED)
186+
set_property(TARGET ipasir_custom
187+
PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
188+
)
189+
190+
target_include_directories(solvers
191+
PUBLIC
192+
${IPASIR}
193+
)
194+
target_link_libraries(solvers ipasir_custom pthread)
163195
endif()
164196

165197
if(CMAKE_USE_CUDD)

0 commit comments

Comments
 (0)