Skip to content

Commit dd06dd3

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 693ddca commit dd06dd3

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+
```sh
471+
$ cmake -Bbuild_ipasir -S . -Dsat-impl=ipasir-cadical
470472
```
471-
$ cmake -Bbuild_ipasir -S. -Dsat-impl=ipasir-cadical
473+
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>
472480
```
473481

482+
with `<source_location>` being the path to the folder containing the solver implementation
483+
and `<lib_location>` being the path that contains a precompiled static library of
484+
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)