, including all inherited members.
| addClause(const LitVec &cl) | Clasp::SatPreprocessor | [inline] |
| addClause(const Literal *clause, uint32 size) | Clasp::SatPreprocessor | |
| addResolvent(uint32 newId, const Clause &c1, const Clause &c2) | Clasp::SatElite::SatElite | [private] |
| addToSubQueue(uint32 clauseId) | Clasp::SatElite::SatElite | [inline, private] |
| attach(uint32 cId, bool initialClause) | Clasp::SatElite::SatElite | [private] |
| backwardSubsume() | Clasp::SatElite::SatElite | [private] |
| bce() | Clasp::SatElite::SatElite | [private] |
| bceVe(Var v, uint32 maxCnt) | Clasp::SatElite::SatElite | [private] |
| bceVeRemove(uint32 cId, bool freeId, Var v, bool blocked) | Clasp::SatElite::SatElite | [private] |
| clause(uint32 clId) | Clasp::SatPreprocessor | [inline, protected] |
| clause(uint32 clId) const | Clasp::SatPreprocessor | [inline, protected] |
| ClauseList typedef | Clasp::SatPreprocessor | [protected] |
| cleanUp(bool discardEliminated=false) | Clasp::SatPreprocessor | |
| ClIter typedef | Clasp::SatElite::SatElite | [private] |
| clone() | Clasp::SatElite::SatElite | [virtual] |
| ClRange typedef | Clasp::SatElite::SatElite | [private] |
| ClWList typedef | Clasp::SatElite::SatElite | [private] |
| ctx_ | Clasp::SatPreprocessor | [protected] |
| cutoff(Var v) const | Clasp::SatElite::SatElite | [inline, private] |
| destroyClause(uint32 clId) | Clasp::SatPreprocessor | [inline, protected] |
| detach(uint32 cId) | Clasp::SatElite::SatElite | [private] |
| discardClauses(bool discardEliminated) | Clasp::SatPreprocessor | [protected] |
| doCleanUp() | Clasp::SatElite::SatElite | [protected, virtual] |
| doExtendModel(ValueVec &m, LitVec &open) | Clasp::SatElite::SatElite | [protected, virtual] |
| doPreprocess() | Clasp::SatElite::SatElite | [protected, virtual] |
| ElimHeap typedef | Clasp::SatElite::SatElite | [private] |
| elimHeap_ | Clasp::SatElite::SatElite | [private] |
| eliminateClause(uint32 id) | Clasp::SatPreprocessor | [inline, protected] |
| eliminateVars() | Clasp::SatElite::SatElite | [private] |
| elimTop_ | Clasp::SatPreprocessor | [protected] |
| extendModel(ValueVec &m, LitVec &open) | Clasp::SatPreprocessor | |
| facts_ | Clasp::SatElite::SatElite | [private] |
| findUnmarkedLit(const Clause &c, uint32 x) const | Clasp::SatElite::SatElite | [inline, private] |
| freezeSeen() | Clasp::SatPreprocessor | [protected] |
| initPreprocess(Options &opts) | Clasp::SatElite::SatElite | [protected, virtual] |
| markAll(const Literal *lits, uint32 size) const | Clasp::SatElite::SatElite | [private] |
| negT_ | Clasp::SatElite::SatElite | [private] |
| numClauses() const | Clasp::SatPreprocessor | [inline] |
| occurs_ | Clasp::SatElite::SatElite | [private] |
| operator=(const SatElite &) | Clasp::SatElite::SatElite | [private] |
| Options typedef | Clasp::SatPreprocessor | |
| opts_ | Clasp::SatElite::SatElite | [private] |
| peekSubQueue() const | Clasp::SatElite::SatElite | [inline, private] |
| popSubQueue() | Clasp::SatElite::SatElite | [inline, private] |
| posT_ | Clasp::SatElite::SatElite | [private] |
| preprocess(SharedContext &ctx, SatPreParams &opts) | Clasp::SatPreprocessor | |
| preprocess(SharedContext &ctx) | Clasp::SatPreprocessor | |
| propagateFacts() | Clasp::SatElite::SatElite | [private] |
| qFront_ | Clasp::SatElite::SatElite | [private] |
| queue_ | Clasp::SatElite::SatElite | [private] |
| reportProgress(Progress::EventOp, uint32 curr, uint32 max) | Clasp::SatElite::SatElite | [protected] |
| resCands_ | Clasp::SatElite::SatElite | [private] |
| resolvent_ | Clasp::SatElite::SatElite | [private] |
| SatElite() | Clasp::SatElite::SatElite | |
| SatElite(const SatElite &) | Clasp::SatElite::SatElite | [private] |
| SatPreprocessor() | Clasp::SatPreprocessor | [inline] |
| setClause(uint32 clId, const LitVec &cl) | Clasp::SatPreprocessor | [inline, protected] |
| splitOcc(Var v, bool mark) | Clasp::SatElite::SatElite | [private] |
| stats | Clasp::SatPreprocessor | |
| strengthenClause(uint32 clauseId, Literal p) | Clasp::SatElite::SatElite | [private] |
| subsumed(LitVec &cl) | Clasp::SatElite::SatElite | [private] |
| subsumes(const Clause &c, const Clause &other, Literal res) const | Clasp::SatElite::SatElite | [private] |
| timeout() const | Clasp::SatElite::SatElite | [inline, private] |
| timeout_ | Clasp::SatElite::SatElite | [private] |
| TouchedList typedef | Clasp::SatElite::SatElite | [private] |
| trivialResolvent(const Clause &c2, Var v) const | Clasp::SatElite::SatElite | [private] |
| unmarkAll(const Literal *lits, uint32 size) const | Clasp::SatElite::SatElite | [private] |
| updateHeap(Var v) | Clasp::SatElite::SatElite | [inline, private] |
| WIter typedef | Clasp::SatElite::SatElite | [private] |
| ~SatElite() | Clasp::SatElite::SatElite | |
| ~SatPreprocessor() | Clasp::SatPreprocessor | [virtual] |