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

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);