1 files changed, 30 insertions, 30 deletions

diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index fca2c7aa1..32c05974b 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -16,12 +16,22 @@
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__PROP__CRYPTOMINISAT_H
+#define __CVC4__PROP__CRYPTOMINISAT_H
+
+#ifdef CVC4_USE_CRYPTOMINISAT
 
 #include "prop/sat_solver.h"
 
-#ifdef CVC4_USE_CRYPTOMINISAT
-#include <cryptominisat4/cryptominisat.h>
+// Cryptominisat has name clashes with the other Minisat implementations since
+// the Minisat implementations export var_Undef, l_True, ... as macro whereas
+// Cryptominisat uses static const. In order to avoid these conflicts we
+// forward declare CMSat::SATSolver and include the cryptominisat header only
+// in cryptominisat.cpp.
+namespace CMSat {
+  class SATSolver;
+}
+
 namespace CVC4 {
 namespace prop {
 
@@ -36,41 +46,29 @@ private:
 public:
   CryptoMinisatSolver(StatisticsRegistry* registry,
                       const std::string& name = "");
-  virtual ~CryptoMinisatSolver();
+  ~CryptoMinisatSolver() override;
 
-  ClauseId addClause(SatClause& clause, bool removable);
-  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
+  ClauseId addClause(SatClause& clause, bool removable) override;
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
 
-  bool nativeXor() { return true; }
-  
-  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
+  bool nativeXor() override { return true; }
+
+  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true) override;
 
-  SatVariable trueVar();
-  SatVariable falseVar();
+  SatVariable trueVar() override;
+  SatVariable falseVar() override;
 
   void markUnremovable(SatLiteral lit);
 
-  void interrupt();
+  void interrupt() override;
   
-  SatValue solve();
-  SatValue solve(long unsigned int&);
-  bool ok() const;
-  SatValue value(SatLiteral l);
-  SatValue modelValue(SatLiteral l);
+  SatValue solve() override;
+  SatValue solve(long unsigned int&) override;
+  bool ok() const override;
+  SatValue value(SatLiteral l) override;
+  SatValue modelValue(SatLiteral l) override;
 
-  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);
+  unsigned getAssertionLevel() const override;
 
   class Statistics {
   public:
@@ -90,4 +88,6 @@ public:
 
 }  // namespace prop
 }  // namespace CVC4
+
 #endif  // CVC4_USE_CRYPTOMINISAT
+#endif  // __CVC4__PROP__CRYPTOMINISAT_H