Merged cryptominisat from experimental branch.

3 files changed, 37 insertions, 9 deletions

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