build: add ipasir solver support

Add necessary steps to set variables for IPASIR

Furthermore, allow to select SAT solver from make command line,
for example by calling

IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a make

Not, to compile with a different SAT solver, e.g.

GLUCOSE=../../glucose-syrup make

it has to be ensured, that the solvers.a library is rebuild, and all
components that link against this library are renewed as well. This
can be achieved by touching the satcheck.h flie, i.e.:

touch src/solvers/sat/satcheck.h

Author: Norbert Manthey

src/Makefile

@@ -84,4 +84,41 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-.PHONY: minisat2-download glucose-download
+zlib-download:
+	@echo "Downloading zlib 1.2.11"
+	@lwp-download http://zlib.net/zlib-1.2.11.tar.gz
+	@tar xfz zlib-1.2.11.tar.gz
+	@rm -Rf ../zlib
+	@mv zlib-1.2.11 ../zlib
+	@rm zlib-1.2.11.tar.gz
+
+libzip-download:
+	@echo "Downloading libzip 1.1.2"
+	# The below wants SSL
+	#@lwp-download http://www.nih.at/libzip/libzip-1.1.2.tar.gz
+	@lwp-download http://http.debian.net/debian/pool/main/libz/libzip/libzip_1.1.2.orig.tar.gz
+	@tar xfz libzip_1.1.2.orig.tar.gz
+	@rm -Rf ../libzip
+	@mv libzip-1.1.2 ../libzip
+	@rm libzip_1.1.2.orig.tar.gz
+
+libzip-build:
+	@echo "Building zlib"
+	@(cd ../zlib; ./configure; make)
+	@echo "Building libzip"
+	@(cd ../libzip; BASE=`pwd`; ./configure --with-zlib=$(BASE)/zlib ; make)
+
+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 libpicaso, 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 Picaso 961 from ipasir 2016 package"
+	$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
+	@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
+
+.PHONY: ipasir-build minisat2-download glucose-download zlib-download libzip-download libzip-build

src/common

@@ -150,6 +150,64 @@ else
   $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_))
 endif
 
+# select default solver to be minisat2 if no other is specified
+ifndef IPASIR
+ifndef PRECOSAT
+ifndef PICOSAT
+ifndef LINGELING
+ifndef CHAFF
+ifndef BOOLEFORCE
+ifndef MINISAT
+ifndef MINISAT2
+ifndef GLUCOSE
+MINISAT2 = ../../minisat-2.2.1
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+
+ifneq ($(IPASIR),)
+  CP_CXXFLAGS += -DHAVE_IPASIR
+endif
+
+ifneq ($(PRECOSAT),)
+  CP_CXXFLAGS += -DHAVE_PRECOSAT
+endif
+
+ifneq ($(PICOSAT),)
+  CP_CXXFLAGS += -DHAVE_PICOSAT
+endif
+
+ifneq ($(LINGELING),)
+  CP_CXXFLAGS += -DHAVE_LINGELING
+endif
+
+ifneq ($(CHAFF),)
+  CP_CXXFLAGS += -DHAVE_CHAFF
+endif
+
+ifneq ($(BOOLEFORCE),)
+  CP_CXXFLAGS += -DHAVE_BOOLEFORCE
+endif
+
+ifneq ($(MINISAT),)
+  CP_CXXFLAGS += -DHAVE_MINISAT
+endif
+
+ifneq ($(MINISAT2),)
+  CP_CXXFLAGS += -DHAVE_MINISAT2
+endif
+
+ifneq ($(GLUCOSE),)
+  CP_CXXFLAGS += -DHAVE_GLUCOSE
+endif
+
+
 
 first_target: all
 

src/config.inc

@@ -21,10 +21,14 @@ BUILD_ENV = AUTO
 #CHAFF = ../../zChaff
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
-MINISAT2 = ../../minisat-2.2.1
+#MINISAT2 = ../../minisat-2.2.1
+#IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =
 
+LIBZIPLIB = ../../libzip/lib/.libs/libzip.a ../../zlib/libz.a
+LIBZIPINC = ../../libzip/lib
+
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"