Cleanup Cryptominisat SAT wrapper. (#1652)

Cryptominisat has name conflicts 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.

Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.

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