Build cbmc with cadical using make and IPASIR #6047
Conversation
This commit adds the first instructions for building cbmc with CaDiCaL 1.4.0 using the IPASIR interface in cbmc.
TGWDB
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6047 +/- ##
===========================================
- Coverage 74.30% 73.91% -0.40%
===========================================
Files 1444 1444
Lines 157453 157448 -5
===========================================
- Hits 116995 116373 -622
- Misses 40458 41075 +617
Continue to review full report at Codecov.
|
| The [CaDiCaL](https://github.com/arminbiere/cadical) solver supports the | ||
| [IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT | ||
| solvers, which is also supported by CBMC. So the process for producing a CBMC | ||
| with CaDiCaL build is to build CaDiCaL as a static library then compile CBMC | ||
| with the IPASIR build options and link to the CaDiCaL static library. |
There was a problem hiding this comment.
While that is one way of doing it, it's also possible to use the simpler approach using -Dsat_impl=cadical (with cmake) or make -C src cadical-download followed by make -C src CADICAL=../../cadical.
There was a problem hiding this comment.
Yes. This was to document how to do it with the IPASIR interface.
There was a problem hiding this comment.
I figured as much from the commit message, but could you perhaps also include a few words on those simpler approaches? I don't think the remainder of the section makes clear that this is only needed when choosing the IPASIR approach. (That said, it may be worth pondering long term whether we should stop supporting interfaces other than IPASIR to simplify maintenance.)
There was a problem hiding this comment.
Pushed a change now that I believe clarifies how to build and link different SAT solvers and makes clear the differences.
This adds documentation on alternativer SAT solvers and how to compile them using different builds processed and linking methods. In particular this not documents the make and cmake build processes for CaDiCaL and glucose, as well as general IPASIR linking.
Improves clarity of the documentation for building CBMC with alternative SAT solvers.
This adds documentation for CaDiCaL with IPASIR linking to
cbmc. This is tested for Ubuntu and MacOS.Note that while CaDiCaL can be compiled for Windows (Cygwin), there are problems with building
cbmcthat need to be fixed, and also problems with Cygwin handling of some libraries. For this reason Windows build support is not included in this PR, although this may come later (or viacmake).