Public Types | |
typedef Solver::ConstraintDB | ConstraintDB |
typedef CBConsequences::SharedConstraint | SharedCon |
typedef SharedLiterals | SharedLits |
Public Member Functions | |
CBFinder (Solver &s, MinimizeConstraint *min, SharedCon *sh) | |
Constraint * | cloneAttach (Solver &s) |
Returns a clone of this and adds necessary watches to the given solver. | |
void | destroy (Solver *s, bool detach) |
Default is to call delete this. | |
void | doCommitModel (Enumerator &ctx, Solver &s) |
bool | doUpdate (Solver &s) |
void | pushLocked (Solver &s, ClauseHead *h) |
Public Attributes | |
LitVec | current |
SharedLits * | last |
ConstraintDB | locked |
SharedCon * | shared |
Definition at line 51 of file cb_enumerator.cpp.
Definition at line 54 of file cb_enumerator.cpp.
Definition at line 53 of file cb_enumerator.cpp.
Definition at line 55 of file cb_enumerator.cpp.
Clasp::CBConsequences::CBFinder::CBFinder | ( | Solver & | s, |
MinimizeConstraint * | min, | ||
SharedCon * | sh | ||
) | [inline] |
Definition at line 56 of file cb_enumerator.cpp.
Constraint* Clasp::CBConsequences::CBFinder::cloneAttach | ( | Solver & | other | ) | [inline, virtual] |
Returns a clone of this and adds necessary watches to the given solver.
The function shall create and return a copy of this constraint to be used in the given solver. Furthermore, it shall add necessary watches to the given solver.
Implements Clasp::Constraint.
Definition at line 59 of file cb_enumerator.cpp.
void Clasp::CBConsequences::CBFinder::destroy | ( | Solver * | s, |
bool | detach | ||
) | [virtual] |
Default is to call delete this.
Reimplemented from Clasp::EnumerationConstraint.
Definition at line 152 of file cb_enumerator.cpp.
void Clasp::CBConsequences::CBFinder::doCommitModel | ( | Enumerator & | ctx, |
Solver & | s | ||
) | [inline, virtual] |
Reimplemented from Clasp::EnumerationConstraint.
Definition at line 60 of file cb_enumerator.cpp.
bool Clasp::CBConsequences::CBFinder::doUpdate | ( | Solver & | s | ) | [virtual] |
Implements Clasp::EnumerationConstraint.
Definition at line 166 of file cb_enumerator.cpp.
void Clasp::CBConsequences::CBFinder::pushLocked | ( | Solver & | s, |
ClauseHead * | h | ||
) |
Definition at line 159 of file cb_enumerator.cpp.
Definition at line 64 of file cb_enumerator.cpp.
Definition at line 66 of file cb_enumerator.cpp.
Definition at line 67 of file cb_enumerator.cpp.
Definition at line 65 of file cb_enumerator.cpp.