From: Mathias Preiner Date: Fri, 9 Mar 2018 02:42:03 +0000 (-0800) Subject: Cleanup Cryptominisat SAT wrapper. (#1652) X-Git-Tag: cvc5-1.0.0~5243 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c64f2388a5dca50ecbd0610f9dcb13324345b94;p=cvc5.git 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 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 -#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& 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& 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& 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 +// 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& internal_clause); - static void toSatClause (std::vector& 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 {