Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)

diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4
index 2cd48e87ddcab4b0aca384d86c7348cef0208019..8f2f5bc51de37d4788c5b794245b9d6a3facdfdb 100644 (file)
--- 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 937b223bfe41ca215462ffe63a6ca9d9ce2a46c5..72e354d97baaaa8f1f7b4982104da71b22d7fac6 100644 (file)
--- 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 (file)
index 30b24a3..0000000
--- 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 (file)
index 4b3fdf7..0000000
--- 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-cryptominisat b/contrib/get-cryptominisat
new file mode 100755 (executable)
index 0000000..a7a1552
--- /dev/null
+++ b/contrib/get-cryptominisat
@@ -0,0 +1,36 @@
+#!/bin/bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+
+if [ -e cryptominisat5 ]; then
+  echo 'error: file or directory "cryptominisat5" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+version="5.0.2"
+
+mkdir cryptominisat5
+cd cryptominisat5
+CRYPTOMINISAT_PATH=`pwd`
+
+webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz
+gunzip -f cryptominisat-$version.tar.gz
+tar xfv cryptominisat-$version.tar
+cd cryptominisat-$version
+
+mkdir ../build
+cd ../build
+
+cmake -DENABLE_PYTHON_INTERFACE=OFF \
+      -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install \
+      -DSTATICCOMPILE=ON \
+      -DNOM4RI=ON \
+      ../cryptominisat-$version
+
+make install -j$(nproc)
+
+cd ../
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-cryptominisat

diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
deleted file mode 100755 (executable)
index 0a7173c..0000000
--- a/contrib/get-cryptominisat4
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/bin/bash
-#
-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
-  exit 1
-fi
-
-version="4.2.0"
-
-mkdir cryptominisat4
-cd cryptominisat4
-CRYPTOMINISAT_PATH=`pwd`
-
-webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz
-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
-make install -j$(nproc)
-
-cd ../
-
-echo
-echo ===================== Now configure CVC4 with =====================
-echo ./configure --with-cryptominisat

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 197fece173cd617c0515a4443fb37ca5027e1981..c48a54afb1305abe4ffc8ba63db159e3b8f38044 100644 (file)
--- 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);