diff options
-rwxr-xr-x | contrib/get-cryptominisat4 | 2 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 93 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 60 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 |
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 { |