, including all inherited members.
| add(Constraint *c) | Clasp::Solver | |
| add(const ClauseRep &c, bool isNew=true) | Clasp::Solver | |
| addLearnt(LearntConstraint *c, uint32 size, ConstraintType type) | Clasp::Solver | [inline] |
| addLearnt(LearntConstraint *c, uint32 size) | Clasp::Solver | [inline] |
| addLearntBytes(uint32 bytes) | Clasp::Solver | [inline] |
| addPost(PostPropagator *p) | Clasp::Solver | [inline] |
| addPost(PostPropagator *p, bool init) | Clasp::Solver | [inline] |
| addUndoWatch(uint32 dl, Constraint *c) | Clasp::Solver | [inline] |
| addWatch(Literal p, Constraint *c, uint32 data=0) | Clasp::Solver | [inline] |
| addWatch(Literal p, const ClauseWatch &w) | Clasp::Solver | [inline] |
| allocSmall() | Clasp::Solver | [inline] |
| allocUndo(Constraint *c) | Clasp::Solver | [private] |
| allowImplicit(const ClauseRep &c) const | Clasp::Solver | [inline] |
| analyzeConflict() | Clasp::Solver | [private] |
| assign_ | Clasp::Solver | [private] |
| assignment() const | Clasp::Solver | [inline] |
| assume(const Literal &p) | Clasp::Solver | |
| auxVar(Var var) const | Clasp::Solver | [inline] |
| backtrack() | Clasp::Solver | |
| backtrackLevel() const | Clasp::Solver | [inline] |
| bumpAct_ | Clasp::Solver | [private] |
| cancelPropagation() | Clasp::Solver | [inline, private] |
| cc_ | Clasp::Solver | [private] |
| ccHasReverseArc(Literal p, uint32 maxLevel, uint32 maxNew) | Clasp::Solver | [private] |
| ccInfo_ | Clasp::Solver | [private] |
| ccMin_ | Clasp::Solver | [private] |
| ccMinimize(Literal p, CCMinRecursive *rec) const | Clasp::Solver | [inline] |
| ccMinimize(LitVec &cc, LitVec &removed, uint32 antes, CCMinRecursive *ccMin) | Clasp::Solver | [private] |
| ccRemovable(Literal p, uint32 antes, CCMinRecursive *ccMin) | Clasp::Solver | [private] |
| ccResolve(LitVec &cc, uint32 pos, const LitVec &reason) | Clasp::Solver | [private] |
| cflStamp_ | Clasp::Solver | [private] |
| clearAssumptions() | Clasp::Solver | |
| clearSeen(Var v) | Clasp::Solver | [inline] |
| clearStopConflict() | Clasp::Solver | |
| cloneDB(const ConstraintDB &db) | Clasp::Solver | [private] |
| configuration() const | Clasp::Solver | |
| conflict() const | Clasp::Solver | [inline] |
| conflict_ | Clasp::Solver | [private] |
| conflictClause() const | Clasp::Solver | [inline] |
| ConstraintDB typedef | Clasp::Solver | |
| constraints() const | Clasp::Solver | [inline] |
| constraints_ | Clasp::Solver | [private] |
| copyGuidingPath(LitVec &out) | Clasp::Solver | |
| countLevels(const Literal *first, const Literal *last, uint32 maxLevels) | Clasp::Solver | |
| dbIdx_ | Clasp::Solver | [private] |
| DBRef typedef | Clasp::Solver | |
| decideNextBranch(double f=0.0) | Clasp::Solver | |
| decision(uint32 dl) const | Clasp::Solver | [inline] |
| decisionLevel() const | Clasp::Solver | [inline] |
| distribute(const Literal *lits, uint32 size, const ClauseInfo &extra) | Clasp::Solver | |
| endInit() | Clasp::Solver | [private] |
| enum_ | Clasp::Solver | [private] |
| enumerationConstraint() const | Clasp::Solver | [inline] |
| estimateBCP(const Literal &p, int maxRecursionDepth=5) const | Clasp::Solver | |
| finalizeConflictClause(LitVec &cc, ClauseInfo &info, uint32 ccRepMode=0) | Clasp::Solver | |
| force(const Literal &p, const Antecedent &a) | Clasp::Solver | [inline] |
| force(const Literal &p, const Antecedent &a, uint32 data) | Clasp::Solver | [inline] |
| force(Literal p, uint32 dl, const Antecedent &r, uint32 d=UINT32_MAX) | Clasp::Solver | [inline] |
| force(Literal p) | Clasp::Solver | [inline] |
| freeLearntBytes(uint64 bytes) | Clasp::Solver | [inline] |
| freeMem() | Clasp::Solver | [private] |
| freeSmall(void *m) | Clasp::Solver | [inline] |
| freezeLevel(uint32 dl) | Clasp::Solver | [inline] |
| frozenLevel(uint32 dl) const | Clasp::Solver | [inline] |
| getLearnt(uint32 idx) const | Clasp::Solver | [inline] |
| getPost(uint32 prio) const | Clasp::Solver | |
| getWatch(Literal p, Constraint *c) const | Clasp::Solver | |
| hasConflict() const | Clasp::Solver | [inline] |
| hasLevel(uint32 dl) const | Clasp::Solver | [inline] |
| hasStopConflict() const | Clasp::Solver | [inline] |
| hasWatch(Literal p, Constraint *c) const | Clasp::Solver | |
| hasWatch(Literal p, ClauseHead *c) const | Clasp::Solver | |
| Heuristic typedef | Clasp::Solver | |
| heuristic() const | Clasp::Solver | [inline] |
| heuristic() | Clasp::Solver | [inline] |
| heuristic_ | Clasp::Solver | [private] |
| id() const | Clasp::Solver | [inline] |
| impliedLits_ | Clasp::Solver | [private] |
| inDegree(WeightLitVec &out) | Clasp::Solver | |
| initPost_ | Clasp::Solver | [private] |
| isFalse(Literal p) const | Clasp::Solver | [inline] |
| isTrue(Literal p) const | Clasp::Solver | [inline] |
| lastSimp_ | Clasp::Solver | [private] |
| lbdStamp_ | Clasp::Solver | [private] |
| lbdTime_ | Clasp::Solver | [private] |
| learntLimit(const SearchLimits &x) const | Clasp::Solver | [inline] |
| learnts_ | Clasp::Solver | [private] |
| level(Var v) const | Clasp::Solver | [inline] |
| levels_ | Clasp::Solver | [private] |
| levelStart(uint32 dl) const | Clasp::Solver | [inline] |
| markLevel(uint32 dl) | Clasp::Solver | [inline] |
| markSeen(Var v) | Clasp::Solver | [inline] |
| markSeen(Literal p) | Clasp::Solver | [inline] |
| memUse_ | Clasp::Solver | [private] |
| model | Clasp::Solver | |
| numAssignedVars() const | Clasp::Solver | [inline] |
| numAuxVars() const | Clasp::Solver | [inline] |
| numConstraints() const | Clasp::Solver | |
| numFreeVars() const | Clasp::Solver | [inline] |
| numLearntConstraints() const | Clasp::Solver | [inline] |
| numProblemVars() const | Clasp::Solver | [inline] |
| numVars() const | Clasp::Solver | [inline] |
| numWatches(Literal p) const | Clasp::Solver | |
| otfs(Antecedent &lhs, const Antecedent &rhs, Literal p, bool final) | Clasp::Solver | [private] |
| otfsRemove(ClauseHead *c, const LitVec *newC) | Clasp::Solver | [private] |
| popAuxVar(uint32 num=UINT32_MAX) | Clasp::Solver | |
| popRootLevel(uint32 i=1, LitVec *popped=0, bool aux=true) | Clasp::Solver | |
| post_ | Clasp::Solver | [private] |
| pref(Var v) const | Clasp::Solver | [inline] |
| preparePost() | Clasp::Solver | [private] |
| propagate() | Clasp::Solver | |
| propagateUntil(PostPropagator *p) | Clasp::Solver | [inline] |
| pushAuxVar() | Clasp::Solver | |
| pushRoot(const LitVec &path) | Clasp::Solver | |
| pushRoot(Literal p) | Clasp::Solver | |
| pushRootLevel(uint32 i=1) | Clasp::Solver | [inline] |
| pushTagVar(bool pushToRoot) | Clasp::Solver | |
| queueSize() const | Clasp::Solver | [inline] |
| reason(Literal p) const | Clasp::Solver | [inline] |
| reason(Literal p, LitVec &out) | Clasp::Solver | [inline] |
| reasonData(Literal p) const | Clasp::Solver | [inline] |
| ReasonVec typedef | Clasp::Solver | [private] |
| receive(SharedLiterals **out, uint32 maxOut) const | Clasp::Solver | |
| reduceLearnts(float remMax, const ReduceStrategy &rs=ReduceStrategy()) | Clasp::Solver | |
| reduceLinear(uint32 maxR, const CmpScore &cmp) | Clasp::Solver | [private] |
| reduceSort(uint32 maxR, const CmpScore &cmp) | Clasp::Solver | [private] |
| reduceSortInPlace(uint32 maxR, const CmpScore &cmp, bool onlyPartialSort) | Clasp::Solver | [private] |
| removeConditional() | Clasp::Solver | |
| removePost(PostPropagator *p) | Clasp::Solver | [inline] |
| removeUndoWatch(uint32 dl, Constraint *c) | Clasp::Solver | |
| removeWatch(const Literal &p, Constraint *c) | Clasp::Solver | |
| removeWatch(const Literal &p, ClauseHead *c) | Clasp::Solver | |
| requestData(Var v) | Clasp::Solver | [inline] |
| reset() | Clasp::Solver | [private] |
| resetId(uint32 id) | Clasp::Solver | [inline, private] |
| resolveConflict() | Clasp::Solver | |
| restart() | Clasp::Solver | [inline] |
| rng | Clasp::Solver | |
| rootLevel() const | Clasp::Solver | [inline] |
| satPrepro() const | Clasp::Solver | |
| search(SearchLimits &limit, double randf=0.0) | Clasp::Solver | |
| search(uint64 maxC, uint32 maxL, bool local=false, double rp=0.0) | Clasp::Solver | [inline] |
| searchConfig() const | Clasp::Solver | |
| seen(Var v) const | Clasp::Solver | [inline] |
| seen(Literal p) const | Clasp::Solver | [inline] |
| setBacktrackLevel(uint32 dl) | Clasp::Solver | [inline] |
| setConflict(Literal p, const Antecedent &a, uint32 data) | Clasp::Solver | [private] |
| setEnumerationConstraint(Constraint *c) | Clasp::Solver | |
| setPref(Var v, ValueSet::Value which, ValueRep to) | Clasp::Solver | [inline] |
| setReason(Literal p, const Antecedent &x, uint32 data=UINT32_MAX) | Clasp::Solver | [inline] |
| setStopConflict() | Clasp::Solver | |
| shared_ | Clasp::Solver | [private] |
| SharedContext class | Clasp::Solver | [friend] |
| sharedContext() const | Clasp::Solver | [inline] |
| shuffleOnNextSimplify() | Clasp::Solver | [inline] |
| shufSimp_ | Clasp::Solver | [private] |
| simplify() | Clasp::Solver | |
| simplifyConflictClause(LitVec &cc, ClauseInfo &info, ClauseHead *rhs) | Clasp::Solver | |
| simplifySAT() | Clasp::Solver | [private] |
| smallAlloc_ | Clasp::Solver | [private] |
| Solver(SharedContext *ctx, uint32 id) | Clasp::Solver | [private] |
| split(LitVec &out) | Clasp::Solver | |
| splittable() const | Clasp::Solver | |
| startInit(uint32 constraintGuess) | Clasp::Solver | [private] |
| stats | Clasp::Solver | |
| strategy | Clasp::Solver | |
| strengthenConditional() | Clasp::Solver | |
| symbolTable() const | Clasp::Solver | [inline] |
| symmetric() const | Clasp::Solver | [inline] |
| tag_ | Clasp::Solver | [private] |
| tagLiteral() const | Clasp::Solver | [inline] |
| temp_ | Clasp::Solver | [private] |
| test(Literal p, PostPropagator *c) | Clasp::Solver | |
| topValue(Var v) const | Clasp::Solver | [inline] |
| trail() const | Clasp::Solver | [inline] |
| trueLit(Var v) const | Clasp::Solver | [inline] |
| undoFree(ConstraintDB *x) | Clasp::Solver | [private] |
| undoHead_ | Clasp::Solver | [private] |
| undoLevel(bool sp) | Clasp::Solver | [private] |
| undoUntil(uint32 dl) | Clasp::Solver | |
| undoUntil(uint32 dl, bool popBtLevel) | Clasp::Solver | |
| unfreezeLevel(uint32 dl) | Clasp::Solver | [inline] |
| unitPropagate() | Clasp::Solver | [private] |
| unmarkLevel(uint32 dl) | Clasp::Solver | [inline] |
| updateBranch(uint32 cfl) | Clasp::Solver | [private] |
| updateLearnt(Literal p, const Literal *first, const Literal *last, uint32 cLbd, bool forceUp=false) | Clasp::Solver | [inline] |
| validLevel(uint32 dl) const | Clasp::Solver | [inline] |
| validVar(Var var) const | Clasp::Solver | [inline] |
| validWatch(Literal p) const | Clasp::Solver | [inline, private] |
| value(Var v) const | Clasp::Solver | [inline] |
| varInfo(Var v) const | Clasp::Solver | [inline] |
| Watches typedef | Clasp::Solver | [private] |
| watches_ | Clasp::Solver | [private] |
| ~Solver() | Clasp::Solver | [private] |