SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes | Friends
Minisat::Clause Class Reference

#include <SolverTypes.h>

Collaboration diagram for Minisat::Clause:
Collaboration graph
[legend]

Public Member Functions

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

Private Member Functions

template<class V >
 Clause (const V &ps, bool use_extra, unsigned _type)
 

Private Attributes

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

Friends

class ClauseAllocator
 
template<class V >
Clause * Clause_new (const V &ps, bool learnt=false)
 

Detailed Description

Definition at line 155 of file SolverTypes.h.

Constructor & Destructor Documentation

◆ Clause()

template<class V >
Minisat::Clause::Clause ( const V &  ps,
bool  use_extra,
unsigned  _type 
)
inlineprivate

Definition at line 168 of file SolverTypes.h.

Here is the call graph for this function:

Member Function Documentation

◆ abstraction()

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

Definition at line 226 of file SolverTypes.h.

Here is the caller graph for this function:

◆ activity() [1/2]

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

Definition at line 224 of file SolverTypes.h.

Here is the caller graph for this function:

◆ activity() [2/2]

float Minisat::Clause::activity ( ) const
inline

Definition at line 225 of file SolverTypes.h.

◆ calcAbstraction()

void Minisat::Clause::calcAbstraction ( )
inline

Definition at line 196 of file SolverTypes.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ has_extra()

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

Definition at line 209 of file SolverTypes.h.

◆ last()

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

Definition at line 212 of file SolverTypes.h.

◆ learnt()

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

Definition at line 208 of file SolverTypes.h.

Here is the caller graph for this function:

◆ mark() [1/2]

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

Definition at line 210 of file SolverTypes.h.

◆ mark() [2/2]

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

Definition at line 211 of file SolverTypes.h.

◆ operator const Lit *()

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

Definition at line 222 of file SolverTypes.h.

◆ operator[]() [1/2]

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

Definition at line 220 of file SolverTypes.h.

◆ operator[]() [2/2]

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

Definition at line 221 of file SolverTypes.h.

◆ pop()

void Minisat::Clause::pop ( )
inline

Definition at line 206 of file SolverTypes.h.

Here is the call graph for this function:

◆ relocate()

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

Definition at line 216 of file SolverTypes.h.

Here is the caller graph for this function:

◆ relocation()

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

Definition at line 215 of file SolverTypes.h.

Here is the caller graph for this function:

◆ reloced()

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

Definition at line 214 of file SolverTypes.h.

◆ shrink()

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

Definition at line 205 of file SolverTypes.h.

Here is the caller graph for this function:

◆ size()

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

Definition at line 204 of file SolverTypes.h.

◆ strengthen()

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

Definition at line 453 of file SolverTypes.h.

Here is the call graph for this function:

◆ subsumes()

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

Definition at line 422 of file SolverTypes.h.

◆ type()

unsigned Minisat::Clause::type ( ) const
inline

Definition at line 207 of file SolverTypes.h.

Friends And Related Function Documentation

◆ Clause_new

template<class V >
Clause* Clause_new ( const V &  ps,
bool  learnt = false 
)
friend

Definition at line 187 of file SolverTypes.h.

◆ ClauseAllocator

friend class ClauseAllocator
friend

Definition at line 164 of file SolverTypes.h.

Field Documentation

◆ abs

uint32_t Minisat::Clause::abs

Definition at line 162 of file SolverTypes.h.

◆ act

float Minisat::Clause::act

Definition at line 162 of file SolverTypes.h.

◆ 

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

◆ has_extra

unsigned Minisat::Clause::has_extra

Definition at line 159 of file SolverTypes.h.

◆ 

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

◆ lit

Lit Minisat::Clause::lit

Definition at line 162 of file SolverTypes.h.

◆ mark

unsigned Minisat::Clause::mark

Definition at line 157 of file SolverTypes.h.

◆ rel

CRef Minisat::Clause::rel

Definition at line 162 of file SolverTypes.h.

◆ reloced

unsigned Minisat::Clause::reloced

Definition at line 160 of file SolverTypes.h.

◆ size

unsigned Minisat::Clause::size

Definition at line 161 of file SolverTypes.h.

◆ type

unsigned Minisat::Clause::type

Definition at line 158 of file SolverTypes.h.

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