Skip to content

Commit 9bc54a2

Browse files
committed
Add instructions on how to link against IPASIR solvers through CMAKE.
Add more instructions on linking against custom IPASIR supporting solvers through CMake.
1 parent c15e99c commit 9bc54a2

File tree

2 files changed

+14
-2
lines changed

2 files changed

+14
-2
lines changed

CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
8181

8282
set(sat_impl "minisat2" CACHE STRING
8383
"This setting controls the SAT library which is used. Valid values are
84-
'minisat2', 'glucose', 'cadical' or 'ipasir-cadical'"
84+
'minisat2', 'glucose', 'cadical', 'ipasir-cadical' or 'ipasir-custom'"
8585
)
8686

8787
if(${enable_cbmc_tests})

COMPILING.md

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -467,10 +467,22 @@ Note that at the time of writing this has been tested to work with the CaDiCaL
467467
It's also possible to build CBMC using CaDiCaL through IPASIR via `cmake`,
468468
controlled with the flag `-Dsat_impl=ipasir-cadical`, like so:
469469
470-
```
470+
```sh
471471
$ cmake -Bbuild_ipasir -S. -Dsat_impl=ipasir-cadical
472472
```
473473

474+
An advanced user may also take a more adventurous route, trying to link
475+
CBMC against any solver supporthing the IPASIR interface. To do that,
476+
an invocation like this is needed:
477+
478+
```sh
479+
$ cmake -Bbuild_ipasir -S . -Dsat_impl=ipasir-custom -DIPASIR=<source_location> -DIPASIR_LIB=<lib_location>
480+
```
481+
482+
with `<source_location>` being the absolute path to the folder containing
483+
the solver implementation and `<lib_location>` being the absolute path that
484+
contains a precompiled static library of the solver (`.a` file).
485+
474486
#### Compiling with Riss via IPASIR
475487

476488
The [Riss](https://github.com/conp-solutions/riss) solver supports the

0 commit comments

Comments
 (0)