1 /*********************                                                        */
2 /*! \file sat_solver_types.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Dejan Jovanovic, Liana Hadarean, Kshitij Bansal
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 */
invertValue(SatValue v)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    */
SatLiteral()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    */
getSatVariable()92   SatVariable getSatVariable() const {
93     return d_value >> 1;
94   }
95 
96   /**
97    * Returns true if the literal is a negated variable.
98    */
isNegated()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    * Returns a string representation of the literal.
126    */
toString()127   std::string toString() const {
128     std::ostringstream os;
129     os << (isNegated()? "~" : "") << getSatVariable() << " ";
130     return os.str();
131   }
132 
133   /**
134    * Returns the hash value of a literal.
135    */
hash()136   size_t hash() const {
137     return (size_t)d_value;
138   }
139 
toInt()140   uint64_t toInt() const {
141     return d_value;
142   }
143 
144   /**
145    * Returns true if the literal is undefined.
146    */
isNull()147   bool isNull() const {
148     return getSatVariable() == undefSatVariable;
149   }
150 };
151 
152 /**
153  * A constant representing a undefined literal.
154  */
155 const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
156 
157 /**
158  * Helper for hashing the literals.
159  */
160 struct SatLiteralHashFunction {
operatorSatLiteralHashFunction161   inline size_t operator() (const SatLiteral& literal) const {
162     return literal.hash();
163   }
164 };
165 
166 /**
167  * A SAT clause is a vector of literals.
168  */
169 typedef std::vector<SatLiteral> SatClause;
170 
171 struct SatClauseSetHashFunction
172 {
operatorSatClauseSetHashFunction173   inline size_t operator()(
174       const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
175       const
176   {
177     size_t acc = 0;
178     for (const auto& l : clause)
179     {
180       acc ^= l.hash();
181     }
182     return acc;
183   }
184 };
185 
186 /**
187  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
188  * so that the SAT solver can (or should) remove them when the lifespan is over.
189  */
190 enum SatSolverLifespan
191 {
192   /**
193    * The object should stay forever and never be removed
194    */
195   SAT_LIFESPAN_PERMANENT,
196   /**
197    * The object can be removed at any point when it becomes unnecessary.
198    */
199   SAT_LIFESPAN_REMOVABLE,
200   /**
201    * The object must be removed as soon as the SAT solver exits the search context
202    * where the object got introduced.
203    */
204   SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
205   /**
206    * The object can be removed when SAT solver exits the search context where the object
207    * got introduced, but can be kept at the solver discretion.
208    */
209   SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
210   /**
211    * The object must be removed as soon as the SAT solver exits the user-level context where
212    * the object got introduced.
213    */
214   SAT_LIFESPAN_USER_CONTEXT_STRICT,
215   /**
216    * The object can be removed when the SAT solver exits the user-level context where
217    * the object got introduced.
218    */
219   SAT_LIFESPAN_USER_CONTEXT_LENIENT
220 };
221 
222 }
223 }
224 
225 
226