Base class for post propagators. More...
#include <constraint.h>
Public Types | |
| enum | Priority { priority_class_simple = 0, priority_reserved_msg = 0, priority_reserved_ufs = 10, priority_reserved_look = 1023, priority_class_general = 1024 } |
| Default priorities for post propagators. More... | |
Public Member Functions | |
| virtual bool | init (Solver &s) |
| Called during initialization of s. | |
| virtual bool | isModel (Solver &s) |
| Is the current total assignment a model? | |
| PostPropagator () | |
| virtual uint32 | priority () const =0 |
| Shall return a value representing the priority of this propagator. | |
| virtual bool | propagateFixpoint (Solver &s, PostPropagator *ctx)=0 |
| Shall enqueue and propagate new assignments implied by this propagator. | |
| virtual void | reset () |
| Aborts an active propagation operation. | |
| virtual | ~PostPropagator () |
Public Attributes | |
| PostPropagator * | next |
Protected Member Functions | |
| Constraint * | cloneAttach (Solver &) |
| PostPropagators are not clonable by default. | |
| PropResult | propagate (Solver &, Literal, uint32 &) |
| void | reason (Solver &, Literal, LitVec &) |
Private Member Functions | |
| PostPropagator & | operator= (const PostPropagator &) |
| PostPropagator (const PostPropagator &) | |
Detailed Description
Base class for post propagators.
Post propagators are called during propagation on each decision level and once after a total assignment is found.
They may extend a solver's unit-propagation with more elaborate propagation mechanisms. The typical asp example is an unfounded set check.
- Note:
- Currently, the solver distinguishes *two* classes of post propagators:
- class_simple: deterministic post propagators shall only extend the current decision level. That is, given DL, the decision level on which propagation started, these post propagators shall neither backtrack below DL nor permanently add new decision levels. Deterministic post propagators are called in priority order. For this, the function PostPropagator::priority() is used and shall return a priority in the range: [priority_class_simple, priority_class_general)
- class_general: post propagators that are non-deterministic or those that are not limited to extending the current decision level shall have a priority of priority_class_general. They are called in LIFO order but only after *all* simple post propagators have reached a fixpoint.
- There are currently three reserved priority values, namely priority_reserved_msg for message and termination handler (if any), priority_reserved_ufs for the default unfounded set checker (if any), and priority_reserved_look for the default lookahead operator (if any).
Definition at line 264 of file constraint.h.
Member Enumeration Documentation
Default priorities for post propagators.
- Enumerator:
Definition at line 272 of file constraint.h.
Constructor & Destructor Documentation
Definition at line 45 of file constraint.cpp.
| Clasp::PostPropagator::~PostPropagator | ( | ) | [virtual] |
Definition at line 46 of file constraint.cpp.
| Clasp::PostPropagator::PostPropagator | ( | const PostPropagator & | ) | [private] |
Member Function Documentation
| Constraint* Clasp::PostPropagator::cloneAttach | ( | Solver & | ) | [inline, protected, virtual] |
PostPropagators are not clonable by default.
Implements Clasp::Constraint.
Definition at line 350 of file constraint.h.
| bool Clasp::PostPropagator::init | ( | Solver & | s | ) | [virtual] |
Called during initialization of s.
- Note:
- During initialization a post propagator may assign variables but it must not yet propagate them.
Reimplemented in Clasp::Lookahead, Clasp::DefaultUnfoundedCheck, and Clasp::Test::TestingPostProp.
Definition at line 47 of file constraint.cpp.
| bool Clasp::PostPropagator::isModel | ( | Solver & | s | ) | [virtual] |
Is the current total assignment a model?
- Precondition:
- The assignment is total and not conflicting.
- Returns:
- true if the assignment is a model w.r.t this post propagator
- false otherwise
- Postcondition:
- If the function returned true: s.numFreeVars() == 0 && !s.hasConflict(). If the function returned false: s.numFreeVars() > 0 || s.hasConflict().
- Note:
- The default implementation returns Constraint::valid(s);
Reimplemented in Clasp::DefaultUnfoundedCheck.
Definition at line 49 of file constraint.cpp.
| PostPropagator& Clasp::PostPropagator::operator= | ( | const PostPropagator & | ) | [private] |
| virtual uint32 Clasp::PostPropagator::priority | ( | ) | const [pure virtual] |
Shall return a value representing the priority of this propagator.
The priority is used to order sequences of post propagators and to classify post propagators w.r.t the classes: class_simple and class_general.
- Note:
- See class description for an overview of the two priority classes.
Implemented in Clasp::MessageHandler, Clasp::Lookahead, Clasp::Test::TestingPostProp, and Clasp::DefaultUnfoundedCheck.
| Constraint::PropResult Clasp::PostPropagator::propagate | ( | Solver & | s, |
| Literal | p, | ||
| uint32 & | data | ||
| ) | [protected, virtual] |
Propagate is called for each constraint that watches p. It shall enqueue all consequences of p becoming true.
- Precondition:
- p is true in s
- Parameters:
-
s The solver in which p became true. p A literal watched by this constraint that recently became true. data The data-blob that this constraint passed when the watch for p was registered.
Implements Clasp::Constraint.
Reimplemented in Clasp::DefaultUnfoundedCheck.
Definition at line 51 of file constraint.cpp.
| virtual bool Clasp::PostPropagator::propagateFixpoint | ( | Solver & | s, |
| PostPropagator * | ctx | ||
| ) | [pure virtual] |
Shall enqueue and propagate new assignments implied by this propagator.
This function shall enqueue and propagate all assignments currently implied by this propagator until a fixpoint is reached w.r.t this post propagator or a conflict is detected.
- Precondition:
- The assignment is fully propagated w.r.t any previous post propagator.
- Parameters:
-
s The solver in which this post propagator is used. ctx The post propagator from which this post propagator is called or 0 if no other post propagator is currently active.
- Postcondition:
- s.queueSize() == 0 || s.hasConflict()
- Returns:
- false if propagation led to conflict, true otherwise
- Note:
- The function shall not call Solver::propagate() or any other function that would result in a recursive chain of propagate() calls. On the other hand, it shall call Solver::propagateUntil(this) after enqueuing new assignments to initiate propagation up to this propagator.
Typically, propagateFixpoint() should implemet a loop like this:
for (;;) { if (!assign_newly_implied_literals(s)){ return false; } if (s.queueSize() == 0) { return true; } if (!s.propagateUntil(this)) { return false; } }
Implemented in Clasp::MessageHandler, Clasp::SequentialSolve::InterruptHandler, Clasp::Lookahead, Clasp::DefaultUnfoundedCheck, and Clasp::Test::TestingPostProp.
| void Clasp::PostPropagator::reason | ( | Solver & | s, |
| Literal | p, | ||
| LitVec & | lits | ||
| ) | [protected, virtual] |
- Precondition:
- This constraint is the reason for p being true in s.
- Postcondition:
- The literals implying p were added to lits.
Implements Clasp::Constraint.
Reimplemented in Clasp::DefaultUnfoundedCheck.
Definition at line 50 of file constraint.cpp.
| void Clasp::PostPropagator::reset | ( | ) | [virtual] |
Aborts an active propagation operation.
The function reset() is called whenever propagation on the current decision level is stopped before a fixpoint is reached. In particular, a solver calls reset() when a conflict is detected during propagation.
- Note:
- The default implementation is a noop.
Reimplemented in Clasp::DefaultUnfoundedCheck, and Clasp::Test::TestingPostProp.
Definition at line 48 of file constraint.cpp.
Member Data Documentation
Definition at line 270 of file constraint.h.
The documentation for this class was generated from the following files: