From d0f1945d8be791f49c6d885cb15a79569576aa84 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Apr 2021 12:05:22 +0100 Subject: [PATCH 1/4] Add CaDiCaL make instructions This commit adds the first instructions for building cbmc with CaDiCaL 1.4.0 using the IPASIR interface in cbmc. --- COMPILING.md | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/COMPILING.md b/COMPILING.md index 66e130ca32c..a68eec0a65d 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -380,6 +380,47 @@ 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 CaDiCaL + +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. + +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. + +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 The [Riss](https://github.com/conp-solutions/riss) solver supports the From fc7e5b5e06811825c3de28d2c1691dc1f92ac2ff Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Thu, 22 Apr 2021 16:54:27 +0100 Subject: [PATCH 2/4] Update for MacOS status --- COMPILING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/COMPILING.md b/COMPILING.md index a68eec0a65d..a60c029a3ad 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -389,7 +389,7 @@ 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. 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. +1.4.0 on Ubuntu 18.04 & 20.04 and MacOS. 1. Download CaDiCaL: ``` From a89fc93bcea4d85636bc40fbffa1ff8c90083cf1 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 27 Apr 2021 09:36:58 +0100 Subject: [PATCH 3/4] Add documentation on alternative SAT solvers 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. --- COMPILING.md | 41 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 39 insertions(+), 2 deletions(-) diff --git a/COMPILING.md b/COMPILING.md index a60c029a3ad..1b7d9e4d5fd 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -380,7 +380,44 @@ 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 CaDiCaL +### Compiling with CBMC Wrapper + +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 The [CaDiCaL](https://github.com/arminbiere/cadical) solver supports the [IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT @@ -421,7 +458,7 @@ Note that at the time of writing this has been tested to work with the CaDiCaL 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 +#### Compiling with Riss The [Riss](https://github.com/conp-solutions/riss) solver supports the [IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT From a22fb030cf88f4466fa7ac0f947de7ad38d2bc35 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Wed, 28 Apr 2021 09:22:45 +0100 Subject: [PATCH 4/4] Improve documentation clarity Improves clarity of the documentation for building CBMC with alternative SAT solvers. --- COMPILING.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/COMPILING.md b/COMPILING.md index 1b7d9e4d5fd..50d444c3c63 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -380,7 +380,7 @@ 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 CBMC Wrapper +### 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. @@ -417,7 +417,11 @@ Where `SATOBJ` is the pre-compiled IPASIR compatible SAT binary, The rest of this section provides detailed instructions for some example SAT solvers. -#### Compiling with CaDiCaL +#### 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 @@ -458,7 +462,7 @@ Note that at the time of writing this has been tested to work with the CaDiCaL 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 +#### 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