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)
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

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.

{ Ref_Undef = UINT32_MAX };

anonymous enum

inherited

Definition at line 46 of file Alloc.h.

{ Unit_Size = sizeof(uint32_t) };

Constructor & Destructor Documentation

Minisat::ClauseAllocator::ClauseAllocator ( uint32_t  start_cap )

inline

Definition at line 201 of file SolverTypes.h.

: RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}

Minisat::ClauseAllocator::ClauseAllocator ( )

inline

Definition at line 202 of file SolverTypes.h.

: extra_clause_field(false){}

Member Function Documentation

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

inlineinherited

Definition at line 60 of file Alloc.h.

{ wasted_ += size; }

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

inline

Definition at line 228 of file SolverTypes.h.

    {
        Clause& c = operator[](cid);
        RegionAllocator<uint32_t>::_free(clauseWord32Size(c.size(), c.has_extra()));
    }

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

inlineinherited

Definition at line 68 of file Alloc.h.

                                     { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
        return  (Ref)(t - &memory[0]); }

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

inline

Definition at line 226 of file SolverTypes.h.

{ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }

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.

    {
        assert(sizeof(Lit)      == sizeof(uint32_t));
        assert(sizeof(float)    == sizeof(uint32_t));
        bool use_extra = learnt | extra_clause_field;

        CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
        new (lea(cid)) Clause(ps, use_extra, learnt);

        return cid;
    }

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

inlinestaticprivate

Definition at line 196 of file SolverTypes.h.

                                                         {
        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.

{ return (Clause*)RegionAllocator<uint32_t>::lea(r); }

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

inline

Definition at line 225 of file SolverTypes.h.

{ return (Clause*)RegionAllocator<uint32_t>::lea(r); }

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

inlineinherited

Definition at line 71 of file Alloc.h.

                                         {
        if (to.memory != NULL) ::free(to.memory);
        to.memory = memory;
        to.sz = sz;
        to.cap = cap;
        to.wasted_ = wasted_;

        memory = NULL;
        sz = cap = wasted_ = 0;
    }

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

inline

Definition at line 204 of file SolverTypes.h.

                                    {
        to.extra_clause_field = extra_clause_field;
        RegionAllocator<uint32_t>::moveTo(to); }

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

inline

Definition at line 222 of file SolverTypes.h.

{ return (Clause&)RegionAllocator<uint32_t>::operator[](r); }

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

inline

Definition at line 223 of file SolverTypes.h.

{ return (Clause&)RegionAllocator<uint32_t>::operator[](r); }

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

inline

Definition at line 234 of file SolverTypes.h.

    {
        Clause& c = operator[](cr);
        
        if (c.reloced()) { cr = c.relocation(); return; }
        
        cr = to.alloc(c, c.learnt());
        c.relocate(cr);
        
        // Copy extra data-fields: 
        // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
        to[cr].mark(c.mark());
        if (to[cr].learnt())         to[cr].activity() = c.activity();
        else if (to[cr].has_extra()) to[cr].calcAbstraction();
    }

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

inlineinherited

Definition at line 56 of file Alloc.h.

{ return sz; }

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

inlineinherited

Definition at line 57 of file Alloc.h.

{ 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:

• SolverTypes.h