Bugfix/ipasir

.travis.yml

@@ -39,10 +39,11 @@ matrix:
             - libwww-perl
             - g++-5
             - libubsan0
+            - unzip
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER=g++-5
+      env: COMPILER=g++-5 STATICLINK=-static
 
     # Ubuntu Linux with glibc using clang++-3.7
     - os: linux
@@ -58,10 +59,11 @@ matrix:
             - clang-3.7
             - libstdc++-5-dev
             - libubsan0
+            - unzip
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
-      env: COMPILER=clang++-3.7
+      env: COMPILER=clang++-3.7 STATICLINK=-static
 
     - env: NAME="CPP-LINT"
       script: scripts/travis_lint.sh || true
@@ -70,9 +72,24 @@ script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
     COMMAND="make -C src minisat2-download" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
-    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
-    eval ${PRE_COMMAND} ${COMMAND}
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src clean" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src glucose-download" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src -j2 GLUCOSE=../../glucose-syrup LINKFLAGS=$STATICLINK" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C regression test" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="touch src/solvers/sat/satcheck.h" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src ipasir-build" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src -j2 IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C regression test"

scripts/glucose-syrup-patch

@@ -125,3 +125,14 @@ diff -rupN glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
 +}
 
  #endif
+--- glucose-syrup/utils/System.h	2017-03-23 12:42:13.168183780 +0100
++++ glucose-syrup-patched/utils/System.h	2017-03-23 12:41:12.244000866 +0100
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
+ #ifndef Glucose_System_h
+ #define Glucose_System_h
+
+-#if defined(__linux__)
++#if defined(__linux__) && defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+

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 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/cbmc/Makefile

@@ -26,7 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER) \
       ../util/util$(LIBEXT) \
       ../miniz/miniz$(OBJEXT) \
       ../json/json$(LIBEXT)

src/cegis/Makefile

@@ -105,7 +105,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER)  \
       ../util/util$(LIBEXT) \
       ../goto-instrument/dump_c$(OBJEXT) ../goto-instrument/goto_program2code$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) ../goto-instrument/cover$(OBJEXT) \

src/clobber/Makefile

@@ -9,7 +9,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../langapi/langapi$(LIBEXT) \
        ../xmllang/xmllang$(LIBEXT) \
        ../assembler/assembler$(LIBEXT) \
-       ../solvers/solvers$(LIBEXT) \
+       ../solvers/solvers$(LIBEXT) $(LIBSOLVER)  \
        ../util/util$(LIBEXT) \
        ../goto-symex/adjust_float_expressions$(OBJEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \

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"

src/goto-diff/Makefile

@@ -13,7 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER)\
       ../miniz/miniz$(OBJEXT) \
       ../json/json$(LIBEXT)
 

src/goto-instrument/Makefile

@@ -37,7 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER)\
       ../miniz/miniz$(OBJEXT) \
       ../json/json$(LIBEXT)
 

src/musketeer/Makefile

@@ -13,7 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER)  \
       ../goto-instrument/wmm/weak_memory$(OBJEXT) \
       ../goto-instrument/wmm/fence$(OBJEXT) \
       ../goto-instrument/wmm/event_graph$(OBJEXT) \

src/solvers/Makefile

@@ -22,6 +22,14 @@ ifneq ($(MINISAT2),)
   override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
 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
+
 ifneq ($(GLUCOSE),)
   GLUCOSE_SRC=sat/satcheck_glucose.cpp
   GLUCOSE_INCLUDE=-I $(GLUCOSE)
@@ -72,6 +80,7 @@ ifneq ($(LINGELING),)
 endif
 
 SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \
+      $(IPASIR_SRC) \
       $(SMVSAT_SRC) $(SQUOLEM2_SRC) $(CUDD_SRC) $(GLUCOSE_SRC) \
       $(PRECOSAT_SRC) $(PICOSAT_SRC) $(LINGELING_SRC) \
       sat/cnf.cpp sat/dimacs_cnf.cpp sat/cnf_clause_list.cpp \
@@ -122,6 +131,7 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \
 
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
+  $(IPASIR_INCLUDE) \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 

src/solvers/sat/satcheck.h

@@ -9,16 +9,45 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_H
 #define CPROVER_SOLVERS_SAT_SATCHECK_H
 
-// this picks the "default" SAT solver
+// This sets a define for the SAT solver
+// based on set flags that come via the compiler
+// command line.
 
-// #define SATCHECK_ZCHAFF
-// #define SATCHECK_MINISAT1
+#ifdef HAVE_IPASIR
+#define SATCHECK_IPASIR
+#endif
+
+#ifdef HAVE_ZCHAFF
+#define SATCHECK_ZCHAFF
+#endif
+
+#ifdef HAVE_MINISAT1
+#define SATCHECK_MINISAT1
+#endif
+
+#ifdef HAVE_MINISAT2
 #define SATCHECK_MINISAT2
-// #define SATCHECK_GLUCOSE
-// #define SATCHECK_BOOLEFORCE
-// #define SATCHECK_PRECOSAT
-// #define SATCHECK_PICOSAT
-// #define SATCHECK_LINGELING
+#endif
+
+#ifdef HAVE_GLUCOSE
+#define SATCHECK_GLUCOSE
+#endif
+
+#ifdef HAVE_BOOLEFORCE
+#define SATCHECK_BOOLEFORCE
+#endif
+
+#ifdef HAVE_PRECOSAT
+#define SATCHECK_PRECOSAT
+#endif
+
+#ifdef HAVE_PICOSAT
+#define SATCHECK_PICOSAT
+#endif
+
+#ifdef HAVE_LINGELING
+#define SATCHECK_LINGELING
+#endif
 
 #if defined SATCHECK_ZCHAFF
 
@@ -48,6 +77,13 @@ typedef satcheck_minisat1t satcheck_no_simplifiert;
 typedef satcheck_minisat_simplifiert satcheckt;
 typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
 
+#elif defined SATCHECK_IPASIR
+
+#include "satcheck_ipasir.h"
+
+typedef satcheck_ipasirt satcheckt;
+typedef satcheck_ipasirt satcheck_no_simplifiert;
+
 #elif defined SATCHECK_PRECOSAT
 
 #include "satcheck_precosat.h"