src/prop/sat_solver.h

   1 /*********************                                                        */
   2 /*! \file sat_solver.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Morgan Deters, Liana Hadarean
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief SAT Solver.
  13  **
  14  ** SAT Solver.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__PROP__SAT_SOLVER_H
  20 #define __CVC4__PROP__SAT_SOLVER_H
  21
  22 #include <string>
  23 #include <stdint.h>
  24 #include "util/statistics_registry.h"
  25 #include "context/cdlist.h"
  26 #include "prop/sat_solver_types.h"
  27 #include "expr/node.h"
  28
  29 namespace CVC4 {
  30 namespace prop {
  31
  32 class TheoryProxy;
  33
  34 class SatSolver {
  35
  36 public:
  37
  38   /** Virtual destructor */
  39   virtual ~SatSolver() { }
  40
  41   /** Assert a clause in the solver. */
  42   virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
  43
  44   /**
  45    * Create a new boolean variable in the solver.
  46    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
  47    * @param preRegister whether to preregister the atom with the theory
  48    * @param canErase whether the sat solver can safely eliminate this variable
  49    *
  50    */
  51   virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;
  52
  53   /** Create a new (or return an existing) boolean variable representing the constant true */
  54   virtual SatVariable trueVar() = 0;
  55
  56   /** Create a new (or return an existing) boolean variable representing the constant false */
  57   virtual SatVariable falseVar() = 0;
  58
  59   /** Check the satisfiability of the added clauses */
  60   virtual SatValue solve() = 0;
  61
  62   /** Check the satisfiability of the added clauses */
  63   virtual SatValue solve(long unsigned int&) = 0;
  64
  65   /** Instruct the solver that it should bump its consumed resource count. */
  66   virtual void spendResource() = 0;
  67
  68   /** Interrupt the solver */
  69   virtual void interrupt() = 0;
  70
  71   /** Call value() during the search.*/
  72   virtual SatValue value(SatLiteral l) = 0;
  73
  74   /** Call modelValue() when the search is done.*/
  75   virtual SatValue modelValue(SatLiteral l) = 0;
  76
  77   /** Get the current assertion level */
  78   virtual unsigned getAssertionLevel() const = 0;
  79
  80 };/* class SatSolver */
  81
  82
  83 class BVSatSolverInterface: public SatSolver {
  84 public:
  85
  86   /** Interface for notifications */
  87   class Notify {
  88   public:
  89
  90     virtual ~Notify() {};
  91
  92     /**
  93      * If the notify returns false, the solver will break out of whatever it's currently doing
  94      * with an "unknown" answer.
  95      */
  96     virtual bool notify(SatLiteral lit) = 0;
  97
  98     /**
  99      * Notify about a learnt clause.
 100      */
 101     virtual void notify(SatClause& clause) = 0;
 102     virtual void safePoint() = 0;
 103
 104   };/* class BVSatSolverInterface::Notify */
 105
 106   virtual void setNotify(Notify* notify) = 0;
 107
 108   virtual void markUnremovable(SatLiteral lit) = 0;
 109
 110   virtual void getUnsatCore(SatClause& unsatCore) = 0;
 111
 112   virtual void addMarkerLiteral(SatLiteral lit) = 0;
 113
 114   virtual SatValue propagate() = 0;
 115
 116   virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 117
 118   virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
 119
 120   virtual void popAssumption() = 0;
 121
 122 };/* class BVSatSolverInterface */
 123
 124
 125 class DPLLSatSolverInterface: public SatSolver {
 126 public:
 127   virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0;
 128
 129   virtual void push() = 0;
 130
 131   virtual void pop() = 0;
 132
 133   virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
 134
 135   virtual void requirePhase(SatLiteral lit) = 0;
 136
 137   virtual bool flipDecision() = 0;
 138
 139   virtual bool isDecision(SatVariable decn) const = 0;
 140
 141 };/* class DPLLSatSolverInterface */
 142
 143 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
 144   out << lit.toString();
 145   return out;
 146 }
 147
 148 inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
 149   out << "clause:";
 150   for(unsigned i = 0; i < clause.size(); ++i) {
 151     out << " " << clause[i];
 152   }
 153   out << ";";
 154   return out;
 155 }
 156
 157 inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
 158   std::string str;
 159   switch(val) {
 160   case prop::SAT_VALUE_UNKNOWN:
 161     str = "_";
 162     break;
 163   case prop::SAT_VALUE_TRUE:
 164     str = "1";
 165     break;
 166   case prop::SAT_VALUE_FALSE:
 167     str = "0";
 168     break;
 169   default:
 170     str = "Error";
 171     break;
 172   }
 173
 174   out << str;
 175   return out;
 176 }
 177
 178 }/* CVC4::prop namespace */
 179 }/* CVC4 namespace */
 180
 181 #endif /* __CVC4__PROP__SAT_MODULE_H */