src/prop/sat_solver_types.h

   1 /*********************                                                        */
   2 /*! \file sat_solver_types.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Alex Ozdemir, Liana Hadarean
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 This class transforms a sequence of formulas into clauses.
  13  **
  14  ** This class takes a sequence of formulas.
  15  ** It outputs a stream of clauses that is propositionally
  16  ** equi-satisfiable with the conjunction of the formulas.
  17  ** This stream is maintained in an online fashion.
  18  **
  19  ** Unlike other parts of the system it is aware of the PropEngine's
  20  ** internals such as the representation and translation of [??? -Chris]
  21  **/
  22
  23 #pragma once
  24
  25 #include "cvc4_private.h"
  26
  27 #include <sstream>
  28 #include <string>
  29 #include <unordered_set>
  30 #include <vector>
  31
  32 namespace CVC4 {
  33 namespace prop {
  34
  35 /**
  36  * Boolean values of the SAT solver.
  37  */
  38 enum SatValue {
  39   SAT_VALUE_UNKNOWN,
  40   SAT_VALUE_TRUE,
  41   SAT_VALUE_FALSE
  42 };
  43
  44 /** Helper function for inverting a SatValue */
  45 inline SatValue invertValue(SatValue v)
  46 {
  47   if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
  48   else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
  49   else return SAT_VALUE_TRUE;
  50 }
  51
  52
  53 /**
  54  * A variable of the SAT solver.
  55  */
  56 typedef uint64_t SatVariable;
  57
  58 /**
  59  * Undefined SAT solver variable.
  60  */
  61 const SatVariable undefSatVariable = SatVariable(-1);
  62
  63 /**
  64  * A SAT literal is a variable or an negated variable.
  65  */
  66 class SatLiteral {
  67
  68   /**
  69    * The value holds the variable and a bit noting if the variable is negated.
  70    */
  71   uint64_t d_value;
  72
  73 public:
  74
  75   /**
  76    * Construct an undefined SAT literal.
  77    */
  78   SatLiteral()
  79   : d_value(undefSatVariable)
  80   {}
  81
  82   /**
  83    * Construct a literal given a possible negated variable.
  84    */
  85   SatLiteral(SatVariable var, bool negated = false) {
  86     d_value = var + var + (int)negated;
  87   }
  88
  89   /**
  90    * Returns the variable of the literal.
  91    */
  92   SatVariable getSatVariable() const {
  93     return d_value >> 1;
  94   }
  95
  96   /**
  97    * Returns true if the literal is a negated variable.
  98    */
  99   bool isNegated() const {
 100     return d_value & 1;
 101   }
 102
 103   /**
 104    * Negate the given literal.
 105    */
 106   SatLiteral operator ~ () const {
 107     return SatLiteral(getSatVariable(), !isNegated());
 108   }
 109
 110   /**
 111    * Compare two literals for equality.
 112    */
 113   bool operator == (const SatLiteral& other) const {
 114     return d_value == other.d_value;
 115   }
 116
 117   /**
 118    * Compare two literals for dis-equality.
 119    */
 120   bool operator != (const SatLiteral& other) const {
 121     return !(*this == other);
 122   }
 123
 124   /**
 125    * Compare two literals
 126    */
 127   bool operator<(const SatLiteral& other) const
 128   {
 129     return getSatVariable() == other.getSatVariable()
 130                ? isNegated() < other.isNegated()
 131                : getSatVariable() < other.getSatVariable();
 132   }
 133
 134   /**
 135    * Returns a string representation of the literal.
 136    */
 137   std::string toString() const {
 138     std::ostringstream os;
 139     os << (isNegated()? "~" : "") << getSatVariable() << " ";
 140     return os.str();
 141   }
 142
 143   /**
 144    * Returns the hash value of a literal.
 145    */
 146   size_t hash() const {
 147     return (size_t)d_value;
 148   }
 149
 150   uint64_t toInt() const {
 151     return d_value;
 152   }
 153
 154   /**
 155    * Returns true if the literal is undefined.
 156    */
 157   bool isNull() const {
 158     return getSatVariable() == undefSatVariable;
 159   }
 160 };
 161
 162 /**
 163  * A constant representing a undefined literal.
 164  */
 165 const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
 166
 167 /**
 168  * Helper for hashing the literals.
 169  */
 170 struct SatLiteralHashFunction {
 171   inline size_t operator() (const SatLiteral& literal) const {
 172     return literal.hash();
 173   }
 174 };
 175
 176 /**
 177  * A SAT clause is a vector of literals.
 178  */
 179 typedef std::vector<SatLiteral> SatClause;
 180
 181 struct SatClauseSetHashFunction
 182 {
 183   inline size_t operator()(
 184       const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
 185       const
 186   {
 187     size_t acc = 0;
 188     for (const auto& l : clause)
 189     {
 190       acc ^= l.hash();
 191     }
 192     return acc;
 193   }
 194 };
 195
 196 struct SatClauseLessThan
 197 {
 198   bool operator()(const SatClause& l, const SatClause& r) const;
 199 };
 200
 201 /**
 202  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
 203  * so that the SAT solver can (or should) remove them when the lifespan is over.
 204  */
 205 enum SatSolverLifespan
 206 {
 207   /**
 208    * The object should stay forever and never be removed
 209    */
 210   SAT_LIFESPAN_PERMANENT,
 211   /**
 212    * The object can be removed at any point when it becomes unnecessary.
 213    */
 214   SAT_LIFESPAN_REMOVABLE,
 215   /**
 216    * The object must be removed as soon as the SAT solver exits the search context
 217    * where the object got introduced.
 218    */
 219   SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
 220   /**
 221    * The object can be removed when SAT solver exits the search context where the object
 222    * got introduced, but can be kept at the solver discretion.
 223    */
 224   SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
 225   /**
 226    * The object must be removed as soon as the SAT solver exits the user-level context where
 227    * the object got introduced.
 228    */
 229   SAT_LIFESPAN_USER_CONTEXT_STRICT,
 230   /**
 231    * The object can be removed when the SAT solver exits the user-level context where
 232    * the object got introduced.
 233    */
 234   SAT_LIFESPAN_USER_CONTEXT_LENIENT
 235 };
 236
 237 }
 238 }