Open
Graph Drawing
Framework

 v. 2022.02 (Dogwood)
 

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 Litlast () const
 
bool learnt () const
 
uint32_t mark () const
 
void mark (uint32_t m)
 
 operator const Lit * (void) const
 
Litoperator[] (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 Function 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.

◆ data

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

◆ has_extra

unsigned Minisat::Internal::Clause::has_extra

Definition at line 140 of file SolverTypes.h.

◆ header

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: