Document the IPASIR build in a single place
As witnessed by the prior commit, errors in the instructions had to be updated in multiple places. Also removing the Makefile-based build rules for IPASIR as those would only work for outdated solvers.
This commit is contained in:
parent
98febc9225
commit
3f4a89621a
17
COMPILING.md
17
COMPILING.md
|
@ -55,21 +55,10 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
|
|||
make -C src minisat2-download
|
||||
make -C src
|
||||
```
|
||||
See doc/architectural/compilation-and-development.md for instructions on how
|
||||
to use a SAT solver other than MiniSat 2.
|
||||
|
||||
4. Linking against an IPASIR SAT solver
|
||||
|
||||
Get an IPASIR package and build picosat by default
|
||||
```
|
||||
make -C src ipasir-build
|
||||
```
|
||||
|
||||
Build CBMC with IPASIR and link against the ipasir solver library
|
||||
Note: the LIBS variable could be pointed towards other solvers
|
||||
```
|
||||
make -C src IPASIR=../../ipasir LIBS=$(pwd)/ipasir/libipasir.a
|
||||
```
|
||||
|
||||
5. To compile JBMC, do
|
||||
4. To compile JBMC, do
|
||||
```
|
||||
make -C jbmc/src setup-submodules
|
||||
make -C jbmc/src
|
||||
|
|
|
@ -143,6 +143,35 @@ For more information on the structure of `unit/` and how to tag tests, see
|
|||
repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)
|
||||
|
||||
|
||||
\subsection compilation-and-development-subsection-sat-solver Using a different SAT solver
|
||||
|
||||
By default, CBMC will assume MiniSat 2 as the SAT back-end. Several other
|
||||
solvers are supported (see also
|
||||
[config.inc](compilation-and-development-subsubsection-config-inc) above). As a
|
||||
more general option, which is not limited to a single SAT solver, you may use
|
||||
the IPASIR interface. For example, to use the SAT solver RISS, proceed as
|
||||
follows:
|
||||
|
||||
1) Build RISS (in particular its IPASIR configuration):
|
||||
|
||||
git clone https://github.com/conp-solutions/riss riss.git
|
||||
cd riss.git
|
||||
mkdir build
|
||||
cd build
|
||||
cmake ..
|
||||
make riss-coprocessor-lib-static
|
||||
cd ../..
|
||||
|
||||
2) Build CBMC while enabling the IPASIR back-end:
|
||||
make -C src IPASIR=../../riss.git/riss \
|
||||
LIBS="../../riss.git/build/lib/libriss-coprocessor.a -lpthread"
|
||||
|
||||
3) Run CBMC - note that RISS is highly configurable via the RISSCONFIG
|
||||
environment variable:
|
||||
export RISSCONFIG=VERBOSE:BMC1
|
||||
... run CBMC ...
|
||||
|
||||
|
||||
\section compilation-and-development-section-documentation Documentation
|
||||
|
||||
Apart from the (user-orientated) CBMC user manual and this document, most
|
||||
|
|
13
src/Makefile
13
src/Makefile
|
@ -105,19 +105,6 @@ glucose-download:
|
|||
@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
|
||||
@rm glucose-syrup.tgz
|
||||
|
||||
ipasir-download:
|
||||
# get the 2016 version of the ipasir package, which contains a few solvers
|
||||
@echo "Download ipasir 2016 package"
|
||||
@(lwp-download http://baldur.iti.kit.edu/sat-competition-2016/downloads/ipasir.zip ../ipasir.zip)
|
||||
@(cd ..; unzip -u ipasir.zip)
|
||||
|
||||
ipasir-build: ipasir-download
|
||||
# build libpicosat, and create a libipasir.a in ipasir directory
|
||||
# make sure that the ipasir.h file is located there as well (ships with 2016 package)
|
||||
@echo "Build Picosat 961 from ipasir 2016 package"
|
||||
$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
|
||||
@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
|
||||
|
||||
cadical_release = rel-06w
|
||||
cadical-download:
|
||||
@echo "Downloading CaDiCaL $(cadical_release)"
|
||||
|
|
|
@ -4,18 +4,8 @@ Module:
|
|||
|
||||
Author: Norbert Manthey, nmanthey@amazon.com
|
||||
|
||||
Sample compilation command:
|
||||
(to be executed from base directory of project)
|
||||
|
||||
make clean
|
||||
make ipasir-build
|
||||
CXXFLAGS=-g IPASIR=../../ipasir LIBS=$(pwd)/ipasir/libipasir.a \
|
||||
CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \
|
||||
make -j 7 -C $(pwd)/src/;
|
||||
|
||||
Note: Make sure that the LIBS variable is set in the environment!
|
||||
The variable should point to the solver you actually want to
|
||||
link against.
|
||||
See \ref compilation-and-development-subsection-sat-solver for build
|
||||
instructions.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
|
|
Loading…
Reference in New Issue