Merged cryptominisat from experimental branch.

23 files changed, 723 insertions, 11 deletions

diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4
new file mode 100644
index 000000000..f7d3a1544
--- /dev/null
+++ b/config/cryptominisat.m4
@@ -0,0 +1,87 @@
+# CVC4_CHECK_FOR_CRYPTOMINISAT
+# ------------------
+# Look for cryptominisat and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_CRYPTOMINISAT], [
+AC_MSG_CHECKING([whether user requested cryptominisat support])
+
+have_libcryptominisat=0
+CRYPTOMINISAT_LIBS=
+CRYPTOMINISAT_LDFLAGS=
+     
+have_libcryptominisat=0
+if test "$with_cryptominisat" = no; then
+  AC_MSG_RESULT([no, cryptominisat disabled by user])
+elif test -n "$with_cryptominisat"; then
+  AC_MSG_RESULT([yes, cryptominisat requested by user])
+  AC_ARG_VAR(CRYPTOMINISAT_HOME, [path to top level of cryptominisat source tree])
+  AC_ARG_WITH(
+    [cryptominisat-dir],
+    AS_HELP_STRING(
+      [--with-cryptominisat-dir=PATH],
+      [path to top level of cryptominisat source tree]
+    ),
+    [CRYPTOMINISAT_HOME="$withval"],
+    [ if test -z "$CRYPTOMINISAT_HOME"; then
+        AC_MSG_FAILURE([must give --with-cryptominisat-dir=PATH or define environment variable CRYPTOMINISAT_HOME!])
+      fi
+    ]
+  )
+
+  if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat" ; then
+    AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built])
+  fi
+
+  CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
+  
+  AC_MSG_CHECKING([how to link cryptominisat])
+
+  dnl TODO FIXME:
+  dnl For some reason the CVC4_TRY_CRYPTOMINISAT is not working correctly
+  CVC4_TRY_CRYPTOMINISAT_WITH([])
+  CVC4_TRY_CRYPTOMINISAT_WITH([-lm4ri])
+
+  if test -z "$CRYPTOMINISAT_LIBS"; then
+    AC_MSG_FAILURE([cannot link against libcryptominisat!])
+  else
+    AC_MSG_RESULT([$CRYPTOMINISAT_LIBS])
+    have_libcryptominisat=1
+  fi
+
+  CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
+  CRYPTOMINISAT_LIBS="-lcryptominisat4 -lm4ri"
+
+else
+  AC_MSG_RESULT([no, user didn't request cryptominisat])
+  with_cryptominisat=no
+fi
+
+])# CVC4_CHECK_FOR_CRYPTOMINISAT
+
+# CVC4_TRY_STATIC_CRYPTOMINISAT_WITH(LIBS)
+# ------------------------------
+# Try AC_CHECK_LIB(cryptominisat) with the given linking libraries
+AC_DEFUN([CVC4_TRY_CRYPTOMINISAT_WITH], [
+if test -z "$CRYPTOMINISAT_LIBS"; then
+  AC_LANG_PUSH([C++])
+
+  cvc4_save_LIBS="$LIBS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  cvc4_save_CPPFLAGS="$CPPFLAGS"
+
+  LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
+  LIBS="-lcryptominisat4 $1"
+
+
+  AC_LINK_IFELSE(
+    [AC_LANG_PROGRAM([#include <cryptominisat4/cryptominisat.h>],
+      [CMSat::SATSolver test()])], [CRYPTOMINISAT_LIBS="-lcryptominisat4 $1"],
+    [CRYPTOMINISAT_LIBS=])
+
+  LDFLAGS="$cvc4_save_LDFLAGS"
+  CPPFLAGS="$cvc4_save_CPPFLAGS"
+  LIBS="$cvc4_save_LIBS"
+
+  AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_CRYPTOMINISAT_WITH
+
diff --git a/configure.ac b/configure.ac
index c3c29db38..2f343368a 100644
--- a/configure.ac
+++ b/configure.ac
@@ -113,7 +113,7 @@ AC_ARG_WITH([build],
 if test -z "${with_build+set}"; then
   with_build=production
 fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}" -a -z "${with_cryptominisat+set}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -217,6 +217,12 @@ if test -n "${with_abc+set}"; then
     btargs="$btargs abc"
   fi
 fi
+if test -n "${with_cryptominisat+set}"; then
+  if test "$with_cryptominisat" = yes; then
+    btargs="$btargs cryptominisat"
+  fi
+fi
+
 AC_MSG_RESULT([$with_build])
 
 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
@@ -775,6 +781,21 @@ AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
 AC_SUBST([ABC_LDFLAGS])
 AC_SUBST([ABC_LIBS])
 
+
+# Build with libcryptominisat
+AC_ARG_WITH([cryptominisat],
+  [AS_HELP_STRING([--with-cryptominisat],
+     [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
+CVC4_CHECK_FOR_CRYPTOMINISAT
+if test $have_libcryptominisat -eq 1; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include"
+fi
+AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
+AC_SUBST([CRYPTOMINISAT_LDFLAGS])
+AC_SUBST([CRYPTOMINISAT_LIBS])
+
+
 # Check to see if this version/architecture of GNU C++ explicitly
 # instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
 # See src/util/hash.h.
diff --git a/contrib/cryptominisat-4.2.0.patch b/contrib/cryptominisat-4.2.0.patch
new file mode 100644
index 000000000..30b24a3cc
--- /dev/null
+++ b/contrib/cryptominisat-4.2.0.patch
@@ -0,0 +1,12 @@
+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/get-cryptominisat4 b/contrib/get-cryptominisat4
new file mode 100755
index 000000000..a1a8cb786
--- /dev/null
+++ b/contrib/get-cryptominisat4
@@ -0,0 +1,57 @@
+#!/bin/bash
+#
+set -e
+
+version="4.2.0"
+
+cd "$(dirname "$0")/.."
+
+if ! [ -e src/parser/cvc/Cvc.g ]; then
+  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
+  echo "but apparently:" >&2
+  echo >&2
+  echo "  $(pwd)" >&2
+  echo >&2
+  echo "is not a CVC4 source tree ?!" >&2
+  exit 1
+fi
+
+function webget {
+  if which wget &>/dev/null; then
+    wget -c -O "$2" "$1"
+  elif which curl &>/dev/null; then
+    curl "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
+if [ -e cryptominisat4 ]; then
+  echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+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" ../cryptominisat-$version
+make install -j2
+
+cd ../
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-cryptominisat --with-cryptominisat-dir=`pwd`
diff --git a/src/Makefile.am b/src/Makefile.am
index 908245e63..a3580989c 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -109,6 +109,8 @@ libcvc4_la_SOURCES = \
 	prop/sat_solver_factory.cpp \
 	prop/sat_solver_factory.h \
 	prop/sat_solver_types.h \
+	prop/cryptominisat.h \
+	prop/cryptominisat.cpp \
 	prop/theory_proxy.cpp \
 	prop/theory_proxy.h \
 	smt/boolean_terms.cpp \
@@ -474,6 +476,12 @@ libcvc4_la_LIBADD += $(ABC_LIBS)
 libcvc4_la_LDFLAGS += $(ABC_LDFLAGS)
 endif
 
+if CVC4_USE_CRYPTOMINISAT
+libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS)
+libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS)
+endif
+
+
 BUILT_SOURCES = \
 	theory/rewriter_tables.h \
 	theory/theory_traits.h \
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index ce8967a18..db19469fd 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -134,6 +134,10 @@ bool Configuration::isBuiltWithAbc() {
   return IS_ABC_BUILD;
 }
 
+bool Configuration::isBuiltWithCryptominisat() {
+  return IS_CRYPTOMINISAT_BUILD;
+}
+
 bool Configuration::isBuiltWithReadline() {
   return IS_READLINE_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 498337c4c..5d499174f 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -93,6 +93,8 @@ public:
 
   static bool isBuiltWithAbc();
 
+  static bool isBuiltWithCryptominisat();
+
   static bool isBuiltWithReadline();
 
   static bool isBuiltWithCudd();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 74ce00bdf..f0ef1a795 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -114,6 +114,12 @@ namespace CVC4 {
 #  define IS_ABC_BUILD false
 #endif /* CVC4_USE_ABC */
 
+#if CVC4_USE_CRYPTOMINISAT
+#  define IS_CRYPTOMINISAT_BUILD true
+#else /* CVC4_USE_CRYPTOMINISAT */
+#  define IS_CRYPTOMINISAT_BUILD false
+#endif /* CVC4_USE_CRYPTOMINISAT */
+
 #ifdef HAVE_LIBREADLINE
 #  define IS_READLINE_BUILD true
 #else /* HAVE_LIBREADLINE */
diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 9cf47fe33..f331345f7 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -53,4 +53,19 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) {
+  switch(solver) {
+  case theory::bv::SAT_SOLVER_MINISAT:
+    out << "SAT_SOLVER_MINISAT"; 
+    break;
+  case theory::bv::SAT_SOLVER_CRYPTOMINISAT:
+    out << "SAT_SOLVER_CRYPTOMINISAT"; 
+    break;
+  default:
+    out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 4c8c4f626..3a6474104 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -60,12 +60,19 @@ enum BvSlicerMode {
 
 };/* enum BvSlicerMode */
 
+/** Enumeration of sat solvers that can be used. */
+enum SatSolverMode {
+  SAT_SOLVER_MINISAT,
+  SAT_SOLVER_CRYPTOMINISAT,
+};/* enum SatSolver */
+
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
 std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
+std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
 
 }/* CVC4 namespace */
 
diff --git a/src/options/bv_options b/src/options/bv_options
index 8edc809e3..2e6fa2e7a 100644
--- a/src/options/bv_options
+++ b/src/options/bv_options
@@ -7,6 +7,9 @@ module BV "options/bv_options.h" Bitvector theory
 
 # Option to set the bit-blasting mode (lazy, eager)
 
+expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate satSolverEnabledBuild :handler stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "options/bv_bitblast_mode.h"
+ choose which sat solver to use, see --bv-sat-solver=help
+
 option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h"
  choose bitblasting mode, see --bitblast=help
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 867feef6e..6a5f6cd39 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -821,6 +821,72 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro
 #endif /* CVC4_USE_ABC */
 }
 
+void OptionsHandler::satSolverEnabledBuild(std::string option,
+                                           bool value) throw(OptionException) {
+#ifndef CVC4_USE_CRYPTOMINISAT
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_CRYPTOMINISAT */
+}
+
+void OptionsHandler::satSolverEnabledBuild(std::string option,
+                                           std::string value) throw(OptionException) {
+#ifndef CVC4_USE_CRYPTOMINISAT
+  if(!value.empty()) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_CRYPTOMINISAT */
+}
+
+const std::string OptionsHandler::s_bvSatSolverHelp = "\
+Sat solvers currently supported by the --bv-sat-solver option:\n\
+\n\
+minisat (default)\n\
+\n\
+cryptominisat\n\
+";
+
+theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
+                                                            std::string optarg) throw(OptionException) {
+  if(optarg == "minisat") {
+    return theory::bv::SAT_SOLVER_MINISAT;
+  } else if(optarg == "cryptominisat") {
+    
+    if (options::incrementalSolving() &&
+        options::incrementalSolving.wasSetByUser()) {
+      throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\
+                                         Try --bv-sat-solver=minisat"));
+    }
+
+    if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
+        options::bitblastMode.wasSetByUser()) {
+      throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\
+                                         Try --bv-sat-solver=minisat"));
+    }
+    if (!options::bitvectorToBool.wasSetByUser()) {
+      options::bitvectorToBool.set(true);
+    }
+
+    // if (!options::bvAbstraction.wasSetByUser() &&
+    //     !options::skolemizeArguments.wasSetByUser()) {
+    //   options::bvAbstraction.set(true);
+    //   options::skolemizeArguments.set(true); 
+    // }
+    return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
+  } else if(optarg == "help") {
+    puts(s_bvSatSolverHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
+                          optarg + "'.  Try --bv-sat-solver=help.");
+  }
+}
+
 const std::string OptionsHandler::s_bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 8f23219eb..5db2887c0 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -107,10 +107,15 @@ public:
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value) throw(OptionException);
   void abcEnabledBuild(std::string option, std::string value) throw(OptionException);
+  void satSolverEnabledBuild(std::string option, bool value) throw(OptionException);
+  void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException);
+
   theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException);
   theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException);
   void setBitblastAig(std::string option, bool arg) throw(OptionException);
 
+  theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException);
+    
 
   // theory/booleans/options_handlers.h
   theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
@@ -193,6 +198,7 @@ public:
 
   /* Help strings */
   static const std::string s_bitblastingModeHelp;
+  static const std::string s_bvSatSolverHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
   static const std::string s_cegqiFairModeHelp;
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 20724efd2..56a7c61e2 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -78,6 +78,10 @@ public:
 
   ClauseId addClause(SatClause& clause, bool removable);
 
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable("Minisat does not support native XOR reasoning");
+  }
+  
   SatValue propagate();
 
   SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
new file mode 100644
index 000000000..d8f25a786
--- /dev/null
+++ b/src/prop/cryptominisat.cpp
@@ -0,0 +1,230 @@
+/*********************                                                        */
+/*! \file cryptominisat.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the cryptominisat for cvc4 (bitvectors).
+ **/
+
+#include "prop/cryptominisat.h"
+
+#include "proof/clause_id.h"
+#include "proof/sat_proof.h"
+
+using namespace CVC4;
+using namespace prop;
+
+#ifdef CVC4_USE_CRYPTOMINISAT
+
+CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
+                                         const std::string& name)
+: d_solver(new CMSat::SATSolver())
+, d_numVariables(0)
+, d_okay(true)
+, d_statistics(registry, name)
+{
+  d_true = newVar();
+  d_false = newVar();
+
+  std::vector<CMSat::Lit> clause(1);
+  clause[0] = CMSat::Lit(d_true, false);
+  d_solver->add_clause(clause);
+  
+  clause[0] = CMSat::Lit(d_false, true);
+  d_solver->add_clause(clause);
+}
+
+
+CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) {
+  delete d_solver;
+}
+
+ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
+				       bool rhs,
+				       bool removable) {
+  Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
+
+  if (!d_okay) {
+    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
+    return ClauseIdError;
+  }
+
+  ++(d_statistics.d_xorClausesAdded);
+  
+  // ensure all sat literals have positive polarity by pushing
+  // the negation on the result
+  std::vector<CMSat::Var> xor_clause;
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    xor_clause.push_back(toInternalLit(clause[i]).var());
+    rhs ^= clause[i].isNegated();
+  }
+  bool res = d_solver->add_xor_clause(xor_clause, rhs);
+  d_okay &= res;
+  return ClauseIdError;
+}
+
+ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
+  Debug("sat::cryptominisat") << "Add clause " << clause <<"\n";
+
+  if (!d_okay) {
+    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
+    return ClauseIdError;
+  }
+
+  ++(d_statistics.d_clausesAdded);
+  
+  std::vector<CMSat::Lit> internal_clause;
+  toInternalClause(clause, internal_clause);
+  bool res = d_solver->add_clause(internal_clause);
+  d_okay &= res;
+  return ClauseIdError;
+}
+
+bool CryptoMinisatSolver::ok() const {
+  return d_okay; 
+}
+
+
+SatVariable  CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
+  d_solver->new_var();
+  ++d_numVariables;
+  Assert (d_numVariables == d_solver->nVars());
+  return d_numVariables - 1;
+}
+
+SatVariable CryptoMinisatSolver::trueVar() {
+  return d_true;
+}
+
+SatVariable CryptoMinisatSolver::falseVar() {
+  return d_false;
+}
+
+void CryptoMinisatSolver::markUnremovable(SatLiteral lit) {
+  // cryptominisat supports dynamically adding back variables (?)
+  // so this is a no-op
+  return;
+}
+
+void CryptoMinisatSolver::interrupt(){
+  d_solver->interrupt_asap();
+}
+
+SatValue CryptoMinisatSolver::solve(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  ++d_statistics.d_statCallsToSolve;
+  return toSatLiteralValue(d_solver->solve());
+}
+
+SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
+  // CMSat::SalverConf conf = d_solver->getConf();
+  Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); 
+  return solve();
+}
+
+SatValue CryptoMinisatSolver::value(SatLiteral l){
+  const std::vector<CMSat::lbool> model = d_solver->get_model();
+  CMSat::Var var = l.getSatVariable();
+  Assert (var < model.size());
+  CMSat::lbool value = model[var];
+  return toSatLiteralValue(value);
+}
+
+SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
+  return value(l); 
+}
+
+unsigned CryptoMinisatSolver::getAssertionLevel() const {
+  Unreachable("No interface to get assertion level in Cryptominisat");
+  return -1; 
+}
+
+// converting from internal sat solver representation
+
+SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) {
+  if (var == CMSat::var_Undef) {
+    return undefSatVariable;
+  }
+  return SatVariable(var);
+}
+
+CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return CMSat::lit_Undef;
+  }
+  return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
+}
+
+SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) {
+  Assert (lit != CMSat::lit_Error);
+  if (lit == CMSat::lit_Undef) {
+    return undefSatLiteral;
+  }
+
+  return SatLiteral(SatVariable(lit.var()),
+                    lit.sign());
+}
+
+SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) {
+  if(res == CMSat::l_True) return SAT_VALUE_TRUE;
+  if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
+  Assert(res == CMSat::l_False);
+  return SAT_VALUE_FALSE;
+}
+
+void CryptoMinisatSolver::toInternalClause(SatClause& clause,
+                                           std::vector<CMSat::Lit>& internal_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    internal_clause.push_back(toInternalLit(clause[i]));
+  }
+  Assert(clause.size() == internal_clause.size());
+}
+
+void CryptoMinisatSolver::toSatClause(std::vector<CMSat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert(clause.size() == sat_clause.size());
+}
+
+
+// Satistics for CryptoMinisatSolver
+
+CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+                                            const std::string& prefix) :
+  d_registry(registry),
+  d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0),
+  d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0),
+  d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0),
+  d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"),
+  d_registerStats(!prefix.empty())
+{
+  if (!d_registerStats)
+    return;
+
+  d_registry->registerStat(&d_statCallsToSolve);
+  d_registry->registerStat(&d_xorClausesAdded);
+  d_registry->registerStat(&d_clausesAdded);
+  d_registry->registerStat(&d_solveTime);
+}
+
+CryptoMinisatSolver::Statistics::~Statistics() {
+  if (!d_registerStats)
+    return;
+  d_registry->unregisterStat(&d_statCallsToSolve);
+  d_registry->unregisterStat(&d_xorClausesAdded);
+  d_registry->unregisterStat(&d_clausesAdded);
+  d_registry->unregisterStat(&d_solveTime);
+}
+#endif
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
new file mode 100644
index 000000000..29f8b7a2a
--- /dev/null
+++ b/src/prop/cryptominisat.h
@@ -0,0 +1,137 @@
+/*********************                                                        */
+/*! \file cryptominisat.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors).
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "prop/sat_solver.h"
+
+#ifdef CVC4_USE_CRYPTOMINISAT
+#include <cryptominisat4/cryptominisat.h>
+namespace CVC4 {
+namespace prop {
+
+class CryptoMinisatSolver : public SatSolver {
+
+private:
+  CMSat::SATSolver* d_solver;
+  unsigned d_numVariables;
+  bool d_okay;
+  SatVariable d_true;
+  SatVariable d_false;
+public:
+  CryptoMinisatSolver(StatisticsRegistry* registry,
+                      const std::string& name = "");
+  ~CryptoMinisatSolver() throw(AssertionException);
+
+  ClauseId addClause(SatClause& clause, bool removable);
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
+
+  bool nativeXor() { return true; }
+  
+  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
+
+  SatVariable trueVar();
+  SatVariable falseVar();
+
+  void markUnremovable(SatLiteral lit);
+
+  void interrupt();
+  
+  SatValue solve();
+  SatValue solve(long unsigned int&);
+  bool ok() const;
+  SatValue value(SatLiteral l);
+  SatValue modelValue(SatLiteral l);
+
+  unsigned getAssertionLevel() const;
+
+
+  // helper methods for converting from the internal Minisat representation
+
+  static SatVariable toSatVariable(CMSat::Var var);
+  static CMSat::Lit toInternalLit(SatLiteral lit);
+  static SatLiteral toSatLiteral(CMSat::Lit lit);
+  static SatValue toSatLiteralValue(bool res);
+  static SatValue toSatLiteralValue(CMSat::lbool res);
+
+  static void  toInternalClause(SatClause& clause, std::vector<CMSat::Lit>& internal_clause);
+  static void  toSatClause (std::vector<CMSat::Lit>& clause, SatClause& sat_clause);
+
+  class Statistics {
+  public:
+    StatisticsRegistry* d_registry;
+    IntStat d_statCallsToSolve;
+    IntStat d_xorClausesAdded;
+    IntStat d_clausesAdded;
+    TimerStat d_solveTime;
+    bool d_registerStats;
+    Statistics(StatisticsRegistry* registry,
+               const std::string& prefix);
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+};
+} // CVC4::prop
+} // CVC4
+
+#else // CVC4_USE_CRYPTOMINISAT
+
+namespace CVC4 {
+namespace prop {
+
+class CryptoMinisatSolver : public SatSolver {
+
+public:
+  CryptoMinisatSolver(const std::string& name = "") { Unreachable(); }
+  /** Assert a clause in the solver. */
+  ClauseId addClause(SatClause& clause, bool removable) {
+    Unreachable();
+  }
+
+  /** Return true if the solver supports native xor resoning */
+  bool nativeXor() { Unreachable(); }
+
+  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable();
+  }
+  
+  SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); }
+  SatVariable trueVar() { Unreachable(); }
+  SatVariable falseVar() { Unreachable(); }
+  SatValue solve() { Unreachable(); }
+  SatValue solve(long unsigned int&) { Unreachable(); }
+  void interrupt() { Unreachable(); }
+  SatValue value(SatLiteral l) { Unreachable(); }
+  SatValue modelValue(SatLiteral l) { Unreachable(); }
+  unsigned getAssertionLevel() const { Unreachable(); }
+  bool ok() const { return false;};
+  
+
+};/* class CryptoMinisatSolver */
+} // CVC4::prop
+} // CVC4
+
+#endif // CVC4_USE_CRYPTOMINISAT
+
+
+
+
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 535ce1a47..ec5297bb7 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,6 +44,9 @@ public:
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
   ClauseId addClause(SatClause& clause, bool removable);
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable("Minisat does not support native XOR reasoning");
+  }
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 92696ae25..81fb94242 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -49,6 +49,12 @@ public:
   virtual ClauseId addClause(SatClause& clause,
                              bool removable) = 0;
 
+  /** Return true if the solver supports native xor resoning */
+  virtual bool nativeXor() { return false; }
+
+  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
+  virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
+  
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,7 +90,8 @@ public:
 
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
-
+  
+  virtual void setProofLog( BitVectorProof * bvp ) {}
   
 };/* class SatSolver */
 
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 092ec72f2..7fdc44e66 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -16,6 +16,7 @@
 
 #include "prop/sat_solver_factory.h"
 
+#include "prop/cryptominisat.h"
 #include "prop/minisat/minisat.h"
 #include "prop/bvminisat/bvminisat.h"
 
@@ -26,6 +27,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatC
   return new BVMinisatSatSolver(registry, mainSatContext, name);
 }
 
+SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
+                                                   const std::string& name) {
+return new CryptoMinisatSolver(registry, name);
+}
+  
+
 DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
   return new MinisatSatSolver(registry);
 }
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 7cc23a8e8..a04bcaaf4 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -35,6 +35,8 @@ public:
                                              StatisticsRegistry* registry,
                                              const std::string& name = "");
   static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
+  static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
+                                        const std::string& name = "");
 
 };/* class SatSolverFactory */
 
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 887daa1bd..80a9396ac 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -140,10 +140,23 @@ AigBitblaster::AigBitblaster()
   , d_bbAtoms()
   , d_aigOutputNode(NULL)
 {
-  d_nullContext = new context::Context(); 
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster");
-  MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-  d_satSolver->setNotify(notify);
+  d_nullContext = new context::Context();
+  switch(options::bvSatSolver()) {
+  case SAT_SOLVER_MINISAT: {
+    prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
+										"AigBitblaster");
+    MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+    minisat->setNotify(notify);
+    d_satSolver = minisat;
+    break;
+  }
+  case SAT_SOLVER_CRYPTOMINISAT:
+    d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
+                                                              "AigBitblaster");
+    break;
+  default:
+    Unreachable("Unknown SAT solver type");
+  }
 }
 
 AigBitblaster::~AigBitblaster() {
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 5fdc549d0..f9f5361d3 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -257,7 +257,7 @@ public:
 class EagerBitblaster : public TBitblaster<Node> {
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
   // sat solver used for bitblasting and associated CnfStream
-  prop::BVSatSolverInterface*        d_satSolver;
+  prop::SatSolver*                   d_satSolver;
   BitblastingRegistrar*              d_bitblastingRegistrar;
   context::Context*                  d_nullContext;
   prop::CnfStream*                   d_cnfStream;
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index a103d1f63..53fb4f94b 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -47,15 +47,30 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
 {
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
-
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
+  
+  switch(options::bvSatSolver()) {
+  case SAT_SOLVER_MINISAT: {
+    prop::BVSatSolverInterface* minisat =
+      prop::SatSolverFactory::createMinisat(d_nullContext,
+                                            smtStatisticsRegistry(),
+                                            "EagerBitblaster");
+    MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+    minisat->setNotify(notify);
+    d_satSolver = minisat;
+    break;
+  }
+  case SAT_SOLVER_CRYPTOMINISAT:
+    d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
+                                                              "EagerBitblaster");
+    break;
+  default:
+    Unreachable("Unknown SAT solver type");
+  }
 
   d_cnfStream = new prop::TseitinCnfStream(
       d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(),
       "EagerBitblaster");
 
-  d_satSolver->setNotify(&d_notify);
   d_bvp = NULL;
 }