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