abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Minisat::ClauseAllocator Class Reference

#include <SolverTypes.h>

Inherits Minisat::RegionAllocator< uint32_t >.

Public Types

enum  
 
enum  
 
typedef uint32_t Ref
 

Public Member Functions

 ClauseAllocator (uint32_t start_cap)
 
 ClauseAllocator ()
 
void moveTo (ClauseAllocator &to)
 
template<class Lits >
CRef alloc (const Lits &ps, bool learnt=false)
 
Clauseoperator[] (Ref r)
 
const Clauseoperator[] (Ref r) const
 
Clauselea (Ref r)
 
const Clauselea (Ref r) const
 
Ref ael (const Clause *t)
 
void _free (CRef cid)
 
void reloc (CRef &cr, ClauseAllocator &to)
 
uint32_t size () const
 
uint32_t wasted () const
 
Ref alloc (int size)
 
void _free (int size)
 
Ref ael (const uint32_t *t)
 
void moveTo (RegionAllocator &to)
 

Data Fields

bool extra_clause_field
 

Static Private Member Functions

static int clauseWord32Size (int size, bool has_extra)
 

Detailed Description

Definition at line 194 of file SolverTypes.h.

Member Typedef Documentation

typedef uint32_t Minisat::RegionAllocator< uint32_t >::Ref
inherited

Definition at line 44 of file Alloc.h.

Member Enumeration Documentation

anonymous enum
inherited

Definition at line 45 of file Alloc.h.

anonymous enum
inherited

Definition at line 46 of file Alloc.h.

Constructor & Destructor Documentation

Minisat::ClauseAllocator::ClauseAllocator ( uint32_t  start_cap)
inline

Definition at line 201 of file SolverTypes.h.

201 : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
Minisat::ClauseAllocator::ClauseAllocator ( )
inline

Definition at line 202 of file SolverTypes.h.

202 : extra_clause_field(false){}

Member Function Documentation

void Minisat::RegionAllocator< uint32_t >::_free ( int  size)
inlineinherited

Definition at line 60 of file Alloc.h.

void Minisat::ClauseAllocator::_free ( CRef  cid)
inline

Definition at line 228 of file SolverTypes.h.

229  {
230  Clause& c = operator[](cid);
231  RegionAllocator<uint32_t>::_free(clauseWord32Size(c.size(), c.has_extra()));
232  }
Clause & operator[](Ref r)
Definition: SolverTypes.h:222
void _free(int size)
Definition: Alloc.h:60
static int clauseWord32Size(int size, bool has_extra)
Definition: SolverTypes.h:196
Ref Minisat::RegionAllocator< uint32_t >::ael ( const uint32_t *  t)
inlineinherited

Definition at line 68 of file Alloc.h.

68  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
69  return (Ref)(t - &memory[0]); }
#define assert(ex)
Definition: util_old.h:213
Ref Minisat::ClauseAllocator::ael ( const Clause t)
inline

Definition at line 226 of file SolverTypes.h.

226 { return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
Ref ael(const T *t)
Definition: Alloc.h:68
Ref Minisat::RegionAllocator< uint32_t >::alloc ( int  size)
inherited
template<class Lits >
CRef Minisat::ClauseAllocator::alloc ( const Lits &  ps,
bool  learnt = false 
)
inline

Definition at line 209 of file SolverTypes.h.

210  {
211  assert(sizeof(Lit) == sizeof(uint32_t));
212  assert(sizeof(float) == sizeof(uint32_t));
213  bool use_extra = learnt | extra_clause_field;
214 
215  CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
216  new (lea(cid)) Clause(ps, use_extra, learnt);
217 
218  return cid;
219  }
RegionAllocator< uint32_t >::Ref CRef
Definition: SolverTypes.h:120
Ref alloc(int size)
Definition: Alloc.h:111
Clause * lea(Ref r)
Definition: SolverTypes.h:224
static int clauseWord32Size(int size, bool has_extra)
Definition: SolverTypes.h:196
#define assert(ex)
Definition: util_old.h:213
static int Minisat::ClauseAllocator::clauseWord32Size ( int  size,
bool  has_extra 
)
inlinestaticprivate

Definition at line 196 of file SolverTypes.h.

196  {
197  return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
Clause* Minisat::ClauseAllocator::lea ( Ref  r)
inline

Definition at line 224 of file SolverTypes.h.

224 { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
T * lea(Ref r)
Definition: Alloc.h:66
const Clause* Minisat::ClauseAllocator::lea ( Ref  r) const
inline

Definition at line 225 of file SolverTypes.h.

225 { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
T * lea(Ref r)
Definition: Alloc.h:66
void Minisat::RegionAllocator< uint32_t >::moveTo ( RegionAllocator< uint32_t > &  to)
inlineinherited

Definition at line 71 of file Alloc.h.

71  {
72  if (to.memory != NULL) ::free(to.memory);
73  to.memory = memory;
74  to.sz = sz;
75  to.cap = cap;
76  to.wasted_ = wasted_;
77 
78  memory = NULL;
79  sz = cap = wasted_ = 0;
80  }
VOID_HACK free()
void Minisat::ClauseAllocator::moveTo ( ClauseAllocator to)
inline

Definition at line 204 of file SolverTypes.h.

204  {
205  to.extra_clause_field = extra_clause_field;
void moveTo(RegionAllocator &to)
Definition: Alloc.h:71
Clause& Minisat::ClauseAllocator::operator[] ( Ref  r)
inline

Definition at line 222 of file SolverTypes.h.

222 { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
T & operator[](Ref r)
Definition: Alloc.h:63
const Clause& Minisat::ClauseAllocator::operator[] ( Ref  r) const
inline

Definition at line 223 of file SolverTypes.h.

223 { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
T & operator[](Ref r)
Definition: Alloc.h:63
void Minisat::ClauseAllocator::reloc ( CRef cr,
ClauseAllocator to 
)
inline

Definition at line 234 of file SolverTypes.h.

235  {
236  Clause& c = operator[](cr);
237 
238  if (c.reloced()) { cr = c.relocation(); return; }
239 
240  cr = to.alloc(c, c.learnt());
241  c.relocate(cr);
242 
243  // Copy extra data-fields:
244  // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
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();
248  }
Clause & operator[](Ref r)
Definition: SolverTypes.h:222
uint32_t Minisat::RegionAllocator< uint32_t >::size ( void  ) const
inlineinherited

Definition at line 56 of file Alloc.h.

56 { return sz; }
uint32_t Minisat::RegionAllocator< uint32_t >::wasted ( ) const
inlineinherited

Definition at line 57 of file Alloc.h.

57 { return wasted_; }

Field Documentation

bool Minisat::ClauseAllocator::extra_clause_field

Definition at line 199 of file SolverTypes.h.


The documentation for this class was generated from the following file: