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, 40 insertions, 53 deletions

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