Minisat::ClauseAllocator Class Reference

#include <SolverTypes.h>

Inheritance diagram for Minisat::ClauseAllocator:

Collaboration diagram for Minisat::ClauseAllocator:

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)
Public Member Functions inherited from Minisat::RegionAllocator< uint32_t >
	RegionAllocator (uint32_t start_cap=1024 *1024)
	~RegionAllocator ()
uint32_t	size () const
uint32_t	wasted () const
Ref	alloc (int size)
void	_free (int size)
uint32_t &	operator[] (Ref r)
const uint32_t &	operator[] (Ref r) const
uint32_t *	lea (Ref r)
const uint32_t *	lea (Ref r) const
Ref	ael (const uint32_t *t)
void	moveTo (RegionAllocator &to)

Public Attributes
bool	extra_clause_field

Additional Inherited Members
Public Types inherited from Minisat::RegionAllocator< uint32_t >
enum
enum
typedef uint32_t	Ref

Detailed Description

Definition at line 196 of file SolverTypes.h.

Constructor & Destructor Documentation

ClauseAllocator() [1/2]

Minisat::ClauseAllocator::ClauseAllocator ( uint32_t start_cap )

inline

Definition at line 203 of file SolverTypes.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

ClauseAllocator() [2/2]

Minisat::ClauseAllocator::ClauseAllocator ( )

inline

Definition at line 204 of file SolverTypes.h.

: extra_clause_field(false){}

Member Function Documentation

_free()

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

inline

Definition at line 230 of file SolverTypes.h.

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

Here is the call graph for this function:

ael()

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

inline

Definition at line 228 of file SolverTypes.h.

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

Here is the call graph for this function:

alloc()

template<class Lits>

CRef Minisat::ClauseAllocator::alloc ( const Lits & ps, bool learnt = false )

inline

Definition at line 211 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;
    }

Here is the call graph for this function:

Here is the caller graph for this function:

lea() [1/2]

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

inline

Definition at line 226 of file SolverTypes.h.

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

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 227 of file SolverTypes.h.

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

Here is the call graph for this function:

moveTo()

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

inline

Definition at line 206 of file SolverTypes.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

operator[]() [1/2]

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

inline

Definition at line 224 of file SolverTypes.h.

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

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 225 of file SolverTypes.h.

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

Here is the call graph for this function:

reloc()

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

inline

Definition at line 236 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();
    }

Here is the call graph for this function:

Member Data Documentation

extra_clause_field

bool Minisat::ClauseAllocator::extra_clause_field

Definition at line 201 of file SolverTypes.h.

---

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

• src/sat/bsat2/SolverTypes.h