Skip to content

Build cbmc with cadical using make and IPASIR #6047

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 28, 2021
Merged

Build cbmc with cadical using make and IPASIR #6047

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d0f1945
Add CaDiCaL make instructions
TGWDB Apr 20, 2021
fc7e5b5
Update for MacOS status
TGWDB Apr 22, 2021
a89fc93
Add documentation on alternative SAT solvers
TGWDB Apr 27, 2021
a22fb03
Improve documentation clarity
TGWDB Apr 28, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 83 additions & 1 deletion COMPILING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,7 +380,89 @@ For the packaged builds of CBMC on our release page we currently build CBMC
with the MiniSat2 SAT solver statically linked at compile time. However it is
also possible to build CBMC using alternative SAT solvers.

### Compiling with Riss
### Compiling CBMC Using Solver Native Interfaces

The following solvers are supported by CBMC using custom interfaces and can
by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.

For `make` alternatives to the default (i.e. not MiniSAT) can be built with the
following commands for CaDiCaL:
```
make -C src cadical-download
make -C src CADICAL=../../cadical
```
and for glucose
```
make -C src glucose-download
make -C src GLUCOSE=../../glucose-syrup
```

For `cmake` the alternatives can be built with the following arguments to `cmake`
for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`.


### Compiling with IPASIR Interface

The below compiling instructions allow linking of an arbitrary IPASIR
compatible SAT solver when compiling CBMC.

The general command using `make` is to compile with
```
make -C src LIBS="$PWD/SATOBJ SATLINKFLAGS" IPASIR=$PWD/SATPATH
```
Where `SATOBJ` is the pre-compiled IPASIR compatible SAT binary,
`SATLINKFLAGS` are any flags required by the SAT object file, and
`SATPATH` is the path to the SAT interface.

The rest of this section provides detailed instructions for some example
SAT solvers.

#### Compiling with CaDiCaL via IPASIR

Note that CaDiCaL can also be built using CBMC's CaDiCaL native interface
as described above. This section is to use CaDiCaL with the IPASIR
interface in CBMC.

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.
Comment on lines +426 to +430
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. This was to document how to do it with the IPASIR interface.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pushed a change now that I believe clarifies how to build and link different SAT solvers and makes clear the differences.


Note that at the time of writing this has been tested to work with the CaDiCaL
1.4.0 on Ubuntu 18.04 & 20.04 and MacOS.

1. Download CaDiCaL:
```
git clone --branch rel-1.4.0 https://github.com/arminbiere/cadical.git
```
This will clone the CaDiCaL repository into a `cadical` subdirectory and
checkout release 1.4.0, which has been checked for compatibility with CBMC at
the time these instructions were written.

2. Build CaDiCaL:
```
cd cadical
./configure
make cadical
cd ..
```
This will create a build directory called `build` inside the clone of the
CaDiCaL repository. The `cadical` make target is specified in this example in
order to avoid building targets which are not required by CBMC. The built
static library will be placed in `cadical/build/libcadical.a`.

3. Build CBMC:
```
make -C src LIBS="$PWD/cadical/build/libcadical.a" IPASIR=$PWD/cadical/src
```
This links the CaDiCaL library as part of the build. Passing the IPASIR
parameter tells the build system to build for the IPASIR interface. The
argument for the IPASIR parameter gives the build system the location for
the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
compiled binary will be placed in `cbmc/src/cbmc/cbmc`.

#### Compiling with Riss via IPASIR

The [Riss](https://github.com/conp-solutions/riss) solver supports the
[IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT
Expand Down