diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-20 16:11:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 16:11:15 -0700 |
commit | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (patch) | |
tree | 7dbdfbbae495fed26877c51267f6775f618f5d33 /src/prop/cadical.cpp | |
parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'src/prop/cadical.cpp')
-rw-r--r-- | src/prop/cadical.cpp | 165 |
1 files changed, 165 insertions, 0 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 |