src/prop/minisat/minisat.cpp

   1 /*********************                                                        */
   2 /*! \file minisat.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors:
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief SAT Solver.
  15  **
  16  ** Implementation of the minisat interface for cvc4.
  17  **/
  18
  19 #include "prop/minisat/minisat.h"
  20 #include "prop/minisat/simp/SimpSolver.h"
  21 #include "prop/options.h"
  22 #include "smt/options.h"
  23 #include "decision/options.h"
  24
  25 using namespace CVC4;
  26 using namespace CVC4::prop;
  27
  28 //// DPllMinisatSatSolver
  29
  30 MinisatSatSolver::MinisatSatSolver() :
  31   d_minisat(NULL),
  32   d_theoryProxy(NULL),
  33   d_context(NULL)
  34 {}
  35
  36 MinisatSatSolver::~MinisatSatSolver() {
  37   delete d_minisat;
  38 }
  39
  40 SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
  41   if (var == var_Undef) {
  42     return undefSatVariable;
  43   }
  44   return SatVariable(var);
  45 }
  46
  47 Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
  48   if (lit == undefSatLiteral) {
  49     return Minisat::lit_Undef;
  50   }
  51   return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
  52 }
  53
  54 SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
  55   if (lit == Minisat::lit_Undef) {
  56     return undefSatLiteral;
  57   }
  58
  59   return SatLiteral(SatVariable(Minisat::var(lit)),
  60                     Minisat::sign(lit));
  61 }
  62
  63 SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
  64   if(res) return SAT_VALUE_TRUE;
  65   else return SAT_VALUE_FALSE;
  66 }
  67
  68 SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
  69   if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
  70   if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
  71   Assert(res == (Minisat::lbool((uint8_t)1)));
  72   return SAT_VALUE_FALSE;
  73 }
  74
  75 Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
  76 {
  77   if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
  78   if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
  79   Assert(val == SAT_VALUE_FALSE);
  80   return Minisat::lbool((uint8_t)1);
  81 }
  82
  83 /*bool MinisatSatSolver::tobool(SatValue val)
  84 {
  85   if(val == SAT_VALUE_TRUE) return true;
  86   Assert(val == SAT_VALUE_FALSE);
  87   return false;
  88   }*/
  89
  90 void MinisatSatSolver::toMinisatClause(SatClause& clause,
  91                                            Minisat::vec<Minisat::Lit>& minisat_clause) {
  92   for (unsigned i = 0; i < clause.size(); ++i) {
  93     minisat_clause.push(toMinisatLit(clause[i]));
  94   }
  95   Assert(clause.size() == (unsigned)minisat_clause.size());
  96 }
  97
  98 void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
  99                                        SatClause& sat_clause) {
 100   for (int i = 0; i < clause.size(); ++i) {
 101     sat_clause.push_back(toSatLiteral(clause[i]));
 102   }
 103   Assert((unsigned)clause.size() == sat_clause.size());
 104 }
 105
 106 void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
 107                                        SatClause& sat_clause) {
 108   for (int i = 0; i < clause.size(); ++i) {
 109     sat_clause.push_back(toSatLiteral(clause[i]));
 110   }
 111   Assert((unsigned)clause.size() == sat_clause.size());
 112 }
 113
 114 void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) {
 115
 116   d_context = context;
 117
 118   if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) {
 119     Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
 120              << " unless using internal decision strategy." << std::endl;
 121   }
 122
 123   // Create the solver
 124   d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
 125                                       options::incrementalSolving() ||
 126                                       options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL );
 127
 128   d_statistics.init(d_minisat);
 129 }
 130
 131 // Like initialize() above, but called just before each search when in
 132 // incremental mode
 133 void MinisatSatSolver::setupOptions() {
 134   // Copy options from CVC4 options structure into minisat, as appropriate
 135
 136   // Set up the verbosity
 137   d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
 138
 139   // Set up the random decision parameters
 140   d_minisat->random_var_freq = options::satRandomFreq();
 141   // If 0, we use whatever we like (here, the Minisat default seed)
 142   if(options::satRandomSeed() != 0) {
 143     d_minisat->random_seed = double(options::satRandomSeed());
 144   }
 145
 146   // Give access to all possible options in the sat solver
 147   d_minisat->var_decay = options::satVarDecay();
 148   d_minisat->clause_decay = options::satClauseDecay();
 149   d_minisat->restart_first = options::satRestartFirst();
 150   d_minisat->restart_inc = options::satRestartInc();
 151 }
 152
 153 void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
 154   Minisat::vec<Minisat::Lit> minisat_clause;
 155   toMinisatClause(clause, minisat_clause);
 156   d_minisat->addClause(minisat_clause, removable);
 157 }
 158
 159 SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
 160   return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
 161 }
 162
 163 SatValue MinisatSatSolver::solve(unsigned long& resource) {
 164   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
 165   setupOptions();
 166   if(resource == 0) {
 167     d_minisat->budgetOff();
 168   } else {
 169     d_minisat->setConfBudget(resource);
 170   }
 171   Minisat::vec<Minisat::Lit> empty;
 172   unsigned long conflictsBefore = d_minisat->conflicts;
 173   SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
 174   d_minisat->clearInterrupt();
 175   resource = d_minisat->conflicts - conflictsBefore;
 176   Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
 177   return result;
 178 }
 179
 180 SatValue MinisatSatSolver::solve() {
 181   setupOptions();
 182   d_minisat->budgetOff();
 183   return toSatLiteralValue(d_minisat->solve());
 184 }
 185
 186
 187 void MinisatSatSolver::interrupt() {
 188   d_minisat->interrupt();
 189 }
 190
 191 SatValue MinisatSatSolver::value(SatLiteral l) {
 192   return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 193 }
 194
 195 SatValue MinisatSatSolver::modelValue(SatLiteral l){
 196   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 197 }
 198
 199 bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
 200   return true;
 201 }
 202
 203 void MinisatSatSolver::requirePhase(SatLiteral lit) {
 204   Assert(!d_minisat->rnd_pol);
 205   Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
 206   SatVariable v = lit.getSatVariable();
 207   d_minisat->freezePolarity(v, lit.isNegated());
 208 }
 209
 210 bool MinisatSatSolver::flipDecision() {
 211   Debug("minisat") << "flipDecision()" << std::endl;
 212   return d_minisat->flipDecision();
 213 }
 214
 215 bool MinisatSatSolver::isDecision(SatVariable decn) const {
 216   return d_minisat->isDecision( decn );
 217 }
 218
 219 /** Incremental interface */
 220
 221 unsigned MinisatSatSolver::getAssertionLevel() const {
 222   return d_minisat->getAssertionLevel();
 223 }
 224
 225 void MinisatSatSolver::push() {
 226   d_minisat->push();
 227 }
 228
 229 void MinisatSatSolver::pop(){
 230   d_minisat->pop();
 231 }
 232
 233 /// Statistics for MinisatSatSolver
 234
 235 MinisatSatSolver::Statistics::Statistics() :
 236   d_statStarts("sat::starts"),
 237   d_statDecisions("sat::decisions"),
 238   d_statRndDecisions("sat::rnd_decisions"),
 239   d_statPropagations("sat::propagations"),
 240   d_statConflicts("sat::conflicts"),
 241   d_statClausesLiterals("sat::clauses_literals"),
 242   d_statLearntsLiterals("sat::learnts_literals"),
 243   d_statMaxLiterals("sat::max_literals"),
 244   d_statTotLiterals("sat::tot_literals")
 245 {
 246   StatisticsRegistry::registerStat(&d_statStarts);
 247   StatisticsRegistry::registerStat(&d_statDecisions);
 248   StatisticsRegistry::registerStat(&d_statRndDecisions);
 249   StatisticsRegistry::registerStat(&d_statPropagations);
 250   StatisticsRegistry::registerStat(&d_statConflicts);
 251   StatisticsRegistry::registerStat(&d_statClausesLiterals);
 252   StatisticsRegistry::registerStat(&d_statLearntsLiterals);
 253   StatisticsRegistry::registerStat(&d_statMaxLiterals);
 254   StatisticsRegistry::registerStat(&d_statTotLiterals);
 255 }
 256 MinisatSatSolver::Statistics::~Statistics() {
 257   StatisticsRegistry::unregisterStat(&d_statStarts);
 258   StatisticsRegistry::unregisterStat(&d_statDecisions);
 259   StatisticsRegistry::unregisterStat(&d_statRndDecisions);
 260   StatisticsRegistry::unregisterStat(&d_statPropagations);
 261   StatisticsRegistry::unregisterStat(&d_statConflicts);
 262   StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
 263   StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
 264   StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
 265   StatisticsRegistry::unregisterStat(&d_statTotLiterals);
 266 }
 267 void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
 268   d_statStarts.setData(d_minisat->starts);
 269   d_statDecisions.setData(d_minisat->decisions);
 270   d_statRndDecisions.setData(d_minisat->rnd_decisions);
 271   d_statPropagations.setData(d_minisat->propagations);
 272   d_statConflicts.setData(d_minisat->conflicts);
 273   d_statClausesLiterals.setData(d_minisat->clauses_literals);
 274   d_statLearntsLiterals.setData(d_minisat->learnts_literals);
 275   d_statMaxLiterals.setData(d_minisat->max_literals);
 276   d_statTotLiterals.setData(d_minisat->tot_literals);
 277 }