From 7d8ad07e9f3b13d73ee6366d32fc9505bf54d7b8 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 25 Jan 2017 09:18:32 +0100 Subject: [PATCH 1/8] build: introduce LIBSOLVER environment variable When building solvers.a while aiming at building CBMC with support for IPASIR solvers, all projects that need SAT checkers would require to link against the provided libipasir.a library. To make this library visible for all subprojects at the same time, but furthermore allow the user to choose which library to pick, the variable LIBSOLVER was introduced, which is set to an empty value by default. To compile while using IPASIR solvers, use for example: IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \ CFLAGS="-DSATCHECK_IPSAIR" make -j 7 -C src --- src/cbmc/Makefile | 2 +- src/cegis/Makefile | 2 +- src/clobber/Makefile | 2 +- src/goto-diff/Makefile | 2 +- src/goto-instrument/Makefile | 2 +- src/musketeer/Makefile | 2 +- src/symex/Makefile | 2 +- unit/Makefile | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 8132097565c..e3f6c5a30d6 100644 --- a/src/cbmc/Makefile +++ b/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) diff --git a/src/cegis/Makefile b/src/cegis/Makefile index f1a38ce4915..196663fecd6 100644 --- a/src/cegis/Makefile +++ b/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) \ diff --git a/src/clobber/Makefile b/src/clobber/Makefile index ee77d22e33a..c52806fa19f 100644 --- a/src/clobber/Makefile +++ b/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) \ diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index fd18897aaea..91fc86b9c19 100644 --- a/src/goto-diff/Makefile +++ b/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) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 4cbd6121b24..983274633fa 100644 --- a/src/goto-instrument/Makefile +++ b/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) diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile index d732a396ebd..78221d1707f 100644 --- a/src/musketeer/Makefile +++ b/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) \ diff --git a/src/symex/Makefile b/src/symex/Makefile index e887ca55352..77913710c93 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -10,7 +10,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) \ diff --git a/unit/Makefile b/unit/Makefile index 007ebd3c70d..3767b4615d5 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,7 +20,7 @@ LIBS = ../src/ansi-c/ansi-c$(LIBEXT) \ ../src/langapi/langapi$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ ../src/analyses/analyses$(LIBEXT) \ - ../src/solvers/solvers$(LIBEXT) \ + ../src/solvers/solvers$(LIBEXT) $(LIBSOLVER) \ CLEANFILES = $(SRC:.cpp=$(EXEEXT)) From 3c0d5e875b557b607b65fc5a5b8bfe7b1ae3f40f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 18 Jan 2017 00:32:26 +0100 Subject: [PATCH 2/8] solvers: add ipasir driver Add the necessary source changes to allow CBMC to use IPASIR solvers. --- src/solvers/Makefile | 10 + src/solvers/sat/satcheck.h | 52 ++++- src/solvers/sat/satcheck_ipasir.cpp | 314 ++++++++++++++++++++++++++++ src/solvers/sat/satcheck_ipasir.h | 56 +++++ 4 files changed, 424 insertions(+), 8 deletions(-) create mode 100644 src/solvers/sat/satcheck_ipasir.cpp create mode 100644 src/solvers/sat/satcheck_ipasir.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 95ea7650274..8cb986174f8 100644 --- a/src/solvers/Makefile +++ b/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) diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h index 19fc7759f69..06c25370b62 100644 --- a/src/solvers/sat/satcheck.h +++ b/src/solvers/sat/satcheck.h @@ -9,16 +9,45 @@ Author: Daniel Kroening, kroening@kroening.com #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" diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp new file mode 100644 index 00000000000..d020ceba65e --- /dev/null +++ b/src/solvers/sat/satcheck_ipasir.cpp @@ -0,0 +1,314 @@ +/*******************************************************************\ + +Module: + +Author: Norbert Manthey, nmanthey@amazon.com + +\*******************************************************************/ + +#ifndef _MSC_VER +#include +#endif + +#include +#include + +#include + +#include "satcheck_ipasir.h" + +extern "C" +{ +#include +} + +#ifndef HAVE_IPASIR +#error "Expected HAVE_IPASIR" +#endif + +/* solver interface: + +Representation: +Variables for a formula start with 1! 0 is used as termination symbol. + +Functions: +const char * ipasir_signature (); +void * ipasir_init (); +void ipasir_release (void * solver); +void ipasir_add (void * solver, int lit_or_zero); +void ipasir_assume (void * solver, int lit); +int ipasir_solve (void * solver); +int ipasir_val (void * solver, int lit); +int ipasir_failed (void * solver, int lit); +void ipasir_set_terminate (void * solver, void * state, int (*terminate)(void * state)); + +*/ + +/*******************************************************************\ + +Function: satcheck_ipasirt::l_get + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +tvt satcheck_ipasirt::l_get(literalt a) const +{ + if(a.is_true()) + return tvt(true); + else if(a.is_false()) + return tvt(false); + + tvt result; + + // compare to internal no_variables number + if(a.var_no()>=(unsigned)no_variables()) + return tvt::unknown(); + + const int val=ipasir_val(solver, a.var_no()); + + if(val>0) + result=tvt(true); + else if(val<0) + result=tvt(false); + else + return tvt::unknown(); + + if(a.sign()) + result=!result; + + return result; +} + +/*******************************************************************\ + +Function: satcheck_minisat_no_simplifiert::solver_text + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +const std::string satcheck_ipasirt::solver_text() +{ + return std::string(ipasir_signature()); +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::lcnf + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +void satcheck_ipasirt::lcnf(const bvt &bv) +{ + forall_literals(it, bv) + { + if(it->is_true()) + return; + else if(!it->is_false()) + assert(it->var_no()<(unsigned)no_variables()); + } + + + forall_literals(it, bv) + { + if(!it->is_false()) + { + // add literal wit correct sign + ipasir_add(solver, it->sign()?-it->var_no():it->var_no()); + } + } + ipasir_add(solver, 0); // terminate clause + + clause_counter++; +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::prop_solve + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +propt::resultt satcheck_ipasirt::prop_solve() +{ + assert(status!=ERROR); + + { + messaget::status() << + (no_variables()-1) << " variables, " << + clause_counter << " clauses" << eom; + } + + // use the internal representation, as ipasir does not support reporting the + // status + if(status==UNSAT) + { + messaget::status() << + "SAT checker inconsistent: instance is UNSATISFIABLE" << eom; + } + else + { + // if assumptions contains false, we need this to be UNSAT + bool has_false=false; + + forall_literals(it, assumptions) + if(it->is_false()) + has_false=true; + + if(has_false) + { + messaget::status() << + "got FALSE as assumption: instance is UNSATISFIABLE" << eom; + } + else + { + forall_literals(it, assumptions) + if(!it->is_false()) + ipasir_assume(solver, it->sign()?-it->var_no():it->var_no()); + + if(10==ipasir_solve(solver)) + { + messaget::status() << + "SAT checker: instance is SATISFIABLE" << eom; + status=SAT; + return P_SATISFIABLE; + } + else + { + messaget::status() << + "SAT checker: instance is UNSATISFIABLE" << eom; + } + } + } + + status=UNSAT; + return P_UNSATISFIABLE; +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::set_assignment + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +void satcheck_ipasirt::set_assignment(literalt a, bool value) +{ + assert(!a.is_constant()); + assert(false && "method not supported"); +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::satcheck_ipasirt + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +satcheck_ipasirt::satcheck_ipasirt() +: solver(0) +{ + assert(!solver); + solver=ipasir_init(); +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::~satcheck_ipasirt + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +satcheck_ipasirt::~satcheck_ipasirt() +{ + if(solver) + ipasir_release(solver); + solver=0; +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::is_in_conflict + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +bool satcheck_ipasirt::is_in_conflict(literalt a) const +{ + int v=a.var_no(); + + if(ipasir_failed(solver, v)) + return true; + return false; +} + +/*******************************************************************\ + +Function: satcheck_ipasirt::set_assumptions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + +void satcheck_ipasirt::set_assumptions(const bvt &bv) +{ + forall_literals(it, bv) + if(it->is_true()) + { + assumptions.clear(); + return; + } + // only copy assertions, if there is no false in bt parameter + assumptions=bv; +} diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h new file mode 100644 index 00000000000..68d9aeafd91 --- /dev/null +++ b/src/solvers/sat/satcheck_ipasir.h @@ -0,0 +1,56 @@ +/*******************************************************************\ + +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 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. + +\*******************************************************************/ + +#ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H +#define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H + +#include "cnf.h" + +// Interface for generic SAT solver interface IPASIR +class satcheck_ipasirt:public cnf_solvert +{ +public: + satcheck_ipasirt(); + virtual ~satcheck_ipasirt(); + + virtual const std::string solver_text(); + + virtual resultt prop_solve() override; + virtual tvt l_get(literalt a) const override final; + + virtual void lcnf(const bvt &bv) override final; + + /* this method is not supported, and currently not called anywhere in CBMC */ + virtual void set_assignment(literalt a, bool value) override; + + virtual void set_assumptions(const bvt &_assumptions) override; + + virtual bool is_in_conflict(literalt a) const override; + virtual bool has_set_assumptions() const override final { return true; } + virtual bool has_is_in_conflict() const override final { return true; } + +protected: + void *solver; + + bvt assumptions; +}; + +#endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H From b4b41078c1dccc7ea2166291e0125ed3605bc3bc Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 18 Jan 2017 00:32:04 +0100 Subject: [PATCH 3/8] 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 --- src/Makefile | 39 ++++++++++++++++++++++++++++++++- src/common | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/config.inc | 6 +++++- 3 files changed, 101 insertions(+), 2 deletions(-) diff --git a/src/Makefile b/src/Makefile index 704a6754a45..9579265ffb9 100644 --- a/src/Makefile +++ b/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 diff --git a/src/common b/src/common index 20c4fadbb44..e4b8da5f45d 100644 --- a/src/common +++ b/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 diff --git a/src/config.inc b/src/config.inc index e1c1266f683..16d50045549 100644 --- a/src/config.inc +++ b/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" From 4a312445f6d627c680d30bfdbe70022458666be2 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Thu, 26 Jan 2017 00:24:27 +0100 Subject: [PATCH 4/8] build: test multiple SAT solvers during CI Besides the usual test with Minisat, also compile with glucose, and test whether compilation with IPASIR works. Perform tests and regression testing for the two variants as well. Furthermore, if libzip and zlib and not inizialized properly, any build will fail. Hence, these targets are added as well. --- .travis.yml | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index d74ec93f7e3..4260198a668 100644 --- a/.travis.yml +++ b/.travis.yml @@ -42,7 +42,7 @@ matrix: 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 @@ -61,10 +61,12 @@ matrix: 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 + - env: NAME="LIB-ZIP" + script: cd src; make zlib-download && make libzip-download && make libzip-build script: - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ; @@ -75,4 +77,19 @@ script: 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 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" \ No newline at end of file From fe08ac7df24e5550e328fc100004ab4d58f92e9e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 12:43:13 +0100 Subject: [PATCH 5/8] include `fpu_control.h` in glucose-syrup only when using glibc --- scripts/glucose-syrup-patch | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/scripts/glucose-syrup-patch b/scripts/glucose-syrup-patch index 138e4a50315..bc64e88f890 100644 --- a/scripts/glucose-syrup-patch +++ b/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 + #endif + From 238b6d6e9a2fd43e583f333b8e663880e8c11c45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 15:51:40 +0100 Subject: [PATCH 6/8] update dir in ipasir-build --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4260198a668..7f8c390daf7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -88,8 +88,8 @@ script: eval ${PRE_COMMAND} ${COMMAND} && COMMAND="touch src/solvers/sat/satcheck.h" && eval ${PRE_COMMAND} ${COMMAND} && - COMMAND="make ipasir-build" && + 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" \ No newline at end of file + COMMAND="make -C regression test" From 5cfc5bbc6aedbd5d65dcb132d74e3ea9b7887192 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 16:44:55 +0100 Subject: [PATCH 7/8] add unzip as required package --- .travis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 7f8c390daf7..19556f07886 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ 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" @@ -58,6 +59,7 @@ 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" @@ -65,14 +67,12 @@ matrix: - env: NAME="CPP-LINT" script: scripts/travis_lint.sh || true - - env: NAME="LIB-ZIP" - script: cd src; make zlib-download && make libzip-download && make libzip-build 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} && From f4358fc655e6b6d793d6bb44631740509b529653 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 23 Mar 2017 18:51:27 +0100 Subject: [PATCH 8/8] remove -u option from unzip command line --- src/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Makefile b/src/Makefile index 9579265ffb9..5cf0986ec64 100644 --- a/src/Makefile +++ b/src/Makefile @@ -112,7 +112,7 @@ 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) + @(cd ..; unzip ipasir.zip) ipasir-build: ipasir-download # build libpicaso, and create a libipasir.a in ipasir directory