Inheritance diagram for Clasp::Test::TestingPostProp:

Public Member Functions
bool	init (Solver &)
	Called during initialization of s.
uint32	priority () const
	Shall return a value representing the priority of this propagator.
bool	propagateFixpoint (Solver &s, PostPropagator *)
	Shall enqueue and propagate new assignments implied by this propagator.
void	reset ()
	Aborts an active propagation operation.
	TestingPostProp (bool cfl, uint32 p=PostPropagator::priority_class_simple)
Public Attributes
bool	conflict
bool	deleteOnProp
int	inits
uint32	prio
int	props
int	resets

Detailed Description

Definition at line 58 of file solver_test.cpp.

Constructor & Destructor Documentation

Clasp::Test::TestingPostProp::TestingPostProp	(	bool	cfl,
		uint32	p = `PostPropagator::priority_class_simple`
	)		`[inline, explicit]`

Definition at line 59 of file solver_test.cpp.

Member Function Documentation

bool Clasp::Test::TestingPostProp::init ( Solver & s ) [inline, virtual]

Called during initialization of s.

Note:: During initialization a post propagator may assign variables but it must not yet propagate them.

Reimplemented from Clasp::PostPropagator.

Definition at line 72 of file solver_test.cpp.

uint32 Clasp::Test::TestingPostProp::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 73 of file solver_test.cpp.

bool Clasp::Test::TestingPostProp::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.

Definition at line 60 of file solver_test.cpp.

void Clasp::Test::TestingPostProp::reset ( ) [inline, 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.