1 |
|
/***********************************************************************************[SolverTypes.h] |
2 |
|
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson |
3 |
|
Copyright (c) 2007-2010, Niklas Sorensson |
4 |
|
|
5 |
|
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and |
6 |
|
associated documentation files (the "Software"), to deal in the Software without restriction, |
7 |
|
including without limitation the rights to use, copy, modify, merge, publish, distribute, |
8 |
|
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is |
9 |
|
furnished to do so, subject to the following conditions: |
10 |
|
|
11 |
|
The above copyright notice and this permission notice shall be included in all copies or |
12 |
|
substantial portions of the Software. |
13 |
|
|
14 |
|
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT |
15 |
|
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
16 |
|
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
17 |
|
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT |
18 |
|
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
19 |
|
**************************************************************************************************/ |
20 |
|
|
21 |
|
#ifndef BVMinisat_SolverTypes_h |
22 |
|
#define BVMinisat_SolverTypes_h |
23 |
|
|
24 |
|
#include "base/check.h" |
25 |
|
#include "prop/bvminisat/mtl/Alg.h" |
26 |
|
#include "prop/bvminisat/mtl/Alloc.h" |
27 |
|
#include "prop/bvminisat/mtl/IntTypes.h" |
28 |
|
#include "prop/bvminisat/mtl/Map.h" |
29 |
|
#include "prop/bvminisat/mtl/Vec.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace BVMinisat { |
33 |
|
class Solver; |
34 |
|
} |
35 |
|
template <class Solver> |
36 |
|
class TSatProof; |
37 |
|
} // namespace cvc5 |
38 |
|
|
39 |
|
namespace cvc5 { |
40 |
|
|
41 |
|
namespace BVMinisat { |
42 |
|
|
43 |
|
//================================================================================================= |
44 |
|
// Variables, literals, lifted booleans, clauses: |
45 |
|
|
46 |
|
|
47 |
|
// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, |
48 |
|
// so that they can be used as array indices. |
49 |
|
|
50 |
|
typedef int Var; |
51 |
|
#define var_Undef (-1) |
52 |
|
|
53 |
|
|
54 |
|
struct Lit { |
55 |
|
int x; |
56 |
|
|
57 |
|
// Use this as a constructor: |
58 |
|
friend Lit mkLit(Var var, bool sign); |
59 |
|
|
60 |
93836 |
bool operator == (Lit p) const { return x == p.x; } |
61 |
27228 |
bool operator != (Lit p) const { return x != p.x; } |
62 |
5892 |
bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering. |
63 |
|
}; |
64 |
|
|
65 |
68204 |
inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } |
66 |
58292 |
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } |
67 |
|
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } |
68 |
42356 |
inline bool sign (Lit p) { return p.x & 1; } |
69 |
153686 |
inline int var (Lit p) { return p.x >> 1; } |
70 |
|
|
71 |
|
// Mapping Literals to and from compact integers suitable for array indexing: |
72 |
22332 |
inline int toInt (Var v) { return v; } |
73 |
83780 |
inline int toInt (Lit p) { return p.x; } |
74 |
|
inline Lit toLit (int i) { Lit p; p.x = i; return p; } |
75 |
|
|
76 |
|
struct LitHashFunction { |
77 |
|
size_t operator () (const Lit& l) const { |
78 |
|
return toInt(l); |
79 |
|
} |
80 |
|
}; |
81 |
|
|
82 |
|
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants. |
83 |
|
//const Lit lit_Error = mkLit(var_Undef, true ); // } |
84 |
|
|
85 |
|
const Lit lit_Undef = { -2 }; // }- Useful special constants. |
86 |
|
const Lit lit_Error = { -1 }; // } |
87 |
|
|
88 |
|
//================================================================================================= |
89 |
|
// Lifted booleans: |
90 |
|
// |
91 |
|
// NOTE: this implementation is optimized for the case when comparisons between |
92 |
|
// values are mostly |
93 |
|
// between one variable and one constant. Some care had to be taken to |
94 |
|
// make sure that gcc does enough constant propagation to produce sensible |
95 |
|
// code, and this appears to be somewhat fragile unfortunately. |
96 |
|
|
97 |
|
#ifndef l_True |
98 |
|
#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants. |
99 |
|
#endif |
100 |
|
|
101 |
|
#ifndef l_False |
102 |
|
#define l_False (lbool((uint8_t)1)) |
103 |
|
#endif |
104 |
|
|
105 |
|
#ifndef l_Undef |
106 |
|
#define l_Undef (lbool((uint8_t)2)) |
107 |
|
#endif |
108 |
|
|
109 |
|
class lbool { |
110 |
|
uint8_t value; |
111 |
|
|
112 |
|
public: |
113 |
78298 |
explicit lbool(uint8_t v) : value(v) { } |
114 |
|
|
115 |
|
lbool() : value(0) { } |
116 |
3284 |
explicit lbool(bool x) : value(!x) { } |
117 |
|
|
118 |
38928 |
bool operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); } |
119 |
10696 |
bool operator != (lbool b) const { return !(*this == b); } |
120 |
35872 |
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); } |
121 |
|
|
122 |
|
lbool operator&&(lbool b) const |
123 |
|
{ |
124 |
|
uint8_t sel = (this->value << 1) | (b.value << 3); |
125 |
|
uint8_t v = (0xF7F755F4 >> sel) & 3; |
126 |
|
return lbool(v); |
127 |
|
} |
128 |
|
|
129 |
|
lbool operator || (lbool b) const { |
130 |
|
uint8_t sel = (this->value << 1) | (b.value << 3); |
131 |
|
uint8_t v = (0xFCFCF400 >> sel) & 3; |
132 |
|
return lbool(v); } |
133 |
|
|
134 |
|
friend int toInt (lbool l); |
135 |
|
friend lbool toLbool(int v); |
136 |
|
}; |
137 |
|
inline int toInt (lbool l) { return l.value; } |
138 |
|
inline lbool toLbool(int v) { return lbool((uint8_t)v); } |
139 |
|
|
140 |
|
//================================================================================================= |
141 |
|
// Clause -- a simple class for representing a clause: |
142 |
|
|
143 |
|
class Clause; |
144 |
|
typedef RegionAllocator<uint32_t>::Ref CRef; |
145 |
|
|
146 |
|
class Clause { |
147 |
|
struct { |
148 |
|
unsigned mark : 2; |
149 |
|
unsigned learnt : 1; |
150 |
|
unsigned has_extra : 1; |
151 |
|
unsigned reloced : 1; |
152 |
|
unsigned size : 27; } header; |
153 |
|
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; |
154 |
|
|
155 |
|
friend class ClauseAllocator; |
156 |
|
|
157 |
|
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory). |
158 |
|
template<class V> |
159 |
1942 |
Clause(const V& ps, bool use_extra, bool learnt) { |
160 |
1942 |
header.mark = 0; |
161 |
1942 |
header.learnt = learnt; |
162 |
1942 |
header.has_extra = use_extra; |
163 |
1942 |
header.reloced = 0; |
164 |
1942 |
header.size = ps.size(); |
165 |
|
|
166 |
1942 |
for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; |
167 |
|
|
168 |
1942 |
if (header.has_extra){ |
169 |
1942 |
if (header.learnt) |
170 |
158 |
data[header.size].act = 0; |
171 |
|
else |
172 |
1784 |
calcAbstraction(); |
173 |
|
} |
174 |
1942 |
} |
175 |
|
|
176 |
|
public: |
177 |
2490 |
void calcAbstraction() { |
178 |
2490 |
Assert(header.has_extra); |
179 |
2490 |
uint32_t abstraction = 0; |
180 |
10148 |
for (int i = 0; i < size(); i++) |
181 |
7658 |
abstraction |= 1 << (var(data[i].lit) & 31); |
182 |
2490 |
data[header.size].abs = abstraction; |
183 |
2490 |
} |
184 |
|
|
185 |
122396 |
int size () const { return header.size; } |
186 |
114 |
void shrink(int i) |
187 |
|
{ |
188 |
114 |
Assert(i <= size()); |
189 |
114 |
if (header.has_extra) data[header.size - i] = data[header.size]; |
190 |
114 |
header.size -= i; |
191 |
114 |
} |
192 |
114 |
void pop () { shrink(1); } |
193 |
4050 |
bool learnt () const { return header.learnt; } |
194 |
1290 |
bool has_extra () const { return header.has_extra; } |
195 |
51250 |
uint32_t mark () const { return header.mark; } |
196 |
4018 |
void mark (uint32_t m) { header.mark = m; } |
197 |
|
const Lit& last () const { return data[header.size-1].lit; } |
198 |
|
|
199 |
3368 |
bool reloced () const { return header.reloced; } |
200 |
2820 |
CRef relocation () const { return data[0].rel; } |
201 |
548 |
void relocate (CRef c) { header.reloced = 1; data[0].rel = c; } |
202 |
|
|
203 |
|
// NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for |
204 |
|
// subsumption operations to behave correctly. |
205 |
60948 |
Lit& operator [] (int i) { return data[i].lit; } |
206 |
47470 |
Lit operator [] (int i) const { return data[i].lit; } |
207 |
13032 |
operator const Lit* (void) const { return (Lit*)data; } |
208 |
|
|
209 |
312 |
float& activity() |
210 |
|
{ |
211 |
312 |
Assert(header.has_extra); |
212 |
312 |
return data[header.size].act; |
213 |
|
} |
214 |
|
uint32_t abstraction() const |
215 |
|
{ |
216 |
|
Assert(header.has_extra); |
217 |
|
return data[header.size].abs; |
218 |
|
} |
219 |
|
|
220 |
|
Lit subsumes (const Clause& other) const; |
221 |
|
void strengthen (Lit p); |
222 |
|
}; |
223 |
|
|
224 |
|
|
225 |
|
//================================================================================================= |
226 |
|
// ClauseAllocator -- a simple class for allocating memory for clauses: |
227 |
|
|
228 |
|
|
229 |
|
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef; |
230 |
|
const CRef CRef_Lazy = RegionAllocator<uint32_t>::Ref_Undef - 1; |
231 |
|
|
232 |
4 |
class ClauseAllocator : public RegionAllocator<uint32_t> |
233 |
|
{ |
234 |
2684 |
static int clauseWord32Size(int size, bool has_extra){ |
235 |
2684 |
return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); } |
236 |
|
public: |
237 |
|
bool extra_clause_field; |
238 |
|
|
239 |
2 |
ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){} |
240 |
2 |
ClauseAllocator() : extra_clause_field(false){} |
241 |
|
|
242 |
2 |
void moveTo(ClauseAllocator& to){ |
243 |
2 |
to.extra_clause_field = extra_clause_field; |
244 |
2 |
RegionAllocator<uint32_t>::moveTo(to); } |
245 |
|
|
246 |
|
template<class Lits> |
247 |
1942 |
CRef alloc(const Lits& ps, bool learnt = false) |
248 |
|
{ |
249 |
1942 |
Assert(sizeof(Lit) == sizeof(uint32_t)); |
250 |
1942 |
Assert(sizeof(float) == sizeof(uint32_t)); |
251 |
1942 |
bool use_extra = learnt | extra_clause_field; |
252 |
|
|
253 |
1942 |
CRef cid = RegionAllocator<uint32_t>::alloc( |
254 |
|
clauseWord32Size(ps.size(), use_extra)); |
255 |
1942 |
new (lea(cid)) Clause(ps, use_extra, learnt); |
256 |
|
|
257 |
1942 |
return cid; |
258 |
|
} |
259 |
|
|
260 |
|
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL): |
261 |
83320 |
Clause& operator[](Ref r) { return (Clause&)RegionAllocator<uint32_t>::operator[](r); } |
262 |
8822 |
const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); } |
263 |
1942 |
Clause* lea (Ref r) { return (Clause*)RegionAllocator<uint32_t>::lea(r); } |
264 |
50 |
const Clause* lea (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); } |
265 |
|
Ref ael (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); } |
266 |
|
|
267 |
742 |
void free(CRef cid) |
268 |
|
{ |
269 |
742 |
Clause& c = operator[](cid); |
270 |
742 |
RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); |
271 |
742 |
} |
272 |
|
|
273 |
|
void reloc(CRef& cr, ClauseAllocator& to); |
274 |
|
}; |
275 |
|
|
276 |
|
|
277 |
|
//================================================================================================= |
278 |
|
// OccLists -- a class for maintaining occurence lists with lazy deletion: |
279 |
|
|
280 |
|
template<class Idx, class Vec, class Deleted> |
281 |
4 |
class OccLists |
282 |
|
{ |
283 |
|
vec<Vec> occs; |
284 |
|
vec<char> dirty; |
285 |
|
vec<Idx> dirties; |
286 |
|
Deleted deleted; |
287 |
|
|
288 |
|
public: |
289 |
4 |
OccLists(const Deleted& d) : deleted(d) {} |
290 |
|
|
291 |
858 |
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } |
292 |
|
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } |
293 |
21858 |
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } |
294 |
2526 |
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; } |
295 |
|
|
296 |
|
void cleanAll (); |
297 |
|
void clean (const Idx& idx); |
298 |
3498 |
void smudge (const Idx& idx){ |
299 |
3498 |
if (dirty[toInt(idx)] == 0){ |
300 |
1278 |
dirty[toInt(idx)] = 1; |
301 |
1278 |
dirties.push(idx); |
302 |
|
} |
303 |
3498 |
} |
304 |
|
|
305 |
|
void clear(bool free = true){ |
306 |
|
occs .clear(free); |
307 |
|
dirty .clear(free); |
308 |
|
dirties.clear(free); |
309 |
|
} |
310 |
|
}; |
311 |
|
|
312 |
|
|
313 |
|
template<class Idx, class Vec, class Deleted> |
314 |
1120 |
void OccLists<Idx,Vec,Deleted>::cleanAll() |
315 |
|
{ |
316 |
2398 |
for (int i = 0; i < dirties.size(); i++) |
317 |
|
// Dirties may contain duplicates so check here if a variable is already cleaned: |
318 |
1278 |
if (dirty[toInt(dirties[i])]) |
319 |
962 |
clean(dirties[i]); |
320 |
1120 |
dirties.clear(); |
321 |
1120 |
} |
322 |
|
|
323 |
|
|
324 |
|
template<class Idx, class Vec, class Deleted> |
325 |
1278 |
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx) |
326 |
|
{ |
327 |
1278 |
Vec& vec = occs[toInt(idx)]; |
328 |
|
int i, j; |
329 |
10100 |
for (i = j = 0; i < vec.size(); i++) |
330 |
8822 |
if (!deleted(vec[i])) |
331 |
5876 |
vec[j++] = vec[i]; |
332 |
1278 |
vec.shrink(i - j); |
333 |
1278 |
dirty[toInt(idx)] = 0; |
334 |
1278 |
} |
335 |
|
|
336 |
|
|
337 |
|
//================================================================================================= |
338 |
|
// CMap -- a class for mapping clauses to values: |
339 |
|
|
340 |
|
|
341 |
|
template<class T> |
342 |
|
class CMap |
343 |
|
{ |
344 |
|
struct CRefHash { |
345 |
|
uint32_t operator()(CRef cr) const { return (uint32_t)cr; } }; |
346 |
|
|
347 |
|
typedef Map<CRef, T, CRefHash> HashTable; |
348 |
|
HashTable map; |
349 |
|
|
350 |
|
public: |
351 |
|
// Size-operations: |
352 |
|
void clear () { map.clear(); } |
353 |
|
int size () const { return map.elems(); } |
354 |
|
|
355 |
|
// Insert/Remove/Test mapping: |
356 |
|
void insert (CRef cr, const T& t){ map.insert(cr, t); } |
357 |
|
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility |
358 |
|
void remove (CRef cr) { map.remove(cr); } |
359 |
|
bool has (CRef cr, T& t) { return map.peek(cr, t); } |
360 |
|
|
361 |
|
// Vector interface (the clause 'c' must already exist): |
362 |
|
const T& operator [] (CRef cr) const { return map[cr]; } |
363 |
|
T& operator [] (CRef cr) { return map[cr]; } |
364 |
|
|
365 |
|
// Iteration (not transparent at all at the moment): |
366 |
|
int bucket_count() const { return map.bucket_count(); } |
367 |
|
const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); } |
368 |
|
|
369 |
|
// Move contents to other map: |
370 |
|
void moveTo(CMap& other){ map.moveTo(other.map); } |
371 |
|
|
372 |
|
// TMP debug: |
373 |
|
void debug(){ |
374 |
|
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); } |
375 |
|
}; |
376 |
|
|
377 |
|
/*_________________________________________________________________________________________________ |
378 |
|
| |
379 |
|
| subsumes : (other : const Clause&) -> Lit |
380 |
|
| |
381 |
|
| Description: |
382 |
|
| Checks if clause subsumes 'other', and at the same time, if it can be |
383 |
|
used to simplify 'other' | by subsumption resolution. |
384 |
|
| |
385 |
|
| Result: |
386 |
|
| lit_Error - No subsumption or simplification |
387 |
|
| lit_Undef - Clause subsumes 'other' |
388 |
|
| p - The literal p can be deleted from 'other' |
389 |
|
|________________________________________________________________________________________________@*/ |
390 |
14042 |
inline Lit Clause::subsumes(const Clause& other) const |
391 |
|
{ |
392 |
|
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) |
393 |
|
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0)) |
394 |
14042 |
Assert(!header.learnt); |
395 |
14042 |
Assert(!other.header.learnt); |
396 |
14042 |
Assert(header.has_extra); |
397 |
14042 |
Assert(other.header.has_extra); |
398 |
14042 |
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) |
399 |
10156 |
return lit_Error; |
400 |
|
|
401 |
3886 |
Lit ret = lit_Undef; |
402 |
3886 |
const Lit* c = (const Lit*)(*this); |
403 |
3886 |
const Lit* d = (const Lit*)other; |
404 |
|
|
405 |
10008 |
for (unsigned i = 0; i < header.size; i++) { |
406 |
|
// search for c[i] or ~c[i] |
407 |
28954 |
for (unsigned j = 0; j < other.header.size; j++) |
408 |
25298 |
if (c[i] == d[j]) |
409 |
2506 |
goto ok; |
410 |
22792 |
else if (ret == lit_Undef && c[i] == ~d[j]){ |
411 |
3616 |
ret = c[i]; |
412 |
3616 |
goto ok; |
413 |
|
} |
414 |
|
|
415 |
|
// did not find it |
416 |
3656 |
return lit_Error; |
417 |
6122 |
ok:; |
418 |
|
} |
419 |
|
|
420 |
230 |
return ret; |
421 |
|
} |
422 |
|
|
423 |
114 |
inline void Clause::strengthen(Lit p) |
424 |
|
{ |
425 |
114 |
remove(*this, p); |
426 |
114 |
calcAbstraction(); |
427 |
114 |
} |
428 |
|
|
429 |
|
|
430 |
|
|
431 |
|
//================================================================================================= |
432 |
|
} // namespace BVMinisat |
433 |
|
} // namespace cvc5 |
434 |
|
|
435 |
|
#endif |