Minisat::ClauseAllocator Class Reference

#include <SolverTypes.h>

Collaboration diagram for Minisat::ClauseAllocator:

Public Types
enum	{ Unit_Size = RegionAllocator<uint32_t>::Unit_Size }

Public Member Functions
	ClauseAllocator (uint32_t start_cap)
	ClauseAllocator ()
void	moveTo (ClauseAllocator &to)
CRef	alloc (const vec< Lit > &ps, bool learnt=false)
CRef	alloc (const Clause &from)
uint32_t	size () const
uint32_t	wasted () const
Clause &	operator[] (CRef r)
const Clause &	operator[] (CRef r) const
Clause *	lea (CRef r)
const Clause *	lea (CRef r) const
CRef	ael (const Clause *t)
void	free (CRef cid)
void	reloc (CRef &cr, ClauseAllocator &to)

Data Fields
bool	extra_clause_field

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

Private Attributes
RegionAllocator< uint32_t >	ra

Detailed Description

Definition at line 226 of file SolverTypes.h.

Member Enumeration Documentation

anonymous enum

Enumerator
Unit_Size

Definition at line 234 of file SolverTypes.h.

{ Unit_Size = RegionAllocator<uint32_t>::Unit_Size };

Constructor & Destructor Documentation

Minisat::ClauseAllocator::ClauseAllocator ( uint32_t  start_cap )

inline

Definition at line 238 of file SolverTypes.h.

: ra(start_cap), extra_clause_field(false){}

Minisat::ClauseAllocator::ClauseAllocator ( )

inline

Definition at line 239 of file SolverTypes.h.

: extra_clause_field(false){}

Member Function Documentation

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

inline

Definition at line 271 of file SolverTypes.h.

{ return ra.ael((uint32_t*)t); }

Here is the call graph for this function:

CRef Minisat::ClauseAllocator::alloc ( const vec< Lit > &  ps, bool  learnt = false  )

inline

Definition at line 245 of file SolverTypes.h.

    {
        assert(sizeof(Lit)      == sizeof(uint32_t));
        assert(sizeof(float)    == sizeof(uint32_t));
        bool use_extra = learnt | extra_clause_field;
        CRef cid       = ra.alloc(clauseWord32Size(ps.size(), use_extra));
        new (lea(cid)) Clause(ps, use_extra, learnt);

        return cid;
    }

Here is the call graph for this function:

Here is the caller graph for this function:

CRef Minisat::ClauseAllocator::alloc ( const Clause &  from )

inline

Definition at line 256 of file SolverTypes.h.

    {
        bool use_extra = from.learnt() | extra_clause_field;
        CRef cid       = ra.alloc(clauseWord32Size(from.size(), use_extra));
        new (lea(cid)) Clause(from, use_extra);
        return cid; }

Here is the call graph for this function:

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

inlinestaticprivate

Definition at line 230 of file SolverTypes.h.

                                                              {
        return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }

Here is the caller graph for this function:

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

inline

Definition at line 273 of file SolverTypes.h.

    {
        Clause& c = operator[](cid);
        ra.free(clauseWord32Size(c.size(), c.has_extra()));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

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

inline

Definition at line 269 of file SolverTypes.h.

{ return (Clause*)ra.lea(r); }

Here is the call graph for this function:

Here is the caller graph for this function:

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

inline

Definition at line 270 of file SolverTypes.h.

{ return (Clause*)ra.lea(r);; }

Here is the call graph for this function:

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

inline

Definition at line 241 of file SolverTypes.h.

                                    {
        to.extra_clause_field = extra_clause_field;
        ra.moveTo(to.ra); }

Here is the call graph for this function:

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

inline

Definition at line 267 of file SolverTypes.h.

{ return (Clause&)ra[r]; }

Here is the caller graph for this function:

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

inline

Definition at line 268 of file SolverTypes.h.

{ return (Clause&)ra[r]; }

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

inline

Definition at line 279 of file SolverTypes.h.

    {
        Clause& c = operator[](cr);
        
        if (c.reloced()) { cr = c.relocation(); return; }
        
        cr = to.alloc(c);
        c.relocate(cr);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

uint32_t Minisat::ClauseAllocator::size ( void  ) const

inline

Definition at line 263 of file SolverTypes.h.

{ return ra.size(); }

Here is the call graph for this function:

Here is the caller graph for this function:

uint32_t Minisat::ClauseAllocator::wasted ( ) const

inline

Definition at line 264 of file SolverTypes.h.

{ return ra.wasted(); }

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

bool Minisat::ClauseAllocator::extra_clause_field

Definition at line 236 of file SolverTypes.h.

RegionAllocator<uint32_t> Minisat::ClauseAllocator::ra

private

Definition at line 228 of file SolverTypes.h.

---

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

• SolverTypes.h