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.

diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
index 5c7cdd95839ced36df822c7fc5f4270e2ad22a90..0a7173ccef8a7019aad87c98fac6bfaa52d2ad8b 100755 (executable)
--- 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 6627e86bbf948be6d80e2cb5d41059b652c0c03f..197fece173cd617c0515a4443fb37ca5027e1981 100644 (file)
--- 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 fca2c7aa1a6a3f3953fd456e651b6ba76f42b0a9..32c05974b61e780e71d765837fb8c3d149032ad8 100644 (file)
--- 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 135fc300d97cdb83af294be009d1bdb5c89d6e3c..69fca59e1ab530adaa9efcabf9644e81a9f7fad3 100644 (file)
--- 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 {