src/prop/cadical.cpp

   1 /*********************                                                        */
   2 /*! \file cadical.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andres Noetzli, Liana Hadarean
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Wrapper for CaDiCaL SAT Solver.
  13  **
  14  ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors).
  15  **/
  16
  17 #include "prop/cadical.h"
  18
  19 #ifdef CVC4_USE_CADICAL
  20
  21 #include "base/check.h"
  22
  23 namespace CVC4 {
  24 namespace prop {
  25
  26 using CadicalLit = int;
  27 using CadicalVar = int;
  28
  29 // helper functions
  30 namespace {
  31
  32 SatValue toSatValue(int result)
  33 {
  34   if (result == 10) return SAT_VALUE_TRUE;
  35   if (result == 20) return SAT_VALUE_FALSE;
  36   Assert(result == 0);
  37   return SAT_VALUE_UNKNOWN;
  38 }
  39
  40 /* Note: CaDiCaL returns lit/-lit for true/false. Older versions returned 1/-1.
  41  */
  42 SatValue toSatValueLit(int value)
  43 {
  44   if (value > 0) return SAT_VALUE_TRUE;
  45   Assert(value < 0);
  46   return SAT_VALUE_FALSE;
  47 }
  48
  49 CadicalLit toCadicalLit(const SatLiteral lit)
  50 {
  51   return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
  52 }
  53
  54 CadicalVar toCadicalVar(SatVariable var) { return var; }
  55
  56 }  // namespace helper functions
  57
  58 CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
  59                              const std::string& name)
  60     : d_solver(new CaDiCaL::Solver()),
  61       // Note: CaDiCaL variables start with index 1 rather than 0 since negated
  62       //       literals are represented as the negation of the index.
  63       d_nextVarIdx(1),
  64       d_statistics(registry, name)
  65 {
  66 }
  67
  68 void CadicalSolver::init()
  69 {
  70   d_true = newVar();
  71   d_false = newVar();
  72
  73   d_solver->set("quiet", 1);  // CaDiCaL is verbose by default
  74   d_solver->add(toCadicalVar(d_true));
  75   d_solver->add(0);
  76   d_solver->add(-toCadicalVar(d_false));
  77   d_solver->add(0);
  78 }
  79
  80 CadicalSolver::~CadicalSolver() {}
  81
  82 ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
  83 {
  84   for (const SatLiteral& lit : clause)
  85   {
  86     d_solver->add(toCadicalLit(lit));
  87   }
  88   d_solver->add(0);
  89   ++d_statistics.d_numClauses;
  90   return ClauseIdError;
  91 }
  92
  93 ClauseId CadicalSolver::addXorClause(SatClause& clause,
  94                                      bool rhs,
  95                                      bool removable)
  96 {
  97   Unreachable() << "CaDiCaL does not support adding XOR clauses.";
  98 }
  99
 100 SatVariable CadicalSolver::newVar(bool isTheoryAtom,
 101                                   bool preRegister,
 102                                   bool canErase)
 103 {
 104   ++d_statistics.d_numVariables;
 105   return d_nextVarIdx++;
 106 }
 107
 108 SatVariable CadicalSolver::trueVar() { return d_true; }
 109
 110 SatVariable CadicalSolver::falseVar() { return d_false; }
 111
 112 SatValue CadicalSolver::solve()
 113 {
 114   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
 115   SatValue res = toSatValue(d_solver->solve());
 116   d_okay = (res == SAT_VALUE_TRUE);
 117   ++d_statistics.d_numSatCalls;
 118   return res;
 119 }
 120
 121 SatValue CadicalSolver::solve(long unsigned int&)
 122 {
 123   Unimplemented() << "Setting limits for CaDiCaL not supported yet";
 124 };
 125
 126 SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
 127 {
 128   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
 129   for (const SatLiteral& lit : assumptions)
 130   {
 131     d_solver->assume(toCadicalLit(lit));
 132   }
 133   SatValue res = toSatValue(d_solver->solve());
 134   d_okay = (res == SAT_VALUE_TRUE);
 135   ++d_statistics.d_numSatCalls;
 136   return res;
 137 }
 138
 139 void CadicalSolver::interrupt() { d_solver->terminate(); }
 140
 141 SatValue CadicalSolver::value(SatLiteral l)
 142 {
 143   Assert(d_okay);
 144   return toSatValueLit(d_solver->val(toCadicalLit(l)));
 145 }
 146
 147 SatValue CadicalSolver::modelValue(SatLiteral l)
 148 {
 149   Assert(d_okay);
 150   return value(l);
 151 }
 152
 153 unsigned CadicalSolver::getAssertionLevel() const
 154 {
 155   Unreachable() << "CaDiCaL does not support assertion levels.";
 156 }
 157
 158 bool CadicalSolver::ok() const { return d_okay; }
 159
 160 CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
 161                                       const std::string& prefix)
 162     : d_registry(registry),
 163       d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0),
 164       d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0),
 165       d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0),
 166       d_solveTime("theory::bv::" + prefix + "::cadical::solve_time")
 167 {
 168   d_registry->registerStat(&d_numSatCalls);
 169   d_registry->registerStat(&d_numVariables);
 170   d_registry->registerStat(&d_numClauses);
 171   d_registry->registerStat(&d_solveTime);
 172 }
 173
 174 CadicalSolver::Statistics::~Statistics() {
 175   d_registry->unregisterStat(&d_numSatCalls);
 176   d_registry->unregisterStat(&d_numVariables);
 177   d_registry->unregisterStat(&d_numClauses);
 178   d_registry->unregisterStat(&d_solveTime);
 179 }
 180
 181 }  // namespace prop
 182 }  // namespace CVC4
 183
 184 #endif  // CVC4_USE_CADICAL