Merge pull request #2983 from tautschnig/ipasir-cleanup

Fix instructions and Makefiles for IPASIR-based SAT solvers

Author: tautschnig

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 LIBSOLVER variable could be pointed towards other solvers
-   ```
-   make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
-   ```
-
-5. To compile JBMC, do
+4. To compile JBMC, do
    ```
    make -C jbmc/src setup-submodules
    make -C jbmc/src

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

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

src/config.inc

@@ -26,10 +26,6 @@ endif
 #GLUCOSE = ../../glucose-syrup
 #CADICAL = ../../cadical
 
-# Extra library for SAT solver. This should link to the archive file to be used
-# when linking against an IPASIR solver.
-LIBSOLVER =
-
 # select default solver to be minisat2 if no other is specified
 ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)
   MINISAT2 = ../../minisat-2.2.1

src/solvers/Makefile

@@ -25,7 +25,6 @@ endif
 ifneq ($(IPASIR),)
   IPASIR_SRC=sat/satcheck_ipasir.cpp
   IPASIR_INCLUDE=-I $(IPASIR)
-  IPASIR_LIB=$(IPASIR)/ipasir.a
   CP_CXXFLAGS += -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
   override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
 endif
@@ -224,10 +223,10 @@ endif
 ###############################################################################
 
 solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
-	$(LINKLIB) $(LIBSOLVER)
+	$(LINKLIB)
 
 -include $(smt2/smt2_solver$(DEPEXT))
 
 smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
 	../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
-	$(LINKBIN) $(LIBSOLVER)
+	$(LINKBIN)

src/solvers/sat/satcheck_ipasir.h

@@ -4,18 +4,8 @@
 
 Author: Norbert Manthey, [email protected]
 
-Sample compilation command:
-(to be executed from base directory of project)
-
-make clean
-make ipasir-build
-CXXFLAGS=-g IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
-  CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \
-  make -j 7 -C $(pwd)/src/;
-
-Note: Make sure, the LIBSOLVER 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.
 
 \*******************************************************************/