src/prop/sat.h

   1 /*********************                                                        */
   2 /*! \file sat.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking, dejan, cconway
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  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  ** SAT Solver.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__PROP__SAT_H
  22 #define __CVC4__PROP__SAT_H
  23
  24 // Just defining this for now, since there's no other SAT solver bindings.
  25 // Optional blocks below will be unconditionally included
  26 #define __CVC4_USE_MINISAT
  27
  28 #include "util/options.h"
  29 #include "util/stats.h"
  30 #include "theory/theory.h"
  31
  32 #ifdef __CVC4_USE_MINISAT
  33
  34 #include "prop/minisat/core/Solver.h"
  35 #include "prop/minisat/core/SolverTypes.h"
  36 #include "prop/minisat/simp/SimpSolver.h"
  37
  38 #endif /* __CVC4_USE_MINISAT */
  39
  40 namespace CVC4 {
  41
  42 class TheoryEngine;
  43
  44 namespace prop {
  45
  46 class PropEngine;
  47 class CnfStream;
  48
  49 /* Definitions of abstract types and conversion functions for SAT interface */
  50
  51 #ifdef __CVC4_USE_MINISAT
  52
  53 /** Type of the SAT variables */
  54 typedef Minisat::Var SatVariable;
  55
  56 /** Type of the Sat literals */
  57 typedef Minisat::Lit SatLiteral;
  58
  59 /** Type of the SAT clauses */
  60 typedef Minisat::vec<SatLiteral> SatClause;
  61
  62 typedef Minisat::lbool SatLiteralValue;
  63
  64 /**
  65  * Returns the variable of the literal.
  66  * @param lit the literal
  67  */
  68 inline SatVariable literalToVariable(SatLiteral lit) {
  69   return Minisat::var(lit);
  70 }
  71
  72 inline bool literalSign(SatLiteral lit) {
  73   return Minisat::sign(lit);
  74 }
  75
  76 static inline size_t
  77 hashSatLiteral(const SatLiteral& literal) {
  78   return (size_t) Minisat::toInt(literal);
  79 }
  80
  81 inline std::string stringOfLiteralValue(SatLiteralValue val) {
  82   if( val == l_False ) {
  83     return "0";
  84   } else if (val == l_True ) {
  85     return "1";
  86   } else { // unknown
  87     return "_";
  88   }
  89 }
  90 #endif /* __CVC4_USE_MINISAT */
  91
  92 /** Interface encapsulating the "input" to the solver, e.g., from the
  93  * CNF converter.
  94  *
  95  * TODO: Is it possible to push the typedefs of SatClause and SatVariable
  96  * into here, somehow?
  97  */
  98 class SatInputInterface {
  99 public:
 100   /** Virtual destructor to make g++ happy */
 101   virtual ~SatInputInterface() { }
 102   /** Assert a clause in the solver. */
 103   virtual void addClause(SatClause& clause, bool lemma) = 0;
 104   /** Create a new boolean variable in the solver. */
 105   virtual SatVariable newVar(bool theoryAtom = false) = 0;
 106 };
 107
 108 /**
 109  * The proxy class that allows us to modify the internals of the SAT solver.
 110  * It's only accessible from the PropEngine, and should be treated with major
 111  * care.
 112  */
 113 class SatSolver : public SatInputInterface {
 114
 115   /** The prop engine we are using */
 116   PropEngine* d_propEngine;
 117
 118   /** The CNF engine we are using */
 119   CnfStream* d_cnfStream;
 120
 121   /** The theory engine we are using */
 122   TheoryEngine* d_theoryEngine;
 123
 124   /** Context we will be using to synchronzie the sat solver */
 125   context::Context* d_context;
 126
 127   /** Remember the options */
 128   Options* d_options;
 129
 130   /* Pointer to the concrete SAT solver. Including this via the
 131      preprocessor saves us a level of indirection vs, e.g., defining a
 132      sub-class for each solver. */
 133
 134 #ifdef __CVC4_USE_MINISAT
 135
 136   /** Minisat solver */
 137   Minisat::SimpSolver* d_minisat;
 138
 139   class Statistics {
 140   private:
 141     ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
 142     ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
 143     ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
 144     ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
 145     ReferenceStat<uint64_t> d_statTotLiterals;
 146   public:
 147     Statistics() :
 148       d_statStarts("sat::starts"),
 149       d_statDecisions("sat::decisions"),
 150       d_statRndDecisions("sat::rnd_decisions"),
 151       d_statPropagations("sat::propagations"),
 152       d_statConflicts("sat::conflicts"),
 153       d_statClausesLiterals("sat::clauses_literals"),
 154       d_statLearntsLiterals("sat::learnts_literals"),
 155       d_statMaxLiterals("sat::max_literals"),
 156       d_statTotLiterals("sat::tot_literals")
 157     {
 158       StatisticsRegistry::registerStat(&d_statStarts);
 159       StatisticsRegistry::registerStat(&d_statDecisions);
 160       StatisticsRegistry::registerStat(&d_statRndDecisions);
 161       StatisticsRegistry::registerStat(&d_statPropagations);
 162       StatisticsRegistry::registerStat(&d_statConflicts);
 163       StatisticsRegistry::registerStat(&d_statClausesLiterals);
 164       StatisticsRegistry::registerStat(&d_statLearntsLiterals);
 165       StatisticsRegistry::registerStat(&d_statMaxLiterals);
 166       StatisticsRegistry::registerStat(&d_statTotLiterals);
 167     }
 168     ~Statistics() {
 169       StatisticsRegistry::unregisterStat(&d_statStarts);
 170       StatisticsRegistry::unregisterStat(&d_statDecisions);
 171       StatisticsRegistry::unregisterStat(&d_statRndDecisions);
 172       StatisticsRegistry::unregisterStat(&d_statPropagations);
 173       StatisticsRegistry::unregisterStat(&d_statConflicts);
 174       StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
 175       StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
 176       StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
 177       StatisticsRegistry::unregisterStat(&d_statTotLiterals);
 178     }
 179     void init(Minisat::SimpSolver* d_minisat){
 180       d_statStarts.setData(d_minisat->starts);
 181       d_statDecisions.setData(d_minisat->decisions);
 182       d_statRndDecisions.setData(d_minisat->rnd_decisions);
 183       d_statPropagations.setData(d_minisat->propagations);
 184       d_statConflicts.setData(d_minisat->conflicts);
 185       d_statClausesLiterals.setData(d_minisat->clauses_literals);
 186       d_statLearntsLiterals.setData(d_minisat->learnts_literals);
 187       d_statMaxLiterals.setData(d_minisat->max_literals);
 188       d_statTotLiterals.setData(d_minisat->tot_literals);
 189     }
 190   };
 191   Statistics d_statistics;
 192
 193 #endif /* __CVC4_USE_MINISAT */
 194
 195 protected:
 196
 197 public:
 198   /** Hash function for literals */
 199   struct SatLiteralHashFunction {
 200     inline size_t operator()(const SatLiteral& literal) const;
 201   };
 202
 203   SatSolver(PropEngine* propEngine,
 204                    TheoryEngine* theoryEngine,
 205                    context::Context* context,
 206                    const Options* options);
 207
 208   ~SatSolver();
 209
 210   bool solve();
 211
 212   void addClause(SatClause& clause, bool lemma);
 213
 214   SatVariable newVar(bool theoryAtom = false);
 215
 216   void theoryCheck(theory::Theory::Effort effort, SatClause& conflict);
 217
 218   void explainPropagation(SatLiteral l, SatClause& explanation);
 219
 220   void theoryPropagate(std::vector<SatLiteral>& output);
 221
 222   void clearPropagatedLiterals();
 223
 224   void enqueueTheoryLiteral(const SatLiteral& l);
 225
 226   void setCnfStream(CnfStream* cnfStream);
 227
 228   SatLiteralValue value(SatLiteral l);
 229 };
 230
 231 /* Functions that delegate to the concrete SAT solver. */
 232
 233 #ifdef __CVC4_USE_MINISAT
 234
 235 inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
 236                      context::Context* context, const Options* options) :
 237   d_propEngine(propEngine),
 238   d_cnfStream(NULL),
 239   d_theoryEngine(theoryEngine),
 240   d_context(context),
 241   d_statistics()
 242 {
 243   // Create the solver
 244   d_minisat = new Minisat::SimpSolver(this, d_context);
 245   // Setup the verbosity
 246   d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
 247
 248   // No random choices
 249   if(Debug.isOn("no_rnd_decisions")){
 250     d_minisat->random_var_freq = 0;
 251   }
 252
 253   d_statistics.init(d_minisat);
 254 }
 255
 256 inline SatSolver::~SatSolver() {
 257   delete d_minisat;
 258 }
 259
 260 inline bool SatSolver::solve() {
 261   return d_minisat->solve();
 262 }
 263
 264 inline void SatSolver::addClause(SatClause& clause, bool lemma) {
 265   d_minisat->addClause(clause, lemma ? Minisat::Solver::CLAUSE_LEMMA : Minisat::Solver::CLAUSE_PROBLEM);
 266 }
 267
 268 inline SatVariable SatSolver::newVar(bool theoryAtom) {
 269   return d_minisat->newVar(true, true, theoryAtom);
 270 }
 271
 272 inline SatLiteralValue SatSolver::value(SatLiteral l) {
 273   return d_minisat->modelValue(l);
 274 }
 275
 276 #endif /* __CVC4_USE_MINISAT */
 277
 278 inline size_t
 279 SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
 280   return hashSatLiteral(literal);
 281 }
 282
 283 }/* CVC4::prop namespace */
 284
 285 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
 286   const char * s = (prop::literalSign(lit)) ? "~" : " ";
 287   out << s << prop::literalToVariable(lit);
 288   return out;
 289 }
 290
 291 inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
 292   out << "clause:";
 293   for(int i = 0; i < clause.size(); ++i) {
 294     out << " " << clause[i];
 295   }
 296   out << ";";
 297   return out;
 298 }
 299
 300 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
 301   out << prop::stringOfLiteralValue(val);
 302   return out;
 303 }
 304
 305 }/* CVC4 namespace */
 306
 307 #endif /* __CVC4__PROP__SAT_H */