Minisat::ClauseAllocator Class Reference

#include <SolverTypes.h>

Inheritance diagram for Minisat::ClauseAllocator:

Collaboration diagram for Minisat::ClauseAllocator:

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, unsigned _type)
Clause &	operator[] (Ref r)
const Clause &	operator[] (Ref r) const
Clause *	lea (Ref r)
const Clause *	lea (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

Private Member Functions
void	capacity (uint32_t min_cap)

Static Private Member Functions
static int	clauseWord32Size (int size, bool has_extra)

Private Attributes
uint32_t *	memory
uint32_t	sz
uint32_t	cap
uint32_t	wasted_

Detailed Description

Definition at line 249 of file SolverTypes.h.

Member Typedef Documentation

Ref

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

inherited

Definition at line 43 of file Alloc.h.

Member Enumeration Documentation

anonymous enum

anonymous enum

inherited

Definition at line 45 of file Alloc.h.

anonymous enum

anonymous enum

inherited

Definition at line 47 of file Alloc.h.

Constructor & Destructor Documentation

ClauseAllocator() [1/2]

Minisat::ClauseAllocator::ClauseAllocator ( uint32_t  start_cap )

inline

Definition at line 256 of file SolverTypes.h.

ClauseAllocator() [2/2]

Minisat::ClauseAllocator::ClauseAllocator ( )

inline

Definition at line 257 of file SolverTypes.h.

Member Function Documentation

ael() [1/2]

Ref Minisat::ClauseAllocator::ael ( const Clause *  t )

inline

Definition at line 281 of file SolverTypes.h.

Here is the call graph for this function:

ael() [2/2]

Ref Minisat::RegionAllocator< uint32_t >::ael ( const uint32_t *  t )

inlineinherited

Definition at line 106 of file Alloc.h.

alloc() [1/2]

template<class Lits >

CRef Minisat::ClauseAllocator::alloc ( const Lits &  ps, unsigned  _type  )

inline

Definition at line 264 of file SolverTypes.h.

Here is the call graph for this function:

Here is the caller graph for this function:

alloc() [2/2]

RegionAllocator< uint32_t >::Ref Minisat::RegionAllocator< uint32_t >::alloc ( int  size )

inherited

Definition at line 73 of file Alloc.h.

capacity()

void Minisat::RegionAllocator< uint32_t >::capacity ( uint32_t  min_cap )

privateinherited

Definition at line 39 of file Alloc.h.

clauseWord32Size()

static int Minisat::ClauseAllocator::clauseWord32Size ( int  size, bool  has_extra  )

inlinestaticprivate

Definition at line 251 of file SolverTypes.h.

Here is the call graph for this function:

Here is the caller graph for this function:

free() [1/2]

void Minisat::ClauseAllocator::free ( CRef  cid )

inline

Definition at line 283 of file SolverTypes.h.

Here is the call graph for this function:

free() [2/2]

void Minisat::RegionAllocator< uint32_t >::free ( int  size )

inlineinherited

Definition at line 75 of file Alloc.h.

lea() [1/2]

Clause* Minisat::ClauseAllocator::lea ( Ref  r )

inline

Definition at line 279 of file SolverTypes.h.

Here is the call graph for this function:

Here is the caller graph for this function:

lea() [2/2]

const Clause* Minisat::ClauseAllocator::lea ( Ref  r ) const

inline

Definition at line 280 of file SolverTypes.h.

Here is the call graph for this function:

moveTo() [1/2]

void Minisat::ClauseAllocator::moveTo ( ClauseAllocator &  to )

inline

Definition at line 259 of file SolverTypes.h.

Here is the call graph for this function:

moveTo() [2/2]

void Minisat::RegionAllocator< uint32_t >::moveTo ( RegionAllocator< uint32_t > &  to )

inlineinherited

Definition at line 112 of file Alloc.h.

operator[]() [1/2]

Clause& Minisat::ClauseAllocator::operator[] ( Ref  r )

inline

Definition at line 277 of file SolverTypes.h.

Here is the call graph for this function:

Here is the caller graph for this function:

operator[]() [2/2]

const Clause& Minisat::ClauseAllocator::operator[] ( Ref  r ) const

inline

Definition at line 278 of file SolverTypes.h.

Here is the call graph for this function:

reloc()

void Minisat::ClauseAllocator::reloc ( CRef &  cr, ClauseAllocator &  to  )

inline

Definition at line 289 of file SolverTypes.h.

Here is the call graph for this function:

Here is the caller graph for this function:

size()

uint32_t Minisat::RegionAllocator< uint32_t >::size ( void  ) const

inlineinherited

Definition at line 63 of file Alloc.h.

wasted()

uint32_t Minisat::RegionAllocator< uint32_t >::wasted ( ) const

inlineinherited

Definition at line 68 of file Alloc.h.

Field Documentation

cap

uint32_t Minisat::RegionAllocator< uint32_t >::cap

privateinherited

Definition at line 36 of file Alloc.h.

extra_clause_field

bool Minisat::ClauseAllocator::extra_clause_field

Definition at line 254 of file SolverTypes.h.

memory

uint32_t * Minisat::RegionAllocator< uint32_t >::memory

privateinherited

Definition at line 34 of file Alloc.h.

sz

uint32_t Minisat::RegionAllocator< uint32_t >::sz

privateinherited

Definition at line 35 of file Alloc.h.

wasted_

uint32_t Minisat::RegionAllocator< uint32_t >::wasted_

privateinherited

Definition at line 37 of file Alloc.h.

---

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

• smtrat-modules/SATModule/SolverTypes.h