Open
Graph Drawing
Framework

  v. 2025.10 (Foxglove)
 
Overview Class Hierarchy Class Index Class List Members Namespaces Source Files
 

Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
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 137 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 150 of file SolverTypes.h.

Member Function Documentation

◆ abstraction()

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

Definition at line 196 of file SolverTypes.h.

◆ activity()

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

Definition at line 195 of file SolverTypes.h.

◆ calcAbstraction()

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

Definition at line 168 of file SolverTypes.h.

◆ has_extra()

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

Definition at line 180 of file SolverTypes.h.

◆ last()

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

Definition at line 183 of file SolverTypes.h.

◆ learnt()

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

Definition at line 179 of file SolverTypes.h.

◆ mark() [1/2]

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

Definition at line 181 of file SolverTypes.h.

◆ mark() [2/2]

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

Definition at line 182 of file SolverTypes.h.

◆ operator const Lit *()

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

Definition at line 193 of file SolverTypes.h.

◆ operator[]() [1/2]

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

Definition at line 191 of file SolverTypes.h.

◆ operator[]() [2/2]

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

Definition at line 192 of file SolverTypes.h.

◆ pop()

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

Definition at line 178 of file SolverTypes.h.

◆ relocate()

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

Definition at line 187 of file SolverTypes.h.

◆ relocation()

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

Definition at line 186 of file SolverTypes.h.

◆ reloced()

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

Definition at line 185 of file SolverTypes.h.

◆ shrink()

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

Definition at line 177 of file SolverTypes.h.

◆ size()

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

Definition at line 176 of file SolverTypes.h.

◆ strengthen()

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

Definition at line 420 of file SolverTypes.h.

◆ subsumes()

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

Definition at line 387 of file SolverTypes.h.

Friends And Related Symbol Documentation

◆ ClauseAllocator

friend class ClauseAllocator
friend

Definition at line 146 of file SolverTypes.h.

Member Data Documentation

◆ abs

uint32_t Minisat::Internal::Clause::abs

Definition at line 144 of file SolverTypes.h.

◆ act

float Minisat::Internal::Clause::act

Definition at line 144 of file SolverTypes.h.

◆ [union]

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

◆ has_extra

unsigned Minisat::Internal::Clause::has_extra

Definition at line 141 of file SolverTypes.h.

◆ [struct]

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

◆ learnt

unsigned Minisat::Internal::Clause::learnt

Definition at line 140 of file SolverTypes.h.

◆ lit

Lit Minisat::Internal::Clause::lit

Definition at line 144 of file SolverTypes.h.

◆ mark

unsigned Minisat::Internal::Clause::mark

Definition at line 139 of file SolverTypes.h.

◆ rel

CRef Minisat::Internal::Clause::rel

Definition at line 144 of file SolverTypes.h.

◆ reloced

unsigned Minisat::Internal::Clause::reloced

Definition at line 142 of file SolverTypes.h.

◆ size

unsigned Minisat::Internal::Clause::size

Definition at line 143 of file SolverTypes.h.

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