diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cadical.cpp | 165 | ||||
-rw-r--r-- | src/prop/cadical.h | 90 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 17 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 25 |
6 files changed, 288 insertions, 15 deletions
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp new file mode 100644 index 000000000..3fd210699 --- /dev/null +++ b/src/prop/cadical.cpp @@ -0,0 +1,165 @@ +/********************* */ +/*! \file cadical.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Wrapper for CaDiCaL SAT Solver. + ** + ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors). + **/ + +#include "prop/cadical.h" + +#ifdef CVC4_USE_CADICAL + +#include "proof/sat_proof.h" + +namespace CVC4 { +namespace prop { + +using CadicalLit = int; +using CadicalVar = int; + +// helper functions +namespace { + +SatValue toSatValue(int result) +{ + if (result == 10) return SAT_VALUE_TRUE; + if (result == 20) return SAT_VALUE_FALSE; + Assert(result == 0); + return SAT_VALUE_UNKNOWN; +} + +SatValue toSatValueLit(int value) +{ + if (value == 1) return SAT_VALUE_TRUE; + Assert(value == -1); + return SAT_VALUE_FALSE; +} + +CadicalLit toCadicalLit(const SatLiteral lit) +{ + return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable(); +} + +CadicalVar toCadicalVar(SatVariable var) { return var; } + +} // namespace helper functions + +CadicalSolver::CadicalSolver(StatisticsRegistry* registry, + const std::string& name) + : d_solver(new CaDiCaL::Solver()), + // Note: CaDiCaL variables start with index 1 rather than 0 since negated + // literals are represented as the negation of the index. + d_nextVarIdx(1), + d_statistics(registry, name) +{ + d_true = newVar(); + d_false = newVar(); + + d_solver->set("quiet", 1); // CaDiCaL is verbose by default + d_solver->add(toCadicalVar(d_true)); + d_solver->add(0); + d_solver->add(-toCadicalVar(d_false)); + d_solver->add(0); +} + +CadicalSolver::~CadicalSolver() {} + +ClauseId CadicalSolver::addClause(SatClause& clause, bool removable) +{ + for (const SatLiteral& lit : clause) + { + d_solver->add(toCadicalLit(lit)); + } + d_solver->add(0); + ++d_statistics.d_numClauses; + return ClauseIdError; +} + +ClauseId CadicalSolver::addXorClause(SatClause& clause, + bool rhs, + bool removable) +{ + Unreachable("CaDiCaL does not support adding XOR clauses."); +} + +SatVariable CadicalSolver::newVar(bool isTheoryAtom, + bool preRegister, + bool canErase) +{ + ++d_statistics.d_numVariables; + return d_nextVarIdx++; +} + +SatVariable CadicalSolver::trueVar() { return d_true; } + +SatVariable CadicalSolver::falseVar() { return d_false; } + +SatValue CadicalSolver::solve() +{ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + SatValue res = toSatValue(d_solver->solve()); + d_okay = (res == SAT_VALUE_TRUE); + ++d_statistics.d_numSatCalls; + return res; +} + +SatValue CadicalSolver::solve(long unsigned int&) +{ + Unimplemented("Setting limits for CaDiCaL not supported yet"); +}; + +void CadicalSolver::interrupt() { d_solver->terminate(); } + +SatValue CadicalSolver::value(SatLiteral l) +{ + Assert(d_okay); + return toSatValueLit(d_solver->val(toCadicalLit(l))); +} + +SatValue CadicalSolver::modelValue(SatLiteral l) +{ + Assert(d_okay); + return value(l); +} + +unsigned CadicalSolver::getAssertionLevel() const +{ + Unreachable("CaDiCal does not support assertion levels."); +} + +bool CadicalSolver::ok() const { return d_okay; } + +CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry, + const std::string& prefix) + : d_registry(registry), + d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0), + d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0), + d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0), + d_solveTime("theory::bv::" + prefix + "::cadical::solve_time") +{ + d_registry->registerStat(&d_numSatCalls); + d_registry->registerStat(&d_numVariables); + d_registry->registerStat(&d_numClauses); + d_registry->registerStat(&d_solveTime); +} + +CadicalSolver::Statistics::~Statistics() { + d_registry->unregisterStat(&d_numSatCalls); + d_registry->unregisterStat(&d_numVariables); + d_registry->unregisterStat(&d_numClauses); + d_registry->unregisterStat(&d_solveTime); +} + +} // namespace prop +} // namespace CVC4 + +#endif // CVC4_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h new file mode 100644 index 000000000..2e2c1cc51 --- /dev/null +++ b/src/prop/cadical.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file cadical.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Wrapper for CaDiCaL SAT Solver. + ** + ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__CADICAL_H +#define __CVC4__PROP__CADICAL_H + +#ifdef CVC4_USE_CADICAL + +#include "prop/sat_solver.h" + +#include <cadical.hpp> + +namespace CVC4 { +namespace prop { + +class CadicalSolver : public SatSolver +{ + public: + CadicalSolver(StatisticsRegistry* registry, const std::string& name = ""); + + ~CadicalSolver() override; + + ClauseId addClause(SatClause& clause, bool removable) override; + + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override; + + SatVariable newVar(bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true) override; + + SatVariable trueVar() override; + + SatVariable falseVar() override; + + SatValue solve() override; + + SatValue solve(long unsigned int&) override; + + void interrupt() override; + + SatValue value(SatLiteral l) override; + + SatValue modelValue(SatLiteral l) override; + + unsigned getAssertionLevel() const override; + + bool ok() const override; + + private: + std::unique_ptr<CaDiCaL::Solver> d_solver; + + unsigned d_nextVarIdx; + bool d_okay; + SatVariable d_true; + SatVariable d_false; + + struct Statistics + { + StatisticsRegistry* d_registry; + IntStat d_numSatCalls; + IntStat d_numVariables; + IntStat d_numClauses; + TimerStat d_solveTime; + Statistics(StatisticsRegistry* registry, const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +} // namespace prop +} // namespace CVC4 + +#endif // CVC4_USE_CADICAL +#endif // __CVC4__PROP__CADICAL_H diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index c48a54afb..249a5eabb 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -79,9 +79,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, } -CryptoMinisatSolver::~CryptoMinisatSolver() { - delete d_solver; -} +CryptoMinisatSolver::~CryptoMinisatSolver() {} ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, bool rhs, diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index 32c05974b..c1782b6c0 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -38,7 +38,7 @@ namespace prop { class CryptoMinisatSolver : public SatSolver { private: - CMSat::SATSolver* d_solver; + std::unique_ptr<CMSat::SATSolver> d_solver; unsigned d_numVariables; bool d_okay; SatVariable d_true; diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 69fca59e1..0a8246667 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -17,6 +17,7 @@ #include "prop/sat_solver_factory.h" #include "prop/bvminisat/bvminisat.h" +#include "prop/cadical.h" #include "prop/cryptominisat.h" #include "prop/minisat/minisat.h" @@ -31,6 +32,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat( return new BVMinisatSatSolver(registry, mainSatContext, name); } +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat( + StatisticsRegistry* registry) +{ + return new MinisatSatSolver(registry); +} + SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, const std::string& name) { @@ -41,10 +48,14 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, #endif } -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat( - StatisticsRegistry* registry) +SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry, + const std::string& name) { - return new MinisatSatSolver(registry); +#ifdef CVC4_USE_CADICAL + return new CadicalSolver(registry, name); +#else + Unreachable("CVC4 was not compiled with CaDiCaL support."); +#endif } } // namespace prop diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index fac8c9083..8d6e405d8 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -16,7 +16,8 @@ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H +#define __CVC4__PROP__SAT_SOLVER_FACTORY_H #include <string> #include <vector> @@ -28,17 +29,25 @@ namespace CVC4 { namespace prop { -class SatSolverFactory { -public: - +class SatSolverFactory +{ + public: static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = ""); - static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); + + static DPLLSatSolverInterface* createDPLLMinisat( + StatisticsRegistry* registry); + static SatSolver* createCryptoMinisat(StatisticsRegistry* registry, const std::string& name = ""); -};/* class SatSolverFactory */ + static SatSolver* createCadical(StatisticsRegistry* registry, + const std::string& name = ""); + +}; /* class SatSolverFactory */ + +} // namespace prop +} // namespace CVC4 -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +#endif // __CVC4__PROP__SAT_SOLVER_FACTORY_H |