1 /***********************************************************************************[SolverTypes.h]
2 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2007-2010, Niklas Sorensson
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:
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
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 **************************************************************************************************/
22 #ifndef Minisat_SolverTypes_h
23 #define Minisat_SolverTypes_h
27 #include "libs/minisat/IntTypes.h"
28 #include "libs/minisat/Alg.h"
29 #include "libs/minisat/Vec.h"
30 #include "libs/minisat/IntMap.h"
31 #include "libs/minisat/Map.h"
32 #include "libs/minisat/Alloc.h"
36 //=================================================================================================
37 // Variables, literals, lifted booleans, clauses:
40 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
41 // so that they can be used as array indices.
44 #if defined(MINISAT_CONSTANTS_AS_MACROS)
45 #define var_Undef (-1)
47 const Var var_Undef
= -1;
54 // Use this as a constructor:
55 friend Lit
mkLit(Var var
, bool sign
);
57 bool operator == (Lit p
) const { return x
== p
.x
; }
58 bool operator != (Lit p
) const { return x
!= p
.x
; }
59 bool operator < (Lit p
) const { return x
< p
.x
; } // '<' makes p, ~p adjacent in the ordering.
63 inline Lit
mkLit (Var var
, bool sign
= false) { Lit p
; p
.x
= var
+ var
+ (int)sign
; return p
; }
64 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 inline bool sign (Lit p
) { return p
.x
& 1; }
67 inline int var (Lit p
) { return p
.x
>> 1; }
69 // Mapping Literals to and from compact integers suitable for array indexing:
70 inline int toInt (Var v
) { return v
; }
71 inline int toInt (Lit p
) { return p
.x
; }
72 inline Lit
toLit (int i
) { Lit p
; p
.x
= i
; return p
; }
74 //const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
75 //const Lit lit_Error = mkLit(var_Undef, true ); // }
77 const Lit lit_Undef
= { -2 }; // }- Useful special constants.
78 const Lit lit_Error
= { -1 }; // }
80 struct MkIndexLit
{ vec
<Lit
>::Size
operator()(Lit l
) const { return vec
<Lit
>::Size(l
.x
); } };
82 template<class T
> class VMap
: public IntMap
<Var
, T
>{};
83 template<class T
> class LMap
: public IntMap
<Lit
, T
, MkIndexLit
>{};
84 class LSet
: public IntSet
<Lit
, MkIndexLit
>{};
86 //=================================================================================================
89 // NOTE: this implementation is optimized for the case when comparisons between values are mostly
90 // between one variable and one constant. Some care had to be taken to make sure that gcc
91 // does enough constant propagation to produce sensible code, and this appears to be somewhat
92 // fragile unfortunately.
98 explicit lbool(uint8_t v
) : value(v
) { }
100 lbool() : value(0) { }
101 explicit lbool(bool x
) : value(!x
) { }
103 bool operator == (lbool b
) const { return ((b
.value
&2) & (value
&2)) | (!(b
.value
&2)&(value
== b
.value
)); }
104 bool operator != (lbool b
) const { return !(*this == b
); }
105 lbool
operator ^ (bool b
) const { return lbool((uint8_t)(value
^(uint8_t)b
)); }
107 lbool
operator && (lbool b
) const {
108 uint8_t sel
= (this->value
<< 1) | (b
.value
<< 3);
109 uint8_t v
= (0xF7F755F4 >> sel
) & 3;
112 lbool
operator || (lbool b
) const {
113 uint8_t sel
= (this->value
<< 1) | (b
.value
<< 3);
114 uint8_t v
= (0xFCFCF400 >> sel
) & 3;
117 friend int toInt (lbool l
);
118 friend lbool
toLbool(int v
);
120 inline int toInt (lbool l
) { return l
.value
; }
121 inline lbool
toLbool(int v
) { return lbool((uint8_t)v
); }
123 #if defined(MINISAT_CONSTANTS_AS_MACROS)
124 #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
125 #define l_False (lbool((uint8_t)1))
126 #define l_Undef (lbool((uint8_t)2))
128 const lbool
l_True ((uint8_t)0);
129 const lbool
l_False((uint8_t)1);
130 const lbool
l_Undef((uint8_t)2);
134 //=================================================================================================
135 // Clause -- a simple class for representing a clause:
138 typedef RegionAllocator
<uint32_t>::Ref CRef
;
144 unsigned has_extra
: 1;
145 unsigned reloced
: 1;
146 unsigned size
: 27; } header
;
147 union { Lit lit
; float act
; uint32_t abs
; CRef rel
; } data
[0];
149 friend class ClauseAllocator
;
151 // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
152 Clause(const vec
<Lit
>& ps
, bool use_extra
, bool learnt
) {
154 header
.learnt
= learnt
;
155 header
.has_extra
= use_extra
;
157 header
.size
= ps
.size();
159 for (int i
= 0; i
< ps
.size(); i
++)
162 if (header
.has_extra
){
164 data
[header
.size
].act
= 0;
170 // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
171 Clause(const Clause
& from
, bool use_extra
){
172 header
= from
.header
;
173 header
.has_extra
= use_extra
; // NOTE: the copied clause may lose the extra field.
175 for (int i
= 0; i
< from
.size(); i
++)
176 data
[i
].lit
= from
[i
];
178 if (header
.has_extra
){
180 data
[header
.size
].act
= from
.data
[header
.size
].act
;
182 data
[header
.size
].abs
= from
.data
[header
.size
].abs
;
187 void calcAbstraction() {
188 assert(header
.has_extra
);
189 uint32_t abstraction
= 0;
190 for (int i
= 0; i
< size(); i
++)
191 abstraction
|= 1 << (var(data
[i
].lit
) & 31);
192 data
[header
.size
].abs
= abstraction
; }
195 int size () const { return header
.size
; }
196 void shrink (int i
) { assert(i
<= size()); if (header
.has_extra
) data
[header
.size
-i
] = data
[header
.size
]; header
.size
-= i
; }
197 void pop () { shrink(1); }
198 bool learnt () const { return header
.learnt
; }
199 bool has_extra () const { return header
.has_extra
; }
200 uint32_t mark () const { return header
.mark
; }
201 void mark (uint32_t m
) { header
.mark
= m
; }
202 const Lit
& last () const { return data
[header
.size
-1].lit
; }
204 bool reloced () const { return header
.reloced
; }
205 CRef
relocation () const { return data
[0].rel
; }
206 void relocate (CRef c
) { header
.reloced
= 1; data
[0].rel
= c
; }
208 // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
209 // subsumption operations to behave correctly.
210 Lit
& operator [] (int i
) { return data
[i
].lit
; }
211 Lit
operator [] (int i
) const { return data
[i
].lit
; }
212 operator const Lit
* (void) const { return (Lit
*)data
; }
214 float& activity () { assert(header
.has_extra
); return data
[header
.size
].act
; }
215 uint32_t abstraction () const { assert(header
.has_extra
); return data
[header
.size
].abs
; }
217 Lit
subsumes (const Clause
& other
) const;
218 void strengthen (Lit p
);
222 //=================================================================================================
223 // ClauseAllocator -- a simple class for allocating memory for clauses:
225 const CRef CRef_Undef
= RegionAllocator
<uint32_t>::Ref_Undef
;
226 class ClauseAllocator
228 RegionAllocator
<uint32_t> ra
;
230 static uint32_t clauseWord32Size(int size
, bool has_extra
){
231 return (sizeof(Clause
) + (sizeof(Lit
) * (size
+ (int)has_extra
))) / sizeof(uint32_t); }
234 enum { Unit_Size
= RegionAllocator
<uint32_t>::Unit_Size
};
236 bool extra_clause_field
;
238 ClauseAllocator(uint32_t start_cap
) : ra(start_cap
), extra_clause_field(false){}
239 ClauseAllocator() : extra_clause_field(false){}
241 void moveTo(ClauseAllocator
& to
){
242 to
.extra_clause_field
= extra_clause_field
;
245 CRef
alloc(const vec
<Lit
>& ps
, bool learnt
= false)
247 assert(sizeof(Lit
) == sizeof(uint32_t));
248 assert(sizeof(float) == sizeof(uint32_t));
249 bool use_extra
= learnt
| extra_clause_field
;
250 CRef cid
= ra
.alloc(clauseWord32Size(ps
.size(), use_extra
));
251 new (lea(cid
)) Clause(ps
, use_extra
, learnt
);
256 CRef
alloc(const Clause
& from
)
258 bool use_extra
= from
.learnt() | extra_clause_field
;
259 CRef cid
= ra
.alloc(clauseWord32Size(from
.size(), use_extra
));
260 new (lea(cid
)) Clause(from
, use_extra
);
263 uint32_t size () const { return ra
.size(); }
264 uint32_t wasted () const { return ra
.wasted(); }
266 // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
267 Clause
& operator[](CRef r
) { return (Clause
&)ra
[r
]; }
268 const Clause
& operator[](CRef r
) const { return (Clause
&)ra
[r
]; }
269 Clause
* lea (CRef r
) { return (Clause
*)ra
.lea(r
); }
270 const Clause
* lea (CRef r
) const { return (Clause
*)ra
.lea(r
);; }
271 CRef
ael (const Clause
* t
){ return ra
.ael((uint32_t*)t
); }
275 Clause
& c
= operator[](cid
);
276 ra
.free(clauseWord32Size(c
.size(), c
.has_extra()));
279 void reloc(CRef
& cr
, ClauseAllocator
& to
)
281 Clause
& c
= operator[](cr
);
283 if (c
.reloced()) { cr
= c
.relocation(); return; }
290 //=================================================================================================
291 // Simple iterator classes (for iterating over clauses and top-level assignments):
293 class ClauseIterator
{
294 const ClauseAllocator
& ca
;
297 ClauseIterator(const ClauseAllocator
& _ca
, const CRef
* _crefs
) : ca(_ca
), crefs(_crefs
){}
299 void operator++(){ crefs
++; }
300 const Clause
& operator*() const { return ca
[*crefs
]; }
302 // NOTE: does not compare that references use the same clause-allocator:
303 bool operator==(const ClauseIterator
& ci
) const { return crefs
== ci
.crefs
; }
304 bool operator!=(const ClauseIterator
& ci
) const { return crefs
!= ci
.crefs
; }
308 class TrailIterator
{
311 TrailIterator(const Lit
* _lits
) : lits(_lits
){}
313 void operator++() { lits
++; }
314 Lit
operator*() const { return *lits
; }
316 bool operator==(const TrailIterator
& ti
) const { return lits
== ti
.lits
; }
317 bool operator!=(const TrailIterator
& ti
) const { return lits
!= ti
.lits
; }
321 //=================================================================================================
322 // OccLists -- a class for maintaining occurence lists with lazy deletion:
324 template<class K
, class Vec
, class Deleted
, class MkIndex
= MkIndexDefault
<K
> >
327 IntMap
<K
, Vec
, MkIndex
> occs
;
328 IntMap
<K
, char, MkIndex
> dirty
;
333 OccLists(const Deleted
& d
, MkIndex _index
= MkIndex()) :
338 void init (const K
& idx
){ occs
.reserve(idx
); occs
[idx
].clear(); dirty
.reserve(idx
, 0); }
339 Vec
& operator[](const K
& idx
){ return occs
[idx
]; }
340 Vec
& lookup (const K
& idx
){ if (dirty
[idx
]) clean(idx
); return occs
[idx
]; }
343 void clean (const K
& idx
);
344 void smudge (const K
& idx
){
345 if (dirty
[idx
] == 0){
351 void clear(bool free
= true){
359 template<class K
, class Vec
, class Deleted
, class MkIndex
>
360 void OccLists
<K
,Vec
,Deleted
,MkIndex
>::cleanAll()
362 for (int i
= 0; i
< dirties
.size(); i
++)
363 // Dirties may contain duplicates so check here if a variable is already cleaned:
364 if (dirty
[dirties
[i
]])
370 template<class K
, class Vec
, class Deleted
, class MkIndex
>
371 void OccLists
<K
,Vec
,Deleted
,MkIndex
>::clean(const K
& idx
)
373 Vec
& vec
= occs
[idx
];
375 for (i
= j
= 0; i
< vec
.size(); i
++)
376 if (!deleted(vec
[i
]))
383 //=================================================================================================
384 // CMap -- a class for mapping clauses to values:
391 uint32_t operator()(CRef cr
) const { return (uint32_t)cr
; } };
393 typedef Map
<CRef
, T
, CRefHash
> HashTable
;
398 void clear () { map
.clear(); }
399 int size () const { return map
.elems(); }
402 // Insert/Remove/Test mapping:
403 void insert (CRef cr
, const T
& t
){ map
.insert(cr
, t
); }
404 void growTo (CRef cr
, const T
& t
){ map
.insert(cr
, t
); } // NOTE: for compatibility
405 void remove (CRef cr
) { map
.remove(cr
); }
406 bool has (CRef cr
, T
& t
) { return map
.peek(cr
, t
); }
408 // Vector interface (the clause 'c' must already exist):
409 const T
& operator [] (CRef cr
) const { return map
[cr
]; }
410 T
& operator [] (CRef cr
) { return map
[cr
]; }
412 // Iteration (not transparent at all at the moment):
413 int bucket_count() const { return map
.bucket_count(); }
414 const vec
<typename
HashTable::Pair
>& bucket(int i
) const { return map
.bucket(i
); }
416 // Move contents to other map:
417 void moveTo(CMap
& other
){ map
.moveTo(other
.map
); }
421 printf(" --- size = %d, bucket_count = %d\n", size(), map
.bucket_count()); }
425 /*_________________________________________________________________________________________________
427 | subsumes : (other : const Clause&) -> Lit
430 | Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
431 | by subsumption resolution.
434 | lit_Error - No subsumption or simplification
435 | lit_Undef - Clause subsumes 'other'
436 | p - The literal p can be deleted from 'other'
437 |________________________________________________________________________________________________@*/
438 inline Lit
Clause::subsumes(const Clause
& other
) const
440 //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
441 //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
442 assert(!header
.learnt
); assert(!other
.header
.learnt
);
443 assert(header
.has_extra
); assert(other
.header
.has_extra
);
444 if (other
.header
.size
< header
.size
|| (data
[header
.size
].abs
& ~other
.data
[other
.header
.size
].abs
) != 0)
448 const Lit
* c
= (const Lit
*)(*this);
449 const Lit
* d
= (const Lit
*)other
;
451 for (unsigned i
= 0; i
< header
.size
; i
++) {
452 // search for c[i] or ~c[i]
453 for (unsigned j
= 0; j
< other
.header
.size
; j
++)
456 else if (ret
== lit_Undef
&& c
[i
] == ~d
[j
]){
469 inline void Clause::strengthen(Lit p
)
475 //=================================================================================================