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