#include <constraint.h>
Public Member Functions | |
| virtual bool | handleMessages ()=0 |
| MessageHandler () | |
| virtual uint32 | priority () const |
| Shall return a value representing the priority of this propagator. | |
| virtual bool | propagateFixpoint (Solver &, PostPropagator *) |
| Shall enqueue and propagate new assignments implied by this propagator. | |
Detailed Description
Definition at line 359 of file constraint.h.
Constructor & Destructor Documentation
Definition at line 54 of file constraint.cpp.
Member Function Documentation
| virtual bool Clasp::MessageHandler::handleMessages | ( | ) | [pure virtual] |
Implemented in Clasp::SequentialSolve::InterruptHandler.
| virtual uint32 Clasp::MessageHandler::priority | ( | ) | const [inline, 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.
Implements Clasp::PostPropagator.
Definition at line 363 of file constraint.h.
| virtual bool Clasp::MessageHandler::propagateFixpoint | ( | Solver & | s, |
| PostPropagator * | ctx | ||
| ) | [inline, 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; } }
Implements Clasp::PostPropagator.
Reimplemented in Clasp::SequentialSolve::InterruptHandler.
Definition at line 364 of file constraint.h.
The documentation for this class was generated from the following files: