diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-13 15:47:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-13 15:47:34 -0700 |
commit | 36512d36ad34d43277443dcbfabf02baa5ad63b4 (patch) | |
tree | cbb661bab9318f036c032d85c652997701775be0 | |
parent | 10f091e4fc23f80c884520ff484cacb125b45172 (diff) |
Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)
-rw-r--r-- | config/cryptominisat.m4 | 20 | ||||
-rw-r--r-- | contrib/Makefile.am | 4 | ||||
-rw-r--r-- | contrib/cryptominisat-4.2.0.patch | 12 | ||||
-rw-r--r-- | contrib/cryptominisat-4.2.0.second.patch | 11 | ||||
-rwxr-xr-x | contrib/get-cryptominisat (renamed from contrib/get-cryptominisat4) | 20 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 8 |
6 files changed, 27 insertions, 48 deletions
diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4 index 2cd48e87d..8f2f5bc51 100644 --- a/config/cryptominisat.m4 +++ b/config/cryptominisat.m4 @@ -21,22 +21,22 @@ elif test -n "$with_cryptominisat"; then [path to top level of cryptominisat source tree] ), CRYPTOMINISAT_HOME="$withval", - [ if test -z "$CRYPTOMINISAT_HOME" && ! test -e "$ac_abs_confdir/cryptominisat4/install/bin/cryptominisat"; then - AC_MSG_FAILURE([must give --with-cryptominisat-dir=PATH, define environment variable CRYPTOMINISAT_HOME, or use contrib/get-cryptominisat4 to setup Cryptominisat4 for CVC4!]) + [ if test -z "$CRYPTOMINISAT_HOME" && ! test -e "$ac_abs_confdir/cryptominisat5/install/bin/cryptominisat5"; then + AC_MSG_FAILURE([must give --with-cryptominisat-dir=PATH, define environment variable CRYPTOMINISAT_HOME, or use contrib/get-cryptominisat to setup cryptominisat5 for CVC4!]) fi ] ) - # Check if cryptominisat4 was installed via contrib/get-cryptominisat4 - AC_MSG_CHECKING([whether Cryptominisat4 was already installed via contrib/get-cryptominisat4]) - if test -z "$CRYPTOMINISAT_HOME" && test -e "$ac_abs_confdir/cryptominisat4/install/bin/cryptominisat"; then - CRYPTOMINISAT_HOME="$ac_abs_confdir/cryptominisat4" + # Check if cryptominisat5 was installed via contrib/get-cryptominisat + AC_MSG_CHECKING([whether cryptominisat5 was already installed via contrib/get-cryptominisat]) + if test -z "$CRYPTOMINISAT_HOME" && test -e "$ac_abs_confdir/cryptominisat5/install/bin/cryptominisat5"; then + CRYPTOMINISAT_HOME="$ac_abs_confdir/cryptominisat5" AC_MSG_RESULT([yes, $CRYPTOMINISAT_HOME]) else AC_MSG_RESULT([no]) fi - if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat" ; then + if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat5" ; then AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built]) fi @@ -77,11 +77,11 @@ if test -z "$CRYPTOMINISAT_LIBS"; then cvc4_save_CPPFLAGS="$CPPFLAGS" LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" - LIBS="-lcryptominisat4 $1" + LIBS="-lcryptominisat5 $1" AC_LINK_IFELSE( - [AC_LANG_PROGRAM([[#include <cryptominisat4/cryptominisat.h>]], - [[CMSat::SATSolver test()]])], [CRYPTOMINISAT_LIBS="-lcryptominisat4 $1"], + [AC_LANG_PROGRAM([[#include <cryptominisat5/cryptominisat.h>]], + [[CMSat::SATSolver test()]])], [CRYPTOMINISAT_LIBS="-lcryptominisat5 $1"], [CRYPTOMINISAT_LIBS=]) LDFLAGS="$cvc4_save_LDFLAGS" diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 937b223bf..72e354d97 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -9,11 +9,9 @@ EXTRA_DIST = \ addsourcedir \ new-theory \ configure-in-place \ - cryptominisat-4.2.0.patch \ - cryptominisat-4.2.0.second.patch \ depgraph \ get-antlr-3.4 \ - get-cryptominisat4 \ + get-cryptominisat \ get-win-dependencies \ mac-build \ run-script-smtcomp2014 \ diff --git a/contrib/cryptominisat-4.2.0.patch b/contrib/cryptominisat-4.2.0.patch deleted file mode 100644 index 30b24a3cc..000000000 --- a/contrib/cryptominisat-4.2.0.patch +++ /dev/null @@ -1,12 +0,0 @@ -diff -ruN orig/CMakeLists.txt new/CMakeLists.txt ---- CMakeLists.txt 2016-05-24 22:05:50.702570824 -0700 -+++ patched.txt 2016-05-24 22:05:57.778570529 -0700 -@@ -132,7 +132,7 @@ - set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") - SET(Boost_USE_STATIC_LIBS ON) - set(CMAKE_EXE_LINKER_FLAGS "-static -Wl,--whole-archive -lpthread -Wl,--no-whole-archive") -- -+ add_cxx_flag_if_supported("-fPIC") - set(NOMYSQL ON) - else() - add_definitions(-DBOOST_TEST_DYN_LINK) diff --git a/contrib/cryptominisat-4.2.0.second.patch b/contrib/cryptominisat-4.2.0.second.patch deleted file mode 100644 index 4b3fdf722..000000000 --- a/contrib/cryptominisat-4.2.0.second.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- python/CMakeLists.txt 2016-05-24 22:05:50.698570824 -0700 -+++ ../new/python/CMakeLists.txt 2016-05-24 22:05:57.774570529 -0700 -@@ -12,7 +12,7 @@ - - add_custom_target(pytarget ALL DEPENDS ${OUTPUT}/timestamp) - --install(CODE "execute_process(COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --record files.txt)") -+#install(CODE "execute_process(COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --record files.txt)") - - if (ENABLE_TESTING) - #add_test (pytest ${PYTHON_EXECUTABLE} "${CMAKE_CURRENT_SOURCE_DIR}/test_pycryptosat.py") diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat index 0a7173cce..a7a15520c 100755 --- a/contrib/get-cryptominisat4 +++ b/contrib/get-cryptominisat @@ -2,15 +2,15 @@ # source "$(dirname "$0")/get-script-header.sh" -if [ -e cryptominisat4 ]; then - echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2 +if [ -e cryptominisat5 ]; then + echo 'error: file or directory "cryptominisat5" exists; please move it out of the way.' >&2 exit 1 fi -version="4.2.0" +version="5.0.2" -mkdir cryptominisat4 -cd cryptominisat4 +mkdir cryptominisat5 +cd cryptominisat5 CRYPTOMINISAT_PATH=`pwd` webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz @@ -18,13 +18,15 @@ gunzip -f cryptominisat-$version.tar.gz tar xfv cryptominisat-$version.tar cd cryptominisat-$version -patch -p0 < ../../contrib/cryptominisat-4.2.0.patch -patch -p0 < ../../contrib/cryptominisat-4.2.0.second.patch - mkdir ../build cd ../build -cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" -DNOM4RI="ON" ../cryptominisat-$version +cmake -DENABLE_PYTHON_INTERFACE=OFF \ + -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install \ + -DSTATICCOMPILE=ON \ + -DNOM4RI=ON \ + ../cryptominisat-$version + make install -j$(nproc) cd ../ diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 197fece17..c48a54afb 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -21,11 +21,13 @@ #include "proof/clause_id.h" #include "proof/sat_proof.h" -#include <cryptominisat4/cryptominisat.h> +#include <cryptominisat5/cryptominisat.h> namespace CVC4 { namespace prop { +using CMSatVar = unsigned; + // helper functions namespace { @@ -95,7 +97,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, // ensure all sat literals have positive polarity by pushing // the negation on the result - std::vector<CMSat::Var> xor_clause; + std::vector<CMSatVar> xor_clause; for (unsigned i = 0; i < clause.size(); ++i) { xor_clause.push_back(toInternalLit(clause[i]).var()); rhs ^= clause[i].isNegated(); @@ -166,7 +168,7 @@ SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { SatValue CryptoMinisatSolver::value(SatLiteral l){ const std::vector<CMSat::lbool> model = d_solver->get_model(); - CMSat::Var var = l.getSatVariable(); + CMSatVar var = l.getSatVariable(); Assert (var < model.size()); CMSat::lbool value = model[var]; return toSatLiteralValue(value); |