Selects the first free literal w.r.t to the initial variable order. More...
#include <solver.h>
Inheritance diagram for Clasp::SelectFirst:
Public Member Functions | |
| void | updateVar (const Solver &, Var, uint32) |
Private Member Functions | |
| Literal | doSelect (Solver &s) |
| Implements the actual selection process. | |
Detailed Description
Selects the first free literal w.r.t to the initial variable order.
Member Function Documentation
| Literal Clasp::SelectFirst::doSelect | ( | Solver & | ) | [private, virtual] |
Implements the actual selection process.
- Precondition:
- s.numFreeVars() > 0, i.e. there is at least one variable to branch on.
- Returns:
- a literal that is currently free or
- a sentinel literal. In that case, the heuristic shall have asserted a literal!
Implements Clasp::DecisionHeuristic.
Definition at line 33 of file solver.cpp.
| void Clasp::SelectFirst::updateVar | ( | const Solver & | , |
| Var | , | ||
| uint32 | |||
| ) | [inline, virtual] |
Called if the state of one or more variables changed. A state change is one of:
- A previously eliminated variable is resurrected.
- A new aux variable was added.
- An aux variable was removed.
- Parameters:
-
s Solver in which the state change occurred. v The first variable affected by the change. n The range of variables affected, i.e. [v, v+n).
- Note:
- Use s.validVar(v) and s.auxVar(v) to determine the reason for the update.
Implements Clasp::DecisionHeuristic.
The documentation for this class was generated from the following files: