src/prop/cryptominisat.cpp

   1 /*********************                                                        */
   2 /*! \file cryptominisat.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Mathias Preiner, Alex Ozdemir
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 SAT Solver.
  13  **
  14  ** Implementation of the cryptominisat for cvc4 (bitvectors).
  15  **/
  16
  17 #ifdef CVC4_USE_CRYPTOMINISAT
  18
  19 #include "prop/cryptominisat.h"
  20
  21 #include "base/check.h"
  22
  23 #include <cryptominisat5/cryptominisat.h>
  24
  25 namespace cvc5 {
  26 namespace prop {
  27
  28 using CMSatVar = unsigned;
  29
  30 // helper functions
  31 namespace {
  32
  33 CMSat::Lit toInternalLit(SatLiteral lit)
  34 {
  35   if (lit == undefSatLiteral)
  36   {
  37     return CMSat::lit_Undef;
  38   }
  39   return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
  40 }
  41
  42 SatLiteral toSatLiteral(CMSat::Lit lit)
  43 {
  44   if (lit == CMSat::lit_Undef)
  45   {
  46     return undefSatLiteral;
  47   }
  48   return SatLiteral(lit.var(), lit.sign());
  49 }
  50
  51 SatValue toSatLiteralValue(CMSat::lbool res)
  52 {
  53   if (res == CMSat::l_True) return SAT_VALUE_TRUE;
  54   if (res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
  55   Assert(res == CMSat::l_False);
  56   return SAT_VALUE_FALSE;
  57 }
  58
  59 void toInternalClause(SatClause& clause,
  60                       std::vector<CMSat::Lit>& internal_clause)
  61 {
  62   for (unsigned i = 0; i < clause.size(); ++i)
  63   {
  64     internal_clause.push_back(toInternalLit(clause[i]));
  65   }
  66   Assert(clause.size() == internal_clause.size());
  67 }
  68
  69 }  // helper functions
  70
  71 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
  72                                          const std::string& name)
  73     : d_solver(new CMSat::SATSolver()),
  74       d_numVariables(0),
  75       d_okay(true),
  76       d_statistics(registry, name)
  77 {
  78 }
  79
  80 void CryptoMinisatSolver::init()
  81 {
  82   d_true = newVar();
  83   d_false = newVar();
  84
  85   std::vector<CMSat::Lit> clause(1);
  86   clause[0] = CMSat::Lit(d_true, false);
  87   d_solver->add_clause(clause);
  88
  89   clause[0] = CMSat::Lit(d_false, true);
  90   d_solver->add_clause(clause);
  91 }
  92
  93 CryptoMinisatSolver::~CryptoMinisatSolver() {}
  94
  95 ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
  96                                            bool rhs,
  97                                            bool removable)
  98 {
  99   Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
 100
 101   if (!d_okay) {
 102     Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
 103     return ClauseIdError;
 104   }
 105
 106   ++(d_statistics.d_xorClausesAdded);
 107
 108   // ensure all sat literals have positive polarity by pushing
 109   // the negation on the result
 110   std::vector<CMSatVar> xor_clause;
 111   for (unsigned i = 0; i < clause.size(); ++i) {
 112     xor_clause.push_back(toInternalLit(clause[i]).var());
 113     rhs ^= clause[i].isNegated();
 114   }
 115   bool res = d_solver->add_xor_clause(xor_clause, rhs);
 116   d_okay &= res;
 117   return ClauseIdError;
 118 }
 119
 120 ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
 121   Debug("sat::cryptominisat") << "Add clause " << clause <<"\n";
 122
 123   if (!d_okay) {
 124     Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
 125     return ClauseIdError;
 126   }
 127
 128   ++(d_statistics.d_clausesAdded);
 129
 130   std::vector<CMSat::Lit> internal_clause;
 131   toInternalClause(clause, internal_clause);
 132   bool nowOkay = d_solver->add_clause(internal_clause);
 133
 134   ClauseId freshId;
 135   freshId = ClauseIdError;
 136
 137   d_okay &= nowOkay;
 138   return freshId;
 139 }
 140
 141 bool CryptoMinisatSolver::ok() const { return d_okay; }
 142
 143 SatVariable  CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
 144   d_solver->new_var();
 145   ++d_numVariables;
 146   Assert(d_numVariables == d_solver->nVars());
 147   return d_numVariables - 1;
 148 }
 149
 150 SatVariable CryptoMinisatSolver::trueVar() {
 151   return d_true;
 152 }
 153
 154 SatVariable CryptoMinisatSolver::falseVar() {
 155   return d_false;
 156 }
 157
 158 void CryptoMinisatSolver::markUnremovable(SatLiteral lit) {
 159   // cryptominisat supports dynamically adding back variables (?)
 160   // so this is a no-op
 161   return;
 162 }
 163
 164 void CryptoMinisatSolver::interrupt(){
 165   d_solver->interrupt_asap();
 166 }
 167
 168 SatValue CryptoMinisatSolver::solve(){
 169   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
 170   ++d_statistics.d_statCallsToSolve;
 171   return toSatLiteralValue(d_solver->solve());
 172 }
 173
 174 SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
 175   // CMSat::SalverConf conf = d_solver->getConf();
 176   Unreachable() << "Not sure how to set different limits for calls to solve in "
 177                    "Cryptominisat";
 178   return solve();
 179 }
 180
 181 SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
 182 {
 183   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
 184   std::vector<CMSat::Lit> assumpts;
 185   for (const SatLiteral& lit : assumptions)
 186   {
 187     assumpts.push_back(toInternalLit(lit));
 188   }
 189   ++d_statistics.d_statCallsToSolve;
 190   return toSatLiteralValue(d_solver->solve(&assumpts));
 191 }
 192
 193 void CryptoMinisatSolver::getUnsatAssumptions(
 194     std::vector<SatLiteral>& assumptions)
 195 {
 196   for (const CMSat::Lit& lit : d_solver->get_conflict())
 197   {
 198     assumptions.push_back(toSatLiteral(~lit));
 199   }
 200 }
 201
 202 SatValue CryptoMinisatSolver::value(SatLiteral l){
 203   const std::vector<CMSat::lbool> model = d_solver->get_model();
 204   CMSatVar var = l.getSatVariable();
 205   Assert(var < model.size());
 206   CMSat::lbool value = model[var];
 207   return toSatLiteralValue(value);
 208 }
 209
 210 SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); }
 211
 212 unsigned CryptoMinisatSolver::getAssertionLevel() const {
 213   Unreachable() << "No interface to get assertion level in Cryptominisat";
 214   return -1;
 215 }
 216
 217 // Satistics for CryptoMinisatSolver
 218
 219 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
 220                                             const std::string& prefix) :
 221   d_registry(registry),
 222   d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0),
 223   d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0),
 224   d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0),
 225   d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"),
 226   d_registerStats(!prefix.empty())
 227 {
 228   if (!d_registerStats)
 229     return;
 230
 231   d_registry->registerStat(&d_statCallsToSolve);
 232   d_registry->registerStat(&d_xorClausesAdded);
 233   d_registry->registerStat(&d_clausesAdded);
 234   d_registry->registerStat(&d_solveTime);
 235 }
 236
 237 CryptoMinisatSolver::Statistics::~Statistics() {
 238   if (!d_registerStats)
 239     return;
 240   d_registry->unregisterStat(&d_statCallsToSolve);
 241   d_registry->unregisterStat(&d_xorClausesAdded);
 242   d_registry->unregisterStat(&d_clausesAdded);
 243   d_registry->unregisterStat(&d_solveTime);
 244 }
 245
 246 }  // namespace prop
 247 }  // namespace cvc5
 248 #endif