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.

4 files changed, 72 insertions, 87 deletions

diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
index 5c7cdd958..0a7173cce 100755
--- a/contrib/get-cryptominisat4
+++ b/contrib/get-cryptominisat4
@@ -31,4 +31,4 @@ cd ../
 
 echo
 echo ===================== Now configure CVC4 with =====================
-echo ./configure --with-cryptominisat --with-cryptominisat-dir=`pwd`
+echo ./configure --with-cryptominisat
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 6627e86bb..197fece17 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -14,15 +14,49 @@
  ** Implementation of the cryptominisat for cvc4 (bitvectors).
  **/
 
+#ifdef CVC4_USE_CRYPTOMINISAT
+
 #include "prop/cryptominisat.h"
 
 #include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 
-using namespace CVC4;
-using namespace prop;
+#include <cryptominisat4/cryptominisat.h>
 
-#ifdef CVC4_USE_CRYPTOMINISAT
+namespace CVC4 {
+namespace prop {
+
+// helper functions
+namespace {
+
+CMSat::Lit toInternalLit(SatLiteral lit)
+{
+  if (lit == undefSatLiteral)
+  {
+    return CMSat::lit_Undef;
+  }
+  return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
+}
+
+SatValue toSatLiteralValue(CMSat::lbool res)
+{
+  if (res == CMSat::l_True) return SAT_VALUE_TRUE;
+  if (res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
+  Assert(res == CMSat::l_False);
+  return SAT_VALUE_FALSE;
+}
+
+void toInternalClause(SatClause& clause,
+                      std::vector<CMSat::Lit>& internal_clause)
+{
+  for (unsigned i = 0; i < clause.size(); ++i)
+  {
+    internal_clause.push_back(toInternalLit(clause[i]));
+  }
+  Assert(clause.size() == internal_clause.size());
+}
+
+}  // helper functions
 
 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
                                          const std::string& name)
@@ -147,56 +181,6 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const {
   return -1; 
 }
 
-// converting from internal sat solver representation
-
-SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) {
-  if (var == CMSat::var_Undef) {
-    return undefSatVariable;
-  }
-  return SatVariable(var);
-}
-
-CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) {
-  if (lit == undefSatLiteral) {
-    return CMSat::lit_Undef;
-  }
-  return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
-}
-
-SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) {
-  Assert (lit != CMSat::lit_Error);
-  if (lit == CMSat::lit_Undef) {
-    return undefSatLiteral;
-  }
-
-  return SatLiteral(SatVariable(lit.var()),
-                    lit.sign());
-}
-
-SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) {
-  if(res == CMSat::l_True) return SAT_VALUE_TRUE;
-  if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
-  Assert(res == CMSat::l_False);
-  return SAT_VALUE_FALSE;
-}
-
-void CryptoMinisatSolver::toInternalClause(SatClause& clause,
-                                           std::vector<CMSat::Lit>& internal_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    internal_clause.push_back(toInternalLit(clause[i]));
-  }
-  Assert(clause.size() == internal_clause.size());
-}
-
-void CryptoMinisatSolver::toSatClause(std::vector<CMSat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i]));
-  }
-  Assert(clause.size() == sat_clause.size());
-}
-
-
 // Satistics for CryptoMinisatSolver
 
 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
@@ -225,4 +209,7 @@ CryptoMinisatSolver::Statistics::~Statistics() {
   d_registry->unregisterStat(&d_clausesAdded);
   d_registry->unregisterStat(&d_solveTime);
 }
+
+}  // namespace prop
+}  // namespace CVC4
 #endif
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
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 135fc300d..69fca59e1 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -16,11 +16,9 @@
 
 #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/bvminisat/bvminisat.h"
 #include "prop/cryptominisat.h"
 #include "prop/minisat/minisat.h"
-#include "prop/bvminisat/bvminisat.h"
 
 namespace CVC4 {
 namespace prop {