From 3f4a89621a9693316c302796a0fe8421cf87ca92 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 19 Sep 2018 08:18:16 +0000
Subject: [PATCH] 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.
---
 COMPILING.md                                  | 17 ++---------
 .../compilation-and-development.md            | 29 +++++++++++++++++++
 src/Makefile                                  | 13 ---------
 src/solvers/sat/satcheck_ipasir.h             | 14 ++-------
 4 files changed, 34 insertions(+), 39 deletions(-)

diff --git a/COMPILING.md b/COMPILING.md
index 6a3448445a..14f2a9ea6f 100644
--- a/COMPILING.md
+++ b/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
diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md
index 714cf05347..508c8edeb8 100644
--- a/doc/architectural/compilation-and-development.md
+++ b/doc/architectural/compilation-and-development.md
@@ -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
diff --git a/src/Makefile b/src/Makefile
index a75535d49b..2fdbcd178b 100644
--- a/src/Makefile
+++ b/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)"
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
index 93c34f27be..58ffb12d08 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -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.
 
 \*******************************************************************/