Merged cryptominisat from experimental branch.

5 files changed, 97 insertions, 0 deletions

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;