summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/cryptominisat.cpp93
-rw-r--r--src/prop/cryptominisat.h60
-rw-r--r--src/prop/sat_solver_factory.cpp4
3 files changed, 71 insertions, 86 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
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback