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