Clasp::PostPropagator Class Reference

Base class for post propagators. More...

#include <constraint.h>

Inheritance diagram for Clasp::PostPropagator:

Collaboration diagram for Clasp::PostPropagator:

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
	PostPropagator ()
virtual	~PostPropagator ()
virtual uint32	priority () const =0
	Shall return a value representing the priority of this propagator. More...
virtual bool	init (Solver &s)
	Called during initialization of s. More...
virtual bool	propagateFixpoint (Solver &s, PostPropagator *ctx)=0
	Shall enqueue and propagate new assignments implied by this propagator. More...
virtual void	reset ()
	Aborts an active propagation operation. More...
virtual bool	isModel (Solver &s)
	Is the current total assignment a model? More...
Public Member Functions inherited from Clasp::Constraint
	Constraint ()
virtual void	destroy (Solver *s=0, bool detach=false)
	Default is to call delete this. More...
virtual ConstraintType	type () const
	Returns the type of this constraint. More...
virtual bool	minimize (Solver &s, Literal p, CCMinRecursive *rec)
virtual void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint. More...
virtual bool	simplify (Solver &s, bool reinit=false)
virtual uint32	estimateComplexity (const Solver &s) const
	Returns an estimate of the constraint's complexity relative to a clause (complexity = 1). More...
virtual ClauseHead *	clause ()
	Shall return this if constraint is a clause, otherwise 0. More...
virtual bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s. More...

Public Attributes
PostPropagator *	next

Protected Member Functions
Constraint *	cloneAttach (Solver &)
	PostPropagators are not clonable by default. More...
PropResult	propagate (Solver &, Literal, uint32 &)
void	reason (Solver &, Literal, LitVec &)
Protected Member Functions inherited from Clasp::Constraint
virtual	~Constraint ()

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).

Member Enumeration Documentation

enum Clasp::PostPropagator::Priority

Default priorities for post propagators.

Enumerator
priority_class_simple	Starting priority of simple post propagators.
priority_reserved_msg	Reserved priority for message/termination handlers (if any).
priority_reserved_ufs	Reserved priority for the default unfounded set checker (if any).
priority_reserved_look	Reserved priority for the default lookahead operator (if any).
priority_class_general	Priortiy of extended post propagators.

Constructor & Destructor Documentation

Clasp::PostPropagator::PostPropagator

(

)

Clasp::PostPropagator::~PostPropagator ( )

virtual

Member Function Documentation

Constraint* Clasp::PostPropagator::cloneAttach ( Solver &  )

inlineprotectedvirtual

PostPropagators are not clonable by default.

Implements Clasp::Constraint.

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, and Clasp::DefaultUnfoundedCheck.

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.

Here is the call graph for this function:

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, and Clasp::DefaultUnfoundedCheck.

Constraint::PropResult Clasp::PostPropagator::propagate ( Solver &  s, Literal  p, uint32 &  data  )

protectedvirtual

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.

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, and Clasp::DefaultUnfoundedCheck.

void Clasp::PostPropagator::reason ( Solver &  s, Literal  p, LitVec &  lits  )

protectedvirtual

Precondition

This constraint is the reason for p being true in s.

Postcondition

The literals implying p were added to lits.

Implements Clasp::Constraint.

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.

Member Data Documentation

PostPropagator* Clasp::PostPropagator::next

---

The documentation for this class was generated from the following files:

• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/constraint.h
• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/constraint.cpp