src/prop/sat_solver.h

   1 /*********************                                                        */
   2 /*! \file sat_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Liana Hadarean, Mathias Preiner
   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  ** 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
  24 #include "context/cdlist.h"
  25 #include "context/context.h"
  26 #include "expr/node.h"
  27 #include "expr/proof_node_manager.h"
  28 #include "proof/clause_id.h"
  29 #include "prop/bv_sat_solver_notify.h"
  30 #include "prop/sat_solver_types.h"
  31 #include "util/statistics_registry.h"
  32
  33 namespace cvc5 {
  34
  35 namespace prop {
  36
  37 class TheoryProxy;
  38
  39 class SatSolver {
  40
  41 public:
  42
  43   /** Virtual destructor */
  44   virtual ~SatSolver() { }
  45
  46   /** Assert a clause in the solver. */
  47   virtual ClauseId addClause(SatClause& clause,
  48                              bool removable) = 0;
  49
  50   /** Return true if the solver supports native xor resoning */
  51   virtual bool nativeXor() { return false; }
  52
  53   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
  54   virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
  55
  56   /**
  57    * Create a new boolean variable in the solver.
  58    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
  59    * @param preRegister whether to preregister the atom with the theory
  60    * @param canErase whether the sat solver can safely eliminate this variable
  61    *
  62    */
  63   virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;
  64
  65   /** Create a new (or return an existing) boolean variable representing the constant true */
  66   virtual SatVariable trueVar() = 0;
  67
  68   /** Create a new (or return an existing) boolean variable representing the constant false */
  69   virtual SatVariable falseVar() = 0;
  70
  71   /** Check the satisfiability of the added clauses */
  72   virtual SatValue solve() = 0;
  73
  74   /** Check the satisfiability of the added clauses */
  75   virtual SatValue solve(long unsigned int&) = 0;
  76
  77   /** Check satisfiability under assumptions */
  78   virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
  79   {
  80     Unimplemented() << "Solving under assumptions not implemented";
  81     return SAT_VALUE_UNKNOWN;
  82   };
  83
  84   /**
  85    * Tell SAT solver to only do propagation on next solve().
  86    *
  87    * @return true if feature is supported, otherwise false.
  88    */
  89   virtual bool setPropagateOnly() { return false; }
  90
  91   /** Interrupt the solver */
  92   virtual void interrupt() = 0;
  93
  94   /** Call value() during the search.*/
  95   virtual SatValue value(SatLiteral l) = 0;
  96
  97   /** Call modelValue() when the search is done.*/
  98   virtual SatValue modelValue(SatLiteral l) = 0;
  99
 100   /** Get the current assertion level */
 101   virtual unsigned getAssertionLevel() const = 0;
 102
 103   /** Check if the solver is in an inconsistent state */
 104   virtual bool ok() const = 0;
 105
 106   /**
 107    * Get list of unsatisfiable assumptions.
 108    *
 109    * The returned assumptions are a subset of the assumptions provided to
 110    * the solve method.
 111    * Can only be called if satisfiability check under assumptions was used and
 112    * if it returned SAT_VALUE_FALSE.
 113    */
 114   virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
 115   {
 116     Unimplemented() << "getUnsatAssumptions not implemented";
 117   }
 118
 119 };/* class SatSolver */
 120
 121
 122 class BVSatSolverInterface: public SatSolver {
 123 public:
 124
 125   virtual ~BVSatSolverInterface() {}
 126   /** Interface for notifications */
 127
 128   virtual void setNotify(BVSatSolverNotify* notify) = 0;
 129
 130   virtual void markUnremovable(SatLiteral lit) = 0;
 131
 132   virtual void getUnsatCore(SatClause& unsatCore) = 0;
 133
 134   virtual void addMarkerLiteral(SatLiteral lit) = 0;
 135
 136   virtual SatValue propagate() = 0;
 137
 138   virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 139
 140   virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
 141
 142   virtual void popAssumption() = 0;
 143
 144 };/* class BVSatSolverInterface */
 145
 146 class CDCLTSatSolverInterface : public SatSolver
 147 {
 148  public:
 149   virtual ~CDCLTSatSolverInterface(){};
 150
 151   virtual void initialize(context::Context* context,
 152                           prop::TheoryProxy* theoryProxy,
 153                           cvc5::context::UserContext* userContext,
 154                           ProofNodeManager* pnm) = 0;
 155
 156   virtual void push() = 0;
 157
 158   virtual void pop() = 0;
 159
 160   /*
 161    * Reset the decisions in the DPLL(T) SAT solver at the current assertion
 162    * level.
 163    */
 164   virtual void resetTrail() = 0;
 165
 166   virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
 167
 168   virtual void requirePhase(SatLiteral lit) = 0;
 169
 170   virtual bool isDecision(SatVariable decn) const = 0;
 171
 172   virtual std::shared_ptr<ProofNode> getProof() = 0;
 173
 174 }; /* class CDCLTSatSolverInterface */
 175
 176 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
 177   out << lit.toString();
 178   return out;
 179 }
 180
 181 inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
 182   out << "clause:";
 183   for(unsigned i = 0; i < clause.size(); ++i) {
 184     out << " " << clause[i];
 185   }
 186   out << ";";
 187   return out;
 188 }
 189
 190 inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
 191   std::string str;
 192   switch(val) {
 193   case prop::SAT_VALUE_UNKNOWN:
 194     str = "_";
 195     break;
 196   case prop::SAT_VALUE_TRUE:
 197     str = "1";
 198     break;
 199   case prop::SAT_VALUE_FALSE:
 200     str = "0";
 201     break;
 202   default:
 203     str = "Error";
 204     break;
 205   }
 206
 207   out << str;
 208   return out;
 209 }
 210
 211 }  // namespace prop
 212 }  // namespace cvc5
 213
 214 #endif /* CVC4__PROP__SAT_MODULE_H */