Clingo::Propagator Class Reference

Interface for user-defined propagators. More...

#include <propagate.hh>

Inheritance diagram for Clingo::Propagator:

Public Member Functions
	Propagator ()=default
	The default constructor.
	Propagator (Propagator &&other)=delete
	Disable copy and move operations.
virtual	~Propagator ()=default
	The default destructor.
void	init (PropagateInit init)
	Callback to initialize the propagator before each solving step.
void	propagate (PropagateControl ctl, ProgramLiteralSpan changes)
	Callback to propagate consequences of the given literals.
void	undo (ProgramId thread_id, Assignment assignment, ProgramLiteralSpan changes)
	Called when the solver backtracks to a previous decision level.
void	check (PropagateControl ctl)
	Callback that is called on propagation fixpoints or total assignments.

Detailed Description

Interface for user-defined propagators.

Member Function Documentation

check()

void Clingo::Propagator::check ( PropagateControl  ctl )

inline

Callback that is called on propagation fixpoints or total assignments.

Clingo::PropagateInit::check_mode() can be used to control when this callback is called.

Like in Clingo::Propagator::Propagate(), a propagator can add clauses here to propagate consequences or discard the current assignment.

Parameters

ctl	the propagate control object

init()

void Clingo::Propagator::init ( PropagateInit  init )

inline

Callback to initialize the propagator before each solving step.

Parameters

init	the initialization object

propagate()

void Clingo::Propagator::propagate ( PropagateControl  ctl, ProgramLiteralSpan  changes  )

inline

Callback to propagate consequences of the given literals.

The function is only called for watched literals that were assigned on the current decision level.

A propagator can add clauses here to propagate consequences of the underlying theory.

Parameters

ctl	the propagate control object
changes	the literals that were assigned on the current decision level

undo()

void Clingo::Propagator::undo ( ProgramId  thread_id, Assignment  assignment, ProgramLiteralSpan  changes  )

inline

Called when the solver backtracks to a previous decision level.

The function is called with literals from all previous propagate calls on the same decision level.

Clingo::PropagateInit::undo_mode() can be used to control when this function is called.

Parameters

thread_id	the id of the current solver thread
assignment	the current assignment of the solver
changes	the literals that were assigned on the current decision level

---

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

• clingo/propagate.hh