Gluco::ClauseAllocator Class Reference

#include <SolverTypes.h>

Inheritance diagram for Gluco::ClauseAllocator:

Collaboration diagram for Gluco::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 Gluco::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)
void	clear ()
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 Gluco::RegionAllocator< uint32_t >
enum
enum
typedef uint32_t	Ref

Detailed Description

Definition at line 217 of file SolverTypes.h.

Constructor & Destructor Documentation

ClauseAllocator() [1/2]

Gluco::ClauseAllocator::ClauseAllocator ( uint32_t start_cap )

inline

Definition at line 224 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]

Gluco::ClauseAllocator::ClauseAllocator ( )

inline

Definition at line 225 of file SolverTypes.h.

: extra_clause_field(false){}

Member Function Documentation

ael()

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

inline

Definition at line 249 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 Gluco::ClauseAllocator::alloc ( const Lits & ps, bool learnt = false )

inline

Definition at line 232 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:

free_()

void Gluco::ClauseAllocator::free_ ( CRef cid )

inline

Definition at line 251 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:

lea() [1/2]

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

inline

Definition at line 247 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 * Gluco::ClauseAllocator::lea ( Ref r ) const

inline

Definition at line 248 of file SolverTypes.h.

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

Here is the call graph for this function:

moveTo()

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

inline

Definition at line 227 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 & Gluco::ClauseAllocator::operator[] ( Ref r )

inline

Definition at line 245 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 & Gluco::ClauseAllocator::operator[] ( Ref r ) const

inline

Definition at line 246 of file SolverTypes.h.

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

Here is the call graph for this function:

reloc()

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

inline

Definition at line 257 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();
      to[cr].setLBD(c.lbd());
      to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors());
      to[cr].setCanBeDel(c.canBeDel());
    }
        else if (to[cr].has_extra()) to[cr].calcAbstraction();
    }

Here is the call graph for this function:

Member Data Documentation

extra_clause_field

bool Gluco::ClauseAllocator::extra_clause_field

Definition at line 222 of file SolverTypes.h.

---

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

• src/sat/glucose/SolverTypes.h