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 |
|
#include "cvc5_private.h" |
22 |
|
|
23 |
|
#ifndef Minisat_SolverTypes_h |
24 |
|
#define Minisat_SolverTypes_h |
25 |
|
|
26 |
|
#include "base/check.h" |
27 |
|
#include "base/output.h" |
28 |
|
#include "prop/minisat/mtl/Alg.h" |
29 |
|
#include "prop/minisat/mtl/Alloc.h" |
30 |
|
#include "prop/minisat/mtl/IntTypes.h" |
31 |
|
#include "prop/minisat/mtl/Map.h" |
32 |
|
#include "prop/minisat/mtl/Vec.h" |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace Minisat { |
36 |
|
|
37 |
|
class Solver; |
38 |
|
|
39 |
|
//================================================================================================= |
40 |
|
// Variables, literals, lifted booleans, clauses: |
41 |
|
|
42 |
|
|
43 |
|
// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, |
44 |
|
// so that they can be used as array indices. |
45 |
|
|
46 |
|
typedef int Var; |
47 |
|
#define var_Undef (-1) |
48 |
|
|
49 |
|
|
50 |
|
|
51 |
|
struct Lit { |
52 |
|
int x; |
53 |
|
|
54 |
|
// Use this as a constructor: |
55 |
|
friend Lit mkLit(Var var, bool sign); |
56 |
|
|
57 |
4079546481 |
bool operator == (Lit p) const { return x == p.x; } |
58 |
335543147 |
bool operator != (Lit p) const { return x != p.x; } |
59 |
35969920 |
bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering. |
60 |
|
}; |
61 |
|
|
62 |
|
|
63 |
72619335 |
inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } |
64 |
1440149778 |
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } |
65 |
|
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } |
66 |
2598687380 |
inline bool sign (Lit p) { return p.x & 1; } |
67 |
7363898868 |
inline int var (Lit p) { return p.x >> 1; } |
68 |
|
|
69 |
|
// Mapping Literals to and from compact integers suitable for array indexing: |
70 |
14717612 |
inline int toInt(Var v) { return v; } |
71 |
319444506 |
inline int toInt(Lit p) { return p.x; } |
72 |
72533 |
inline Lit toLit(int i) |
73 |
|
{ |
74 |
|
Lit p; |
75 |
72533 |
p.x = i; |
76 |
72533 |
return p; |
77 |
|
} |
78 |
|
|
79 |
|
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants. |
80 |
|
//const Lit lit_Error = mkLit(var_Undef, true ); // } |
81 |
|
|
82 |
|
const Lit lit_Undef = { -2 }; // }- Useful special constants. |
83 |
|
const Lit lit_Error = { -1 }; // } |
84 |
|
|
85 |
|
//================================================================================================= |
86 |
|
// Lifted booleans: |
87 |
|
// |
88 |
|
// NOTE: this implementation is optimized for the case when comparisons between |
89 |
|
// values are mostly |
90 |
|
// between one variable and one constant. Some care had to be taken to |
91 |
|
// make sure that gcc does enough constant propagation to produce sensible |
92 |
|
// code, and this appears to be somewhat fragile unfortunately. |
93 |
|
|
94 |
|
/* |
95 |
|
This is to avoid multiple definitions of l_True, l_False and l_Undef if using |
96 |
|
multiple copies of Minisat. IMPORTANT: if we you change the value of the |
97 |
|
constants so that it is not the same in all copies of Minisat this breaks! |
98 |
|
*/ |
99 |
|
|
100 |
|
#ifndef l_True |
101 |
|
#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants. |
102 |
|
#endif |
103 |
|
|
104 |
|
#ifndef l_False |
105 |
|
#define l_False (lbool((uint8_t)1)) |
106 |
|
#endif |
107 |
|
|
108 |
|
#ifndef l_Undef |
109 |
|
#define l_Undef (lbool((uint8_t)2)) |
110 |
|
#endif |
111 |
|
|
112 |
|
class lbool { |
113 |
|
uint8_t value; |
114 |
|
|
115 |
|
public: |
116 |
4846381080 |
explicit lbool(uint8_t v) : value(v) { } |
117 |
|
|
118 |
619953 |
lbool() : value(0) { } |
119 |
116372061 |
explicit lbool(bool x) : value(!x) { } |
120 |
|
|
121 |
2388654460 |
bool operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); } |
122 |
1156428106 |
bool operator != (lbool b) const { return !(*this == b); } |
123 |
2347264086 |
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); } |
124 |
|
|
125 |
|
lbool operator&&(lbool b) const |
126 |
|
{ |
127 |
|
uint8_t sel = (this->value << 1) | (b.value << 3); |
128 |
|
uint8_t v = (0xF7F755F4 >> sel) & 3; |
129 |
|
return lbool(v); |
130 |
|
} |
131 |
|
|
132 |
|
lbool operator || (lbool b) const { |
133 |
|
uint8_t sel = (this->value << 1) | (b.value << 3); |
134 |
|
uint8_t v = (0xFCFCF400 >> sel) & 3; |
135 |
|
return lbool(v); } |
136 |
|
|
137 |
|
friend int toInt (lbool l); |
138 |
|
friend lbool toLbool(int v); |
139 |
|
}; |
140 |
|
inline int toInt (lbool l) { return l.value; } |
141 |
|
inline lbool toLbool(int v) { return lbool((uint8_t)v); } |
142 |
|
|
143 |
|
|
144 |
|
class Clause; |
145 |
|
typedef RegionAllocator<uint32_t>::Ref CRef; |
146 |
|
|
147 |
|
/* convenience printing functions */ |
148 |
|
|
149 |
|
|
150 |
|
inline std::ostream& operator <<(std::ostream& out, Minisat::Lit lit) { |
151 |
|
const char * s = (Minisat::sign(lit)) ? "~" : " "; |
152 |
|
out << s << Minisat::var(lit); |
153 |
|
return out; |
154 |
|
} |
155 |
|
|
156 |
|
inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>& clause) { |
157 |
|
out << "clause:"; |
158 |
|
for(int i = 0; i < clause.size(); ++i) { |
159 |
|
out << " " << clause[i]; |
160 |
|
} |
161 |
|
out << ";"; |
162 |
|
return out; |
163 |
|
} |
164 |
|
|
165 |
|
inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { |
166 |
|
std::string val_str; |
167 |
|
if( val == l_False ) { |
168 |
|
val_str = "0"; |
169 |
|
} else if (val == l_True ) { |
170 |
|
val_str = "1"; |
171 |
|
} else { // unknown |
172 |
|
val_str = "_"; |
173 |
|
} |
174 |
|
|
175 |
|
out << val_str; |
176 |
|
return out; |
177 |
|
} |
178 |
|
|
179 |
|
} // namespace Minisat |
180 |
|
} // namespace cvc5 |
181 |
|
|
182 |
|
namespace cvc5 { |
183 |
|
namespace Minisat{ |
184 |
|
|
185 |
|
//================================================================================================= |
186 |
|
// Clause -- a simple class for representing a clause: |
187 |
|
|
188 |
|
class Clause { |
189 |
|
struct { |
190 |
|
unsigned mark : 2; |
191 |
|
unsigned removable : 1; |
192 |
|
unsigned has_extra : 1; |
193 |
|
unsigned reloced : 1; |
194 |
|
unsigned size : 27; |
195 |
|
unsigned level : 32; } header; |
196 |
|
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; |
197 |
|
|
198 |
|
friend class ClauseAllocator; |
199 |
|
|
200 |
|
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory). |
201 |
|
template<class V> |
202 |
5669597 |
Clause(const V& ps, bool use_extra, bool removable, int level) { |
203 |
5669597 |
header.mark = 0; |
204 |
5669597 |
header.removable = removable; |
205 |
5669597 |
header.has_extra = use_extra; |
206 |
5669597 |
header.reloced = 0; |
207 |
5669597 |
header.size = ps.size(); |
208 |
5669597 |
header.level = level; |
209 |
|
|
210 |
5669597 |
for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; |
211 |
|
|
212 |
5669597 |
if (header.has_extra){ |
213 |
5669597 |
if (header.removable) |
214 |
703433 |
data[header.size].act = 0; |
215 |
|
else |
216 |
4966164 |
calcAbstraction(); |
217 |
|
} |
218 |
5669597 |
} |
219 |
|
|
220 |
|
public: |
221 |
6730461 |
void calcAbstraction() { |
222 |
6730461 |
Assert(header.has_extra); |
223 |
6730461 |
uint32_t abstraction = 0; |
224 |
28032817 |
for (int i = 0; i < size(); i++) |
225 |
21302356 |
abstraction |= 1 << (var(data[i].lit) & 31); |
226 |
6730461 |
data[header.size].abs = abstraction; |
227 |
6730461 |
} |
228 |
|
|
229 |
90640601 |
int level () const { return header.level; } |
230 |
1744422630 |
int size () const { return header.size; } |
231 |
98098 |
void shrink(int i) |
232 |
|
{ |
233 |
98098 |
Assert(i <= size()); |
234 |
98098 |
if (header.has_extra) data[header.size - i] = data[header.size]; |
235 |
98098 |
header.size -= i; |
236 |
98098 |
} |
237 |
98098 |
void pop () { shrink(1); } |
238 |
42146957 |
bool removable () const { return header.removable; } |
239 |
2385318 |
bool has_extra () const { return header.has_extra; } |
240 |
80416760 |
uint32_t mark () const { return header.mark; } |
241 |
3836477 |
void mark (uint32_t m) { header.mark = m; } |
242 |
|
const Lit& last () const { return data[header.size-1].lit; } |
243 |
|
|
244 |
6195162 |
bool reloced () const { return header.reloced; } |
245 |
4329949 |
CRef relocation () const { return data[0].rel; } |
246 |
1826713 |
void relocate (CRef c) { header.reloced = 1; data[0].rel = c; } |
247 |
|
|
248 |
|
// NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for |
249 |
|
// subsumption operations to behave correctly. |
250 |
3283035590 |
Lit& operator [] (int i) { return data[i].lit; } |
251 |
63347856 |
Lit operator [] (int i) const { return data[i].lit; } |
252 |
8727726 |
operator const Lit* (void) const { return (Lit*)data; } |
253 |
|
|
254 |
9549082 |
float& activity() |
255 |
|
{ |
256 |
9549082 |
Assert(header.has_extra); |
257 |
9549082 |
return data[header.size].act; |
258 |
|
} |
259 |
|
uint32_t abstraction() const |
260 |
|
{ |
261 |
|
Assert(header.has_extra); |
262 |
|
return data[header.size].abs; |
263 |
|
} |
264 |
|
|
265 |
|
Lit subsumes (const Clause& other) const; |
266 |
|
void strengthen (Lit p); |
267 |
|
}; |
268 |
|
|
269 |
|
|
270 |
|
//================================================================================================= |
271 |
|
// ClauseAllocator -- a simple class for allocating memory for clauses: |
272 |
|
|
273 |
|
|
274 |
|
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef; |
275 |
|
const CRef CRef_Lazy = RegionAllocator<uint32_t>::Ref_Undef - 1; |
276 |
12808 |
class ClauseAllocator : public RegionAllocator<uint32_t> |
277 |
|
{ |
278 |
6411163 |
static int clauseWord32Size(int size, bool has_extra){ |
279 |
6411163 |
return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); } |
280 |
|
public: |
281 |
|
bool extra_clause_field; |
282 |
|
|
283 |
2820 |
ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){} |
284 |
9991 |
ClauseAllocator() : extra_clause_field(false){} |
285 |
|
|
286 |
2820 |
void moveTo(ClauseAllocator& to){ |
287 |
2820 |
to.extra_clause_field = extra_clause_field; |
288 |
2820 |
RegionAllocator<uint32_t>::moveTo(to); } |
289 |
|
|
290 |
|
template<class Lits> |
291 |
5669597 |
CRef alloc(int level, const Lits& ps, bool removable = false) |
292 |
|
{ |
293 |
5669597 |
Assert(sizeof(Lit) == sizeof(uint32_t)); |
294 |
5669597 |
Assert(sizeof(float) == sizeof(uint32_t)); |
295 |
5669597 |
bool use_extra = removable | extra_clause_field; |
296 |
|
|
297 |
5669597 |
CRef cid = RegionAllocator<uint32_t>::alloc( |
298 |
|
clauseWord32Size(ps.size(), use_extra)); |
299 |
5669597 |
new (lea(cid)) Clause(ps, use_extra, removable, level); |
300 |
|
|
301 |
5669597 |
return cid; |
302 |
|
} |
303 |
|
|
304 |
|
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL): |
305 |
860210405 |
Clause& operator[](Ref r) { return (Clause&)RegionAllocator<uint32_t>::operator[](r); } |
306 |
16802435 |
const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); } |
307 |
5669597 |
Clause* lea (Ref r) { return (Clause*)RegionAllocator<uint32_t>::lea(r); } |
308 |
90813 |
const Clause* lea (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); } |
309 |
|
Ref ael (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); } |
310 |
|
|
311 |
741566 |
void free(CRef cid) |
312 |
|
{ |
313 |
741566 |
Clause& c = operator[](cid); |
314 |
741566 |
RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); |
315 |
741566 |
} |
316 |
|
|
317 |
|
void reloc(CRef& cr, ClauseAllocator& to); |
318 |
|
// Implementation moved to Solver.cc. |
319 |
|
}; |
320 |
|
|
321 |
|
|
322 |
|
//================================================================================================= |
323 |
|
// OccLists -- a class for maintaining occurence lists with lazy deletion: |
324 |
|
|
325 |
|
template<class Idx, class Vec, class Deleted> |
326 |
19976 |
class OccLists |
327 |
|
{ |
328 |
|
vec<Vec> occs; |
329 |
|
vec<char> dirty; |
330 |
|
vec<Idx> dirties; |
331 |
|
Deleted deleted; |
332 |
|
|
333 |
|
public: |
334 |
19982 |
OccLists(const Deleted& d) : deleted(d) {} |
335 |
|
|
336 |
2739128 |
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } |
337 |
|
void resizeTo (const Idx& idx); |
338 |
|
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } |
339 |
293419753 |
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } |
340 |
969962 |
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; } |
341 |
|
|
342 |
|
void cleanAll (); |
343 |
|
void clean (const Idx& idx); |
344 |
2204796 |
void smudge (const Idx& idx){ |
345 |
2204796 |
if (dirty[toInt(idx)] == 0){ |
346 |
667596 |
dirty[toInt(idx)] = 1; |
347 |
667596 |
dirties.push(idx); |
348 |
|
} |
349 |
2204796 |
} |
350 |
|
|
351 |
|
void clear(bool free = true){ |
352 |
|
occs .clear(free); |
353 |
|
dirty .clear(free); |
354 |
|
dirties.clear(free); |
355 |
|
} |
356 |
|
}; |
357 |
|
|
358 |
|
|
359 |
|
template<class Idx, class Vec, class Deleted> |
360 |
4344769 |
void OccLists<Idx,Vec,Deleted>::cleanAll() |
361 |
|
{ |
362 |
4854540 |
for (int i = 0; i < dirties.size(); i++) |
363 |
|
// Dirties may contain duplicates so check here if a variable is already cleaned: |
364 |
509771 |
if (dirty[toInt(dirties[i])]) |
365 |
423459 |
clean(dirties[i]); |
366 |
4344769 |
dirties.clear(); |
367 |
4344769 |
} |
368 |
|
|
369 |
|
template<class Idx, class Vec, class Deleted> |
370 |
3067 |
void OccLists<Idx,Vec,Deleted>::resizeTo(const Idx& idx) |
371 |
|
{ |
372 |
3067 |
int shrinkSize = occs.size() - (toInt(idx) + 1); |
373 |
3067 |
occs.shrink(shrinkSize); |
374 |
3067 |
dirty.shrink(shrinkSize); |
375 |
|
// Remove out-of-bound indices from dirties |
376 |
|
int i, j; |
377 |
175781 |
for (i = j = 0; i < dirties.size(); i++) |
378 |
172714 |
if (toInt(dirties[i]) < occs.size()) |
379 |
17864 |
dirties[j++] = dirties[i]; |
380 |
3067 |
dirties.shrink(i - j); |
381 |
3067 |
} |
382 |
|
|
383 |
|
template<class Idx, class Vec, class Deleted> |
384 |
509771 |
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx) |
385 |
|
{ |
386 |
509771 |
Vec& vec = occs[toInt(idx)]; |
387 |
|
int i, j; |
388 |
17312206 |
for (i = j = 0; i < vec.size(); i++) |
389 |
16802435 |
if (!deleted(vec[i])) |
390 |
15143862 |
vec[j++] = vec[i]; |
391 |
509771 |
vec.shrink(i - j); |
392 |
509771 |
dirty[toInt(idx)] = 0; |
393 |
509771 |
} |
394 |
|
|
395 |
|
|
396 |
|
//================================================================================================= |
397 |
|
// CMap -- a class for mapping clauses to values: |
398 |
|
|
399 |
|
|
400 |
|
template<class T> |
401 |
|
class CMap |
402 |
|
{ |
403 |
|
struct CRefHash { |
404 |
|
uint32_t operator()(CRef cr) const { return (uint32_t)cr; } }; |
405 |
|
|
406 |
|
typedef Map<CRef, T, CRefHash> HashTable; |
407 |
|
HashTable map; |
408 |
|
|
409 |
|
public: |
410 |
|
// Size-operations: |
411 |
|
void clear () { map.clear(); } |
412 |
|
int size () const { return map.elems(); } |
413 |
|
|
414 |
|
// Insert/Remove/Test mapping: |
415 |
|
void insert (CRef cr, const T& t){ map.insert(cr, t); } |
416 |
|
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility |
417 |
|
void remove (CRef cr) { map.remove(cr); } |
418 |
|
bool has (CRef cr, T& t) { return map.peek(cr, t); } |
419 |
|
|
420 |
|
// Vector interface (the clause 'c' must already exist): |
421 |
|
const T& operator [] (CRef cr) const { return map[cr]; } |
422 |
|
T& operator [] (CRef cr) { return map[cr]; } |
423 |
|
|
424 |
|
// Iteration (not transparent at all at the moment): |
425 |
|
int bucket_count() const { return map.bucket_count(); } |
426 |
|
const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); } |
427 |
|
|
428 |
|
// Move contents to other map: |
429 |
|
void moveTo(CMap& other){ map.moveTo(other.map); } |
430 |
|
|
431 |
|
// TMP debug: |
432 |
|
void debug(){ |
433 |
|
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); } |
434 |
|
}; |
435 |
|
|
436 |
|
/*_________________________________________________________________________________________________ |
437 |
|
| |
438 |
|
| subsumes : (other : const Clause&) -> Lit |
439 |
|
| |
440 |
|
| Description: |
441 |
|
| Checks if clause subsumes 'other', and at the same time, if it can be |
442 |
|
used to simplify 'other' | by subsumption resolution. |
443 |
|
| |
444 |
|
| Result: |
445 |
|
| lit_Error - No subsumption or simplification |
446 |
|
| lit_Undef - Clause subsumes 'other' |
447 |
|
| p - The literal p can be deleted from 'other' |
448 |
|
|________________________________________________________________________________________________@*/ |
449 |
27200942 |
inline Lit Clause::subsumes(const Clause& other) const |
450 |
|
{ |
451 |
|
// We restrict subsumtion to clauses at higher levels (if !enable_incremantal this should always be false) |
452 |
27200942 |
if (level() > other.level()) { |
453 |
|
return lit_Error; |
454 |
|
} |
455 |
|
|
456 |
|
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) |
457 |
|
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0)) |
458 |
27200942 |
Assert(!header.removable); |
459 |
27200942 |
Assert(!other.header.removable); |
460 |
27200942 |
Assert(header.has_extra); |
461 |
27200942 |
Assert(other.header.has_extra); |
462 |
27200942 |
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) |
463 |
23838954 |
return lit_Error; |
464 |
|
|
465 |
3361988 |
Lit ret = lit_Undef; |
466 |
3361988 |
const Lit* c = (const Lit*)(*this); |
467 |
3361988 |
const Lit* d = (const Lit*)other; |
468 |
|
|
469 |
13368692 |
for (unsigned i = 0; i < header.size; i++) { |
470 |
|
// search for c[i] or ~c[i] |
471 |
1221550933 |
for (unsigned j = 0; j < other.header.size; j++) |
472 |
1218428606 |
if (c[i] == d[j]) |
473 |
8255657 |
goto ok; |
474 |
1210172949 |
else if (ret == lit_Undef && c[i] == ~d[j]){ |
475 |
1751047 |
ret = c[i]; |
476 |
1751047 |
goto ok; |
477 |
|
} |
478 |
|
|
479 |
|
// did not find it |
480 |
3122327 |
return lit_Error; |
481 |
10006704 |
ok:; |
482 |
|
} |
483 |
|
|
484 |
239661 |
return ret; |
485 |
|
} |
486 |
|
|
487 |
98098 |
inline void Clause::strengthen(Lit p) |
488 |
|
{ |
489 |
98098 |
remove(*this, p); |
490 |
98098 |
calcAbstraction(); |
491 |
98098 |
} |
492 |
|
|
493 |
|
//================================================================================================= |
494 |
|
} |
495 |
|
} // namespace cvc5 |
496 |
|
|
497 |
|
#endif |