diff --git a/.travis.yml b/.travis.yml index d74ec93f7e3..19556f07886 100644 --- a/.travis.yml +++ b/.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" 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 + diff --git a/src/Makefile b/src/Makefile index 704a6754a45..5cf0986ec64 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 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/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/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" 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/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 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))