, including all inherited members.
activity() const | Clasp::ClauseHead | [inline, virtual] |
alloc(Solver &s, uint32 mLits, bool learnt) | Clasp::Clause | [static] |
attach(Solver &s) | Clasp::ClauseHead | |
BoolPair typedef | Clasp::ClauseHead | |
bumpActivity() | Clasp::ClauseHead | [inline] |
clause() | Clasp::ClauseHead | [inline, virtual] |
Clause(Solver &s, const ClauseRep &rep, uint32 tail=UINT32_MAX, bool extend=false) | Clasp::Clause | [private] |
Clause(Solver &s, const Clause &other) | Clasp::Clause | [private] |
ClauseHead(const ClauseInfo &init) | Clasp::ClauseHead | [explicit] |
ClauseWatch | Clasp::ClauseHead | [friend] |
clearTagged() | Clasp::ClauseHead | [inline, protected] |
cloneAttach(Solver &other) | Clasp::Clause | [virtual] |
computeAllocSize() const | Clasp::Clause | |
Constraint() | Clasp::Constraint | |
contracted() const | Clasp::Clause | [inline] |
data_ | Clasp::ClauseHead | [protected] |
decreaseActivity() | Clasp::ClauseHead | [inline, virtual] |
destroy(Solver *s=0, bool detach=false) | Clasp::Clause | [virtual] |
detach(Solver &) | Clasp::Clause | [virtual] |
estimateComplexity(const Solver &s) const | Clasp::Constraint | [virtual] |
hasLbd() const | Clasp::ClauseHead | [inline, protected] |
head_ | Clasp::ClauseHead | [protected] |
HEAD_LITS enum value | Clasp::ClauseHead | |
info_ | Clasp::ClauseHead | [protected] |
isOpen(const Solver &s, const TypeSet &t, LitVec &freeLits) | Clasp::Clause | [virtual] |
isReverseReason(const Solver &s, Literal p, uint32 maxL, uint32 maxN) | Clasp::Clause | [virtual] |
isSmall() const | Clasp::Clause | [inline] |
lbd() const | Clasp::ClauseHead | [inline] |
lbd(uint32 x) | Clasp::ClauseHead | [inline] |
learnt() const | Clasp::ClauseHead | [inline] |
LearntConstraint() | Clasp::LearntConstraint | |
LitRange typedef | Clasp::Clause | [private] |
locked(const Solver &s) const | Clasp::ClauseHead | [virtual] |
longEnd() | Clasp::Clause | [inline, private] |
MAX_ACTIVITY enum value | Clasp::ClauseHead | |
MAX_LBD enum value | Clasp::ClauseHead | |
MAX_SHORT_LEN enum value | Clasp::Clause | |
minimize(Solver &m, Literal p, CCMinRecursive *r) | Clasp::Clause | [virtual] |
newClause(Solver &s, const ClauseRep &rep) | Clasp::Clause | [inline, static] |
newClause(void *mem, Solver &s, const ClauseRep &rep) | Clasp::Clause | [static] |
newContractedClause(Solver &s, const ClauseRep &rep, uint32 tailPos, bool extend) | Clasp::Clause | [static] |
newShared(Solver &s, SharedLiterals *lits, const ClauseInfo &e, const Literal head[3], bool addRef=true) | Clasp::Clause | [static] |
propagate(Solver &s, Literal, uint32 &data) | Clasp::ClauseHead | [virtual] |
PropResult typedef | Clasp::Clause | |
reason(Solver &s, Literal p, LitVec &lits) | Clasp::Clause | [virtual] |
removeFromTail(Solver &s, Literal *it, Literal *end) | Clasp::Clause | [private] |
resetActivity(Activity a) | Clasp::ClauseHead | [inline, virtual] |
satisfied(const Solver &s) | Clasp::ClauseHead | |
setLbd(uint32 x) | Clasp::ClauseHead | [inline, protected] |
simplify(Solver &s, bool=false) | Clasp::Clause | [virtual] |
size() const | Clasp::Clause | [virtual] |
strengthen(Solver &s, Literal p, bool allowToShort) | Clasp::Clause | [virtual] |
strengthened() const | Clasp::Clause | [inline] |
tagged() const | Clasp::ClauseHead | [inline] |
TAGGED_CLAUSE enum value | Clasp::ClauseHead | |
tail() | Clasp::Clause | [inline, private] |
toImplication(Solver &s) | Clasp::ClauseHead | [protected] |
toLits(LitVec &out) const | Clasp::Clause | [virtual] |
type() const | Clasp::ClauseHead | [inline, virtual] |
undoLevel(Solver &s) | Clasp::Clause | [private, virtual] |
updateWatch(Solver &s, uint32 pos) | Clasp::Clause | [private, virtual] |
valid(Solver &s) | Clasp::Constraint | [virtual] |
~Constraint() | Clasp::Constraint | [protected, virtual] |
~LearntConstraint() | Clasp::LearntConstraint | [protected] |