Clasp::SequentialSolve::InterruptHandler Struct Reference

Inheritance diagram for Clasp::SequentialSolve::InterruptHandler:

List of all members.

Public Member Functions
bool	attach (Solver &s)
void	detach ()
bool	handleMessages ()
	InterruptHandler ()
bool	propagateFixpoint (Solver &, PostPropagator *)
	Shall enqueue and propagate new assignments implied by this propagator.
bool	terminate ()
bool	terminated () const
Public Attributes
Solver *	solver
Clasp::atomic< int >	term

---

Detailed Description

Definition at line 269 of file solve_algorithms.cpp.

---

Constructor & Destructor Documentation

Clasp::SequentialSolve::InterruptHandler::InterruptHandler

(

)

[inline]

Definition at line 270 of file solve_algorithms.cpp.

---

Member Function Documentation

bool Clasp::SequentialSolve::InterruptHandler::attach

(

Solver &

s

)

[inline]

Definition at line 273 of file solve_algorithms.cpp.

void Clasp::SequentialSolve::InterruptHandler::detach

(

)

[inline]

Definition at line 274 of file solve_algorithms.cpp.

bool Clasp::SequentialSolve::InterruptHandler::handleMessages

(

)

[inline, virtual]

Implements Clasp::MessageHandler.

Definition at line 275 of file solve_algorithms.cpp.

bool Clasp::SequentialSolve::InterruptHandler::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; }
 }

Reimplemented from Clasp::MessageHandler.

Definition at line 276 of file solve_algorithms.cpp.

bool Clasp::SequentialSolve::InterruptHandler::terminate

(

)

[inline]

Definition at line 272 of file solve_algorithms.cpp.

bool Clasp::SequentialSolve::InterruptHandler::terminated

(

)

const [inline]

Definition at line 271 of file solve_algorithms.cpp.

---

Member Data Documentation

Solver* Clasp::SequentialSolve::InterruptHandler::solver

Definition at line 277 of file solve_algorithms.cpp.

Clasp::atomic<int> Clasp::SequentialSolve::InterruptHandler::term

Definition at line 278 of file solve_algorithms.cpp.

---

The documentation for this struct was generated from the following file:

• solve_algorithms.cpp