#include <ogdf/lib/minisat/core/SolverTypes.h>
|
| template<class V > |
| | Clause (const V &ps, bool use_extra, bool learnt) |
| |
Definition at line 136 of file SolverTypes.h.
◆ Clause()
template<class V >
| Minisat::Internal::Clause::Clause |
( |
const V & |
ps, |
|
|
bool |
use_extra, |
|
|
bool |
learnt |
|
) |
| |
|
inlineprivate |
◆ abstraction()
| uint32_t Minisat::Internal::Clause::abstraction |
( |
| ) |
const |
|
inline |
◆ activity()
| float& Minisat::Internal::Clause::activity |
( |
| ) |
|
|
inline |
◆ calcAbstraction()
| void Minisat::Internal::Clause::calcAbstraction |
( |
| ) |
|
|
inline |
◆ has_extra()
| bool Minisat::Internal::Clause::has_extra |
( |
| ) |
const |
|
inline |
◆ last()
| const Lit& Minisat::Internal::Clause::last |
( |
| ) |
const |
|
inline |
◆ learnt()
| bool Minisat::Internal::Clause::learnt |
( |
| ) |
const |
|
inline |
◆ mark() [1/2]
| uint32_t Minisat::Internal::Clause::mark |
( |
| ) |
const |
|
inline |
◆ mark() [2/2]
| void Minisat::Internal::Clause::mark |
( |
uint32_t |
m | ) |
|
|
inline |
◆ operator const Lit *()
| Minisat::Internal::Clause::operator const Lit * |
( |
void |
| ) |
const |
|
inline |
◆ operator[]() [1/2]
| Lit& Minisat::Internal::Clause::operator[] |
( |
int |
i | ) |
|
|
inline |
◆ operator[]() [2/2]
| Lit Minisat::Internal::Clause::operator[] |
( |
int |
i | ) |
const |
|
inline |
◆ pop()
| void Minisat::Internal::Clause::pop |
( |
| ) |
|
|
inline |
◆ relocate()
| void Minisat::Internal::Clause::relocate |
( |
CRef |
c | ) |
|
|
inline |
◆ relocation()
| CRef Minisat::Internal::Clause::relocation |
( |
| ) |
const |
|
inline |
◆ reloced()
| bool Minisat::Internal::Clause::reloced |
( |
| ) |
const |
|
inline |
◆ shrink()
| void Minisat::Internal::Clause::shrink |
( |
int |
i | ) |
|
|
inline |
◆ size()
| int Minisat::Internal::Clause::size |
( |
| ) |
const |
|
inline |
◆ strengthen()
| void Minisat::Internal::Clause::strengthen |
( |
Lit |
p | ) |
|
|
inline |
◆ subsumes()
| Lit Minisat::Internal::Clause::subsumes |
( |
const Clause & |
other | ) |
const |
|
inline |
◆ ClauseAllocator
◆ abs
| uint32_t Minisat::Internal::Clause::abs |
◆ act
| float Minisat::Internal::Clause::act |
◆ data
| union { ... } Minisat::Internal::Clause::data[0] |
◆ has_extra
| unsigned Minisat::Internal::Clause::has_extra |
◆ header
| struct { ... } Minisat::Internal::Clause::header |
◆ learnt
| unsigned Minisat::Internal::Clause::learnt |
◆ lit
| Lit Minisat::Internal::Clause::lit |
◆ mark
| unsigned Minisat::Internal::Clause::mark |
◆ rel
| CRef Minisat::Internal::Clause::rel |
◆ reloced
| unsigned Minisat::Internal::Clause::reloced |
◆ size
| unsigned Minisat::Internal::Clause::size |
The documentation for this class was generated from the following file:
