#include <SolverTypes.h>
Inherits Minisat::RegionAllocator< uint32_t >.
|
enum | |
|
enum | |
|
typedef uint32_t | Ref |
|
Definition at line 194 of file SolverTypes.h.
Minisat::ClauseAllocator::ClauseAllocator |
( |
uint32_t |
start_cap | ) |
|
|
inline |
Minisat::ClauseAllocator::ClauseAllocator |
( |
| ) |
|
|
inline |
void Minisat::ClauseAllocator::_free |
( |
CRef |
cid | ) |
|
|
inline |
Definition at line 228 of file SolverTypes.h.
Clause & operator[](Ref r)
static int clauseWord32Size(int size, bool has_extra)
Definition at line 209 of file SolverTypes.h.
211 assert(
sizeof(Lit) ==
sizeof(uint32_t));
212 assert(
sizeof(
float) ==
sizeof(uint32_t));
216 new (
lea(cid)) Clause(ps, use_extra, learnt);
RegionAllocator< uint32_t >::Ref CRef
static int clauseWord32Size(int size, bool has_extra)
static int Minisat::ClauseAllocator::clauseWord32Size |
( |
int |
size, |
|
|
bool |
has_extra |
|
) |
| |
|
inlinestaticprivate |
Definition at line 196 of file SolverTypes.h.
197 return (
sizeof(Clause) + (
sizeof(Lit) * (
size + (
int)has_extra))) /
sizeof(uint32_t); }
Clause* Minisat::ClauseAllocator::lea |
( |
Ref |
r | ) |
|
|
inline |
Definition at line 71 of file Alloc.h.
72 if (to.memory != NULL)
::free(to.memory);
Clause& Minisat::ClauseAllocator::operator[] |
( |
Ref |
r | ) |
|
|
inline |
Definition at line 234 of file SolverTypes.h.
238 if (c.reloced()) { cr = c.relocation();
return; }
240 cr = to.alloc(c, c.learnt());
245 to[cr].mark(c.mark());
246 if (to[cr].learnt()) to[cr].activity() = c.activity();
247 else if (to[cr].has_extra()) to[cr].calcAbstraction();
Clause & operator[](Ref r)
bool Minisat::ClauseAllocator::extra_clause_field |
The documentation for this class was generated from the following file: