Cleanup Cryptominisat header. (#1561)

Clang formatted sat_solver_factor.cpp

diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index bb2f477836081a33c5d69eacf7a7e96943efdc0e..fca2c7aa1a6a3f3953fd456e651b6ba76f42b0a9 100644 (file)
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -87,46 +87,7 @@ public:
 
   Statistics d_statistics;
 };
-} // CVC4::prop
-} // CVC4
 
-#else // CVC4_USE_CRYPTOMINISAT
-
-namespace CVC4 {
-namespace prop {
-
-class CryptoMinisatSolver : public SatSolver {
-
-public:
-  CryptoMinisatSolver(StatisticsRegistry* registry,
-                      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
+}  // namespace prop
+}  // namespace CVC4
+#endif  // CVC4_USE_CRYPTOMINISAT

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 27e2daf1177c40f205b9301971310d62cf00d7f1..135fc300d97cdb83af294be009d1bdb5c89d6e3c 100644 (file)
--- 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