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

Note, 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

@@ -93,4 +93,17 @@ cprover-jar-build:
 	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
 	mv org.cprover.jar ../../../)
 
-.PHONY: minisat2-download glucose-download cprover-jar-build
+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)
+
+.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build

src/common

@@ -155,6 +155,48 @@ else
   $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_))
 endif
 
+# select default solver to be minisat2 if no other is specified
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+  MINISAT2 = ../../minisat-2.2.1
+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

@@ -22,7 +22,8 @@ endif
 #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 =