Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

SolverTypes.h
Go to the documentation of this file.
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 #pragma once
22 
23 #include <assert.h>
24 
30 
31 #pragma GCC visibility push(default)
32 namespace Minisat {
33 namespace Internal {
34 
35 //=================================================================================================
36 // Variables, literals, lifted booleans, clauses:
37 
38 
39 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
40 // so that they can be used as array indices.
41 
42 using Var = int;
43 #define var_Undef (-1)
44 
45 
46 struct Lit {
47  int x;
48 
49  // Use this as a constructor:
50  friend Lit mkLit(Var var, bool sign);
51 
52  bool operator == (Lit p) const { return x == p.x; }
53  bool operator != (Lit p) const { return x != p.x; }
54  bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
55 };
56 
57 
58 inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
59 inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
60 inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
61 inline bool sign (Lit p) { return p.x & 1; }
62 inline int var (Lit p) { return p.x >> 1; }
63 
64 // Mapping Literals to and from compact integers suitable for array indexing:
65 inline int toInt (Var v) { return v; }
66 inline int toInt (Lit p) { return p.x; }
67 inline Lit toLit (int i) { Lit p; p.x = i; return p; }
68 
69 #if 0
70 const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
71 const Lit lit_Error = mkLit(var_Undef, true ); // }
72 #endif
73 
74 const Lit lit_Undef = { -2 }; // }- Useful special constants.
75 const Lit lit_Error = { -1 }; // }
76 
77 
78 //=================================================================================================
79 // Lifted booleans:
80 //
81 // NOTE: this implementation is optimized for the case when comparisons between values are mostly
82 // between one variable and one constant. Some care had to be taken to make sure that gcc
83 // does enough constant propagation to produce sensible code, and this appears to be somewhat
84 // fragile unfortunately.
85 
86 #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
87 #define l_False (lbool((uint8_t)1))
88 #define l_Undef (lbool((uint8_t)2))
89 #define l_Timeout (lbool((uint8_t)9)) // HEDTKE
90 
91 class lbool {
92  uint8_t value;
93 
94 public:
95  explicit lbool(uint8_t v) : value(v) { }
96 
97  lbool() : value(0) { }
98  explicit lbool(bool x) : value(!x) { }
99 
100 #if 0
101  bool operator == (lbool b) const { return ( (b.value & 2) & (value & 2) ) | (!(b.value & 2) & (value == b.value)); }
102 #endif
103  bool operator == (lbool b) const {
104  return (( (b.value & 2) & (value & 2) ) | (((b.value & 2) == 0) & (value == b.value))) != 0;
105  }
106 
107  bool operator != (lbool b) const { return !(*this == b); }
108  lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
109 
111  uint8_t sel = (this->value << 1) | (b.value << 3);
112  uint8_t v = (0xF7F755F4 >> sel) & 3;
113  return lbool(v); }
114 
116  uint8_t sel = (this->value << 1) | (b.value << 3);
117  uint8_t v = (0xFCFCF400 >> sel) & 3;
118  return lbool(v); }
119 
120  friend int toInt (lbool l);
121  friend lbool toLbool(int v);
122 };
123 inline int toInt (lbool l) { return l.value; }
124 inline lbool toLbool(int v) { return lbool((uint8_t)v); }
125 
126 //=================================================================================================
127 // Clause -- a simple class for representing a clause:
128 
129 class Clause;
131 
132 #ifdef _MSC_VER
133 #pragma warning ( push )
134 #pragma warning ( disable : 4200 )
135 #endif
136 
137 class Clause {
138  struct {
139  unsigned mark : 2;
140  unsigned learnt : 1;
141  unsigned has_extra : 1;
142  unsigned reloced : 1;
143  unsigned size : 27; } header;
144  union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
145 
146  friend class ClauseAllocator;
147 
148  // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
149  template<class V>
150  Clause(const V& ps, bool use_extra, bool learnt) {
151  header.mark = 0;
152  header.learnt = learnt;
153  header.has_extra = use_extra;
154  header.reloced = 0;
155  header.size = ps.size();
156 
157  for (int i = 0; i < ps.size(); i++)
158  data[i].lit = ps[i];
159 
160  if (header.has_extra){
161  if (header.learnt)
162  data[header.size].act = 0;
163  else
164  calcAbstraction(); }
165  }
166 
167 public:
169  assert(header.has_extra);
170  uint32_t abstraction = 0;
171  for (int i = 0; i < size(); i++)
172  abstraction |= 1 << (var(data[i].lit) & 31);
173  data[header.size].abs = abstraction; }
174 
175 
176  int size () const { return header.size; }
177  void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
178  void pop () { shrink(1); }
179  bool learnt () const { return header.learnt; }
180  bool has_extra () const { return header.has_extra; }
181  uint32_t mark () const { return header.mark; }
182  void mark (uint32_t m) { header.mark = m; }
183  const Lit& last () const { return data[header.size-1].lit; }
184 
185  bool reloced () const { return header.reloced; }
186  CRef relocation () const { return data[0].rel; }
187  void relocate (CRef c) { header.reloced = 1; data[0].rel = c; }
188 
189  // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
190  // subsumption operations to behave correctly.
191  Lit& operator [] (int i) { return data[i].lit; }
192  Lit operator [] (int i) const { return data[i].lit; }
193  operator const Lit* (void) const { return reinterpret_cast<const Lit*>(data); }
194 
195  float& activity () { assert(header.has_extra); return data[header.size].act; }
196  uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
197 
198  Lit subsumes (const Clause& other) const;
199  void strengthen (Lit p);
200 };
201 
202 #ifdef _MSC_VER
203 #pragma warning ( pop )
204 #endif
205 
206 
207 //=================================================================================================
208 // ClauseAllocator -- a simple class for allocating memory for clauses:
209 
210 
212 class ClauseAllocator : public RegionAllocator<uint32_t>
213 {
214  static int clauseWord32Size(int size, bool has_extra){
215  return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
216  public:
218 
219  ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
221 
225 
226  template<class Lits>
227  CRef alloc(const Lits& ps, bool learnt = false)
228  {
229  assert(sizeof(Lit) == sizeof(uint32_t));
230  assert(sizeof(float) == sizeof(uint32_t));
231  bool use_extra = learnt | extra_clause_field;
232 
233  CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
234  new (lea(cid)) Clause(ps, use_extra, learnt);
235 
236  return cid;
237  }
238 
239  // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
242  Clause* lea (Ref r) { return reinterpret_cast<Clause*>(RegionAllocator<uint32_t>::lea(r)); }
243  const Clause* lea(Ref r) const { return reinterpret_cast<const Clause*>(RegionAllocator<uint32_t>::lea(r)); }
244  Ref ael (const Clause* t) { return RegionAllocator<uint32_t>::ael((const uint32_t*)t); }
245 
246  void free(CRef cid)
247  {
248  Clause& c = operator[](cid);
250  }
251 
252  void reloc(CRef& cr, ClauseAllocator& to)
253  {
254  Clause& c = operator[](cr);
255 
256  if (c.reloced()) { cr = c.relocation(); return; }
257 
258  cr = to.alloc(c, c.learnt());
259  c.relocate(cr);
260 
261  // Copy extra data-fields:
262  // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
263  to[cr].mark(c.mark());
264  if (to[cr].learnt()) to[cr].activity() = c.activity();
265  else if (to[cr].has_extra()) to[cr].calcAbstraction();
266  }
267 };
268 
269 
270 //=================================================================================================
271 // OccLists -- a class for maintaining occurence lists with lazy deletion:
272 
273 template<class Idx, class Vec, class Deleted>
274 class OccLists
275 {
279  Deleted deleted;
280 
281  public:
282  OccLists(const Deleted& d) : deleted(d) {}
283 
284  void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
285 #if 0
286  Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
287 #endif
288  Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
289  Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
290 
291  void cleanAll ();
292  void clean (const Idx& idx);
293  void smudge (const Idx& idx){
294  if (dirty[toInt(idx)] == 0){
295  dirty[toInt(idx)] = 1;
296  dirties.push(idx);
297  }
298  }
299 
300  void clear(bool free = true){
301  occs .clear(free);
302  dirty .clear(free);
303  dirties.clear(free);
304  }
305 };
306 
307 
308 template<class Idx, class Vec, class Deleted>
310 {
311  for (int i = 0; i < dirties.size(); i++)
312  // Dirties may contain duplicates so check here if a variable is already cleaned:
313  if (dirty[toInt(dirties[i])])
314  clean(dirties[i]);
315  dirties.clear();
316 }
317 
318 
319 template<class Idx, class Vec, class Deleted>
321 {
322  Vec& vec = occs[toInt(idx)];
323  int i, j;
324  for (i = j = 0; i < vec.size(); i++)
325  if (!deleted(vec[i]))
326  vec[j++] = vec[i];
327  vec.shrink(i - j);
328  dirty[toInt(idx)] = 0;
329 }
330 
331 
332 //=================================================================================================
333 // CMap -- a class for mapping clauses to values:
334 
335 
336 template<class T>
337 class CMap
338 {
339  struct CRefHash {
340  uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
341 
344 
345  public:
346  // Size-operations:
347  void clear () { map.clear(); }
348  int size () const { return map.elems(); }
349 
350 
351  // Insert/Remove/Test mapping:
352  void insert (CRef cr, const T& t){ map.insert(cr, t); }
353  void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
354  void remove (CRef cr) { map.remove(cr); }
355  bool has (CRef cr, T& t) { return map.peek(cr, t); }
356 
357  // Vector interface (the clause 'c' must already exist):
358  const T& operator [] (CRef cr) const { return map[cr]; }
359  T& operator [] (CRef cr) { return map[cr]; }
360 
361  // Iteration (not transparent at all at the moment):
362  int bucket_count() const { return map.bucket_count(); }
363  const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
364 
365  // Move contents to other map:
366  void moveTo(CMap& other){ map.moveTo(other.map); }
367 
368  // TMP debug:
369  void debug(){
370  printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
371 };
372 
373 
374 /*_________________________________________________________________________________________________
375 |
376 | subsumes : (other : const Clause&) -> Lit
377 |
378 | Description:
379 | Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
380 | by subsumption resolution.
381 |
382 | Result:
383 | lit_Error - No subsumption or simplification
384 | lit_Undef - Clause subsumes 'other'
385 | p - The literal p can be deleted from 'other'
386 |________________________________________________________________________________________________@*/
387 inline Lit Clause::subsumes(const Clause& other) const
388 {
389 #if 0
390  if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
391  if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
392 #endif
393  assert(!header.learnt); assert(!other.header.learnt);
394  assert(header.has_extra); assert(other.header.has_extra);
395  if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
396  return lit_Error;
397 
398  Lit ret = lit_Undef;
399  const Lit* c = static_cast<const Lit*>(*this);
400  const Lit* d = static_cast<const Lit*>(other);
401 
402  for (unsigned i = 0; i < header.size; i++) {
403  // search for c[i] or ~c[i]
404  for (unsigned j = 0; j < other.header.size; j++)
405  if (c[i] == d[j])
406  goto ok;
407  else if (ret == lit_Undef && c[i] == ~d[j]){
408  ret = c[i];
409  goto ok;
410  }
411 
412  // did not find it
413  return lit_Error;
414  ok:;
415  }
416 
417  return ret;
418 }
419 
420 inline void Clause::strengthen(Lit p)
421 {
422  remove(*this, p);
423  calcAbstraction();
424 }
425 
426 //=================================================================================================
427 } // namespace Internal
428 } // namespace Minisat
429 #pragma GCC visibility pop
Minisat::Internal::toLit
Lit toLit(int i)
Definition: SolverTypes.h:67
Minisat::Internal::ClauseAllocator::reloc
void reloc(CRef &cr, ClauseAllocator &to)
Definition: SolverTypes.h:252
Minisat::Internal::OccLists::deleted
Deleted deleted
Definition: SolverTypes.h:279
Minisat::Internal::lbool::operator==
bool operator==(lbool b) const
Definition: SolverTypes.h:103
Minisat::Internal::OccLists::dirties
vec< Idx > dirties
Definition: SolverTypes.h:278
Minisat::Internal::lbool::lbool
lbool(bool x)
Definition: SolverTypes.h:98
Minisat::Internal::CMap::CRefHash
Definition: SolverTypes.h:339
Vec.h
Minisat::Internal::Map::elems
int elems() const
Definition: Map.h:174
Minisat::Internal::Lit::operator==
bool operator==(Lit p) const
Definition: SolverTypes.h:52
Minisat::Internal::RegionAllocator< uint32_t >::Ref
uint32_t Ref
Definition: Alloc.h:44
Minisat::Internal::OccLists
Definition: SolverTypes.h:274
Minisat::Internal::ClauseAllocator::clauseWord32Size
static int clauseWord32Size(int size, bool has_extra)
Definition: SolverTypes.h:214
Minisat::Internal::lbool::operator^
lbool operator^(bool b) const
Definition: SolverTypes.h:108
Minisat::Internal::RegionAllocator< uint32_t >::size
uint32_t size() const
Definition: Alloc.h:58
Minisat::Internal::Clause::Clause
Clause(const V &ps, bool use_extra, bool learnt)
Definition: SolverTypes.h:150
Minisat::Internal::CMap::moveTo
void moveTo(CMap &other)
Definition: SolverTypes.h:366
Minisat::Internal::operator^
Lit operator^(Lit p, bool b)
Definition: SolverTypes.h:60
Minisat::Internal::Clause::rel
CRef rel
Definition: SolverTypes.h:144
Minisat::Internal::Clause::header
struct Minisat::Internal::Clause::@7 header
Alloc.h
Minisat::Internal::vec::shrink
void shrink(int nelems)
Definition: Vec.h:65
Minisat::Internal::ClauseAllocator
Definition: SolverTypes.h:212
Minisat::Internal::Lit::operator<
bool operator<(Lit p) const
Definition: SolverTypes.h:54
Minisat::Internal::Clause::size
int size() const
Definition: SolverTypes.h:176
Minisat::Internal::Clause::pop
void pop()
Definition: SolverTypes.h:178
Minisat::Internal::Clause::last
const Lit & last() const
Definition: SolverTypes.h:183
Minisat::Internal::CMap::debug
void debug()
Definition: SolverTypes.h:369
Minisat::Internal::Lit::operator!=
bool operator!=(Lit p) const
Definition: SolverTypes.h:53
Minisat::Internal::Clause::mark
void mark(uint32_t m)
Definition: SolverTypes.h:182
Minisat::Internal::Clause::mark
uint32_t mark() const
Definition: SolverTypes.h:181
Minisat::Internal::Map< CRef, T, CRefHash >
Minisat::Internal::Clause::abstraction
uint32_t abstraction() const
Definition: SolverTypes.h:196
Minisat::Internal::lbool::operator||
lbool operator||(lbool b) const
Definition: SolverTypes.h:115
Minisat::Internal::RegionAllocator::alloc
Ref alloc(int size)
Definition: Alloc.h:118
Minisat::Internal::lbool::operator!=
bool operator!=(lbool b) const
Definition: SolverTypes.h:107
Minisat::Internal::Clause::reloced
bool reloced() const
Definition: SolverTypes.h:185
Minisat::Internal::ClauseAllocator::ClauseAllocator
ClauseAllocator()
Definition: SolverTypes.h:220
Minisat::Internal::Clause::data
union Minisat::Internal::Clause::@8 data[0]
Minisat::Internal::CMap::growTo
void growTo(CRef cr, const T &t)
Definition: SolverTypes.h:353
Minisat::Internal::lbool::lbool
lbool()
Definition: SolverTypes.h:97
Minisat::Internal::Map::moveTo
void moveTo(Map &other)
Definition: Map.h:178
Minisat::Internal::CMap::operator[]
const T & operator[](CRef cr) const
Definition: SolverTypes.h:358
Minisat::Internal::Map::peek
bool peek(const K &k, D &d) const
Definition: Map.h:137
Minisat::Internal::OccLists::occs
vec< Vec > occs
Definition: SolverTypes.h:276
Minisat::Internal::OccLists::OccLists
OccLists(const Deleted &d)
Definition: SolverTypes.h:282
var_Undef
#define var_Undef
Definition: SolverTypes.h:43
Minisat::Internal::lit_Undef
const Lit lit_Undef
Definition: SolverTypes.h:74
Minisat::Internal::lbool::operator&&
lbool operator&&(lbool b) const
Definition: SolverTypes.h:110
Minisat::Internal::Map::bucket
const vec< Pair > & bucket(int i) const
Definition: Map.h:190
Minisat::Internal::OccLists::clear
void clear(bool free=true)
Definition: SolverTypes.h:300
Minisat::Internal::CMap::insert
void insert(CRef cr, const T &t)
Definition: SolverTypes.h:352
Minisat::Internal::CMap::CRefHash::operator()
uint32_t operator()(CRef cr) const
Definition: SolverTypes.h:340
Minisat::Internal::CMap::size
int size() const
Definition: SolverTypes.h:348
IntTypes.h
Minisat::Internal::lbool::lbool
lbool(uint8_t v)
Definition: SolverTypes.h:95
r
int r[]
Definition: hierarchical-ranking.cpp:13
Minisat::Internal::Clause::abs
uint32_t abs
Definition: SolverTypes.h:144
Minisat::Internal::Clause::operator[]
Lit & operator[](int i)
Definition: SolverTypes.h:191
Minisat::Internal::vec::size
int size(void) const
Definition: Vec.h:64
Minisat::Internal::ClauseAllocator::operator[]
Clause & operator[](Ref r)
Definition: SolverTypes.h:240
Minisat::Internal::operator~
Lit operator~(Lit p)
Definition: SolverTypes.h:59
Minisat::Internal::RegionAllocator::free
void free(int size)
Definition: Alloc.h:62
Minisat::Internal::Lit
Definition: SolverTypes.h:46
Minisat::Internal::toInt
int toInt(Var v)
Definition: SolverTypes.h:65
Minisat::Internal::OccLists::dirty
vec< char > dirty
Definition: SolverTypes.h:277
Minisat::Internal::Clause::has_extra
bool has_extra() const
Definition: SolverTypes.h:180
Minisat::Internal::vec::push
void push(void)
Definition: Vec.h:74
Minisat::Internal::Clause::size
unsigned size
Definition: SolverTypes.h:143
Minisat::Internal::Clause::learnt
unsigned learnt
Definition: SolverTypes.h:140
Minisat::Internal::RegionAllocator::lea
T * lea(Ref r)
Definition: Alloc.h:68
Minisat::Internal::OccLists::lookup
Vec & lookup(const Idx &idx)
Definition: SolverTypes.h:289
Minisat::Internal::ClauseAllocator::alloc
CRef alloc(const Lits &ps, bool learnt=false)
Definition: SolverTypes.h:227
Minisat::Internal::vec::growTo
void growTo(int size)
Definition: Vec.h:114
Minisat::Internal::Clause::mark
unsigned mark
Definition: SolverTypes.h:139
Minisat::Internal::Clause::calcAbstraction
void calcAbstraction()
Definition: SolverTypes.h:168
Minisat::Internal::CMap
Definition: SolverTypes.h:337
Minisat::Internal::Clause::relocation
CRef relocation() const
Definition: SolverTypes.h:186
Minisat::Internal::Clause::activity
float & activity()
Definition: SolverTypes.h:195
Minisat::Internal::ClauseAllocator::lea
const Clause * lea(Ref r) const
Definition: SolverTypes.h:243
Minisat::Internal::Clause::has_extra
unsigned has_extra
Definition: SolverTypes.h:141
Minisat::Internal::lbool
Definition: SolverTypes.h:91
Minisat::Internal::Clause::shrink
void shrink(int i)
Definition: SolverTypes.h:177
Minisat::Internal::lbool::value
uint8_t value
Definition: SolverTypes.h:92
Minisat::Internal::Clause::strengthen
void strengthen(Lit p)
Definition: SolverTypes.h:420
Minisat
Definition: Minisat.h:55
Minisat::Internal::ClauseAllocator::lea
Clause * lea(Ref r)
Definition: SolverTypes.h:242
Minisat::Internal::toLbool
lbool toLbool(int v)
Definition: SolverTypes.h:124
Minisat::Internal::lbool::toInt
friend int toInt(lbool l)
Definition: SolverTypes.h:123
Minisat::Internal::Clause::learnt
bool learnt() const
Definition: SolverTypes.h:179
Minisat::Internal::Clause
Definition: SolverTypes.h:137
Minisat::Internal::lit_Error
const Lit lit_Error
Definition: SolverTypes.h:75
Minisat::Internal::sign
bool sign(Lit p)
Definition: SolverTypes.h:61
Minisat::Internal::OccLists::smudge
void smudge(const Idx &idx)
Definition: SolverTypes.h:293
Minisat::Internal::OccLists::operator[]
Vec & operator[](const Idx &idx)
Definition: SolverTypes.h:288
Minisat::Internal::Map::insert
void insert(const K &k, const D &d)
Definition: Map.h:136
Alg.h
Minisat::Internal::Map::remove
void remove(const K &k)
Definition: Map.h:157
Minisat::Internal::CRef_Undef
const CRef CRef_Undef
Definition: SolverTypes.h:211
Minisat::Internal::ClauseAllocator::operator[]
const Clause & operator[](Ref r) const
Definition: SolverTypes.h:241
Minisat::Internal::vec< Vec >
Minisat::Internal::CMap::map
HashTable map
Definition: SolverTypes.h:343
Minisat::Internal::Map::bucket_count
int bucket_count() const
Definition: Map.h:175
Minisat::Clause
Represents a simple class for clause storage.
Definition: Minisat.h:66
Minisat::Internal::Lit::x
int x
Definition: SolverTypes.h:47
Minisat::Internal::CMap::bucket
const vec< typename HashTable::Pair > & bucket(int i) const
Definition: SolverTypes.h:363
Minisat::Internal::RegionAllocator::operator[]
T & operator[](Ref r)
Definition: Alloc.h:65
Minisat::Internal::CMap::has
bool has(CRef cr, T &t)
Definition: SolverTypes.h:355
Minisat::Internal::RegionAllocator::ael
Ref ael(const T *t)
Definition: Alloc.h:71
Minisat::Internal::CMap::clear
void clear()
Definition: SolverTypes.h:347
Minisat::Internal::ClauseAllocator::moveTo
void moveTo(ClauseAllocator &to)
Definition: SolverTypes.h:222
Minisat::Internal::vec::clear
void clear(bool dealloc=false)
Definition: Vec.h:122
Minisat::Internal::mkLit
Lit mkLit(Var var, bool sign=false)
Definition: SolverTypes.h:58
Minisat::Internal::OccLists::clean
void clean(const Idx &idx)
Definition: SolverTypes.h:320
Minisat::Internal::ClauseAllocator::ClauseAllocator
ClauseAllocator(uint32_t start_cap)
Definition: SolverTypes.h:219
Minisat::Internal::Clause::reloced
unsigned reloced
Definition: SolverTypes.h:142
Minisat::Internal::var
int var(Lit p)
Definition: SolverTypes.h:62
Minisat::Internal::CMap::bucket_count
int bucket_count() const
Definition: SolverTypes.h:362
Minisat::Internal::ClauseAllocator::free
void free(CRef cid)
Definition: SolverTypes.h:246
Map.h
Minisat::Internal::OccLists::cleanAll
void cleanAll()
Definition: SolverTypes.h:309
Minisat::Internal::lbool::toLbool
friend lbool toLbool(int v)
Definition: SolverTypes.h:124
Minisat::Internal::RegionAllocator
Definition: Alloc.h:34
Minisat::Internal::Map::clear
void clear()
Definition: Map.h:168
Minisat::Internal::RegionAllocator::moveTo
void moveTo(RegionAllocator &to)
Definition: Alloc.h:77
Minisat::Internal::Clause::lit
Lit lit
Definition: SolverTypes.h:144
Minisat::Internal::Lit::mkLit
friend Lit mkLit(Var var, bool sign)
Definition: SolverTypes.h:58
Minisat::Internal::CMap::remove
void remove(CRef cr)
Definition: SolverTypes.h:354
Minisat::Internal::Var
int Var
Definition: SolverTypes.h:42
Minisat::Internal::CRef
RegionAllocator< uint32_t >::Ref CRef
Definition: SolverTypes.h:130
Minisat::Internal::remove
static void remove(V &ts, const T &t)
Definition: Alg.h:37
Minisat::Internal::Clause::subsumes
Lit subsumes(const Clause &other) const
Definition: SolverTypes.h:387
Minisat::Internal::OccLists::init
void init(const Idx &idx)
Definition: SolverTypes.h:284
Minisat::Internal::ClauseAllocator::ael
Ref ael(const Clause *t)
Definition: SolverTypes.h:244
Minisat::Internal::Clause::relocate
void relocate(CRef c)
Definition: SolverTypes.h:187
Minisat::Internal::ClauseAllocator::extra_clause_field
bool extra_clause_field
Definition: SolverTypes.h:217
Minisat::Internal::Clause::act
float act
Definition: SolverTypes.h:144