Cleanup Cryptominisat header. (#1561)

Clang formatted sat_solver_factor.cpp

1 files changed, 19 insertions, 7 deletions

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 27e2daf11..135fc300d 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -16,6 +16,8 @@
 
 #include "prop/sat_solver_factory.h"
 
+// Cryptominisat header has to come first since there are name clashes for
+// var_Undef, l_True, ... (static const in Cryptominisat vs. #define in Minisat)
 #include "prop/cryptominisat.h"
 #include "prop/minisat/minisat.h"
 #include "prop/bvminisat/bvminisat.h"
@@ -23,19 +25,29 @@
 namespace CVC4 {
 namespace prop {
 
-BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) {
+BVSatSolverInterface* SatSolverFactory::createMinisat(
+    context::Context* mainSatContext,
+    StatisticsRegistry* registry,
+    const std::string& name)
+{
   return new BVMinisatSatSolver(registry, mainSatContext, name);
 }
 
 SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
-                                                   const std::string& name) {
-return new CryptoMinisatSolver(registry, name);
+                                                 const std::string& name)
+{
+#ifdef CVC4_USE_CRYPTOMINISAT
+  return new CryptoMinisatSolver(registry, name);
+#else
+  Unreachable("CVC4 was not compiled with Cryptominisat support.");
+#endif
 }
-  
 
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+    StatisticsRegistry* registry)
+{
   return new MinisatSatSolver(registry);
 }
 
-} /* CVC4::prop namespace */
-} /* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC4