Minisat::Internal::Clause Class Reference

#include <ogdf/lib/minisat/core/SolverTypes.h>

Public Member Functions
uint32_t	abstraction () const
float &	activity ()
void	calcAbstraction ()
bool	has_extra () const
const Lit &	last () const
bool	learnt () const
uint32_t	mark () const
void	mark (uint32_t m)
	operator const Lit * (void) const
Lit &	operator[] (int i)
Lit	operator[] (int i) const
void	pop ()
void	relocate (CRef c)
CRef	relocation () const
bool	reloced () const
void	shrink (int i)
int	size () const
void	strengthen (Lit p)
Lit	subsumes (const Clause &other) const

Private Member Functions
template<class V >
	Clause (const V &ps, bool use_extra, bool learnt)

Private Attributes
union {
uint32_t   abs
float   act
Lit   lit
CRef   rel
}	data [0]
struct {
unsigned   has_extra: 1
unsigned   learnt: 1
unsigned   mark: 2
unsigned   reloced: 1
unsigned   size: 27
}	header

Friends
class	ClauseAllocator

Detailed Description

Definition at line 136 of file SolverTypes.h.

Constructor & Destructor Documentation

Clause()

template<class V >

Minisat::Internal::Clause::Clause ( const V &  ps, bool  use_extra, bool  learnt  )

inlineprivate

Definition at line 149 of file SolverTypes.h.

Member Function Documentation

abstraction()

uint32_t Minisat::Internal::Clause::abstraction ( ) const

inline

Definition at line 195 of file SolverTypes.h.

activity()

float & Minisat::Internal::Clause::activity ( )

inline

Definition at line 194 of file SolverTypes.h.

calcAbstraction()

void Minisat::Internal::Clause::calcAbstraction ( )

inline

Definition at line 167 of file SolverTypes.h.

has_extra()

bool Minisat::Internal::Clause::has_extra ( ) const

inline

Definition at line 179 of file SolverTypes.h.

last()

const Lit & Minisat::Internal::Clause::last ( ) const

inline

Definition at line 182 of file SolverTypes.h.

learnt()

bool Minisat::Internal::Clause::learnt ( ) const

inline

Definition at line 178 of file SolverTypes.h.

mark() [1/2]

uint32_t Minisat::Internal::Clause::mark ( ) const

inline

Definition at line 180 of file SolverTypes.h.

mark() [2/2]

void Minisat::Internal::Clause::mark ( uint32_t  m )

inline

Definition at line 181 of file SolverTypes.h.

operator const Lit *()

Minisat::Internal::Clause::operator const Lit * ( void  ) const

inline

Definition at line 192 of file SolverTypes.h.

operator[]() [1/2]

Lit & Minisat::Internal::Clause::operator[] ( int  i )

inline

Definition at line 190 of file SolverTypes.h.

operator[]() [2/2]

Lit Minisat::Internal::Clause::operator[] ( int  i ) const

inline

Definition at line 191 of file SolverTypes.h.

pop()

void Minisat::Internal::Clause::pop ( )

inline

Definition at line 177 of file SolverTypes.h.

relocate()

void Minisat::Internal::Clause::relocate ( CRef  c )

inline

Definition at line 186 of file SolverTypes.h.

relocation()

CRef Minisat::Internal::Clause::relocation ( ) const

inline

Definition at line 185 of file SolverTypes.h.

reloced()

bool Minisat::Internal::Clause::reloced ( ) const

inline

Definition at line 184 of file SolverTypes.h.

shrink()

void Minisat::Internal::Clause::shrink ( int  i )

inline

Definition at line 176 of file SolverTypes.h.

size()

int Minisat::Internal::Clause::size ( ) const

inline

Definition at line 175 of file SolverTypes.h.

strengthen()

void Minisat::Internal::Clause::strengthen ( Lit  p )

inline

Definition at line 419 of file SolverTypes.h.

subsumes()

Lit Minisat::Internal::Clause::subsumes ( const Clause &  other ) const

inline

Definition at line 386 of file SolverTypes.h.

Friends And Related Symbol Documentation

ClauseAllocator

friend class ClauseAllocator

friend

Definition at line 145 of file SolverTypes.h.

Member Data Documentation

abs

uint32_t Minisat::Internal::Clause::abs

Definition at line 143 of file SolverTypes.h.

act

float Minisat::Internal::Clause::act

Definition at line 143 of file SolverTypes.h.

[union]

union { ... } Minisat::Internal::Clause::data[0]

has_extra

unsigned Minisat::Internal::Clause::has_extra

Definition at line 140 of file SolverTypes.h.

[struct]

struct { ... } Minisat::Internal::Clause::header

learnt

unsigned Minisat::Internal::Clause::learnt

Definition at line 139 of file SolverTypes.h.

lit

Lit Minisat::Internal::Clause::lit

Definition at line 143 of file SolverTypes.h.

mark

unsigned Minisat::Internal::Clause::mark

Definition at line 138 of file SolverTypes.h.

rel

CRef Minisat::Internal::Clause::rel

Definition at line 143 of file SolverTypes.h.

reloced

unsigned Minisat::Internal::Clause::reloced

Definition at line 141 of file SolverTypes.h.

size

unsigned Minisat::Internal::Clause::size

Definition at line 142 of file SolverTypes.h.

---

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

• include/ogdf/lib/minisat/core/SolverTypes.h