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.
auto	operator= (Propagator &&other) -> Propagator &=delete
	Disable copy and move operations.
virtual	~Propagator ()=default
	The destructor.
void	init (Assignment assignment, PropagateInit init)
	Callback to initialize the propagator before each solving step.
void	attach (Assignment assignment, PropagateControl ctl)
	Callback to initialize/setup thread-specific data for the propagator.
void	propagate (Assignment assignment, PropagateControl ctl, ProgramLiteralSpan changes)
	Callback to propagate consequences of the given literals.
void	undo (Assignment assignment, ProgramLiteralSpan changes)
	Called when the solver backtracks to a previous decision level.
void	check (Assignment assignment, PropagateControl ctl)
	Callback that is called on propagation fixpoints or total assignments.

Detailed Description

Interface for user-defined propagators.

Member Function Documentation

attach()

void Clingo::Propagator::attach ( Assignment  assignment, PropagateControl  ctl  )

inline

Callback to initialize/setup thread-specific data for the propagator.

This function is called once for each solving thread before solving of the current step is started.

Parameters

assignment	the current assignment of the solver
ctl	the propagate control object

check()

void Clingo::Propagator::check ( Assignment  assignment, 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

assignment	the current assignment of the solver
ctl	the propagate control object

init()

void Clingo::Propagator::init ( Assignment  assignment, PropagateInit  init  )

inline

Callback to initialize the propagator before each solving step.

Parameters

assignment	the current assignment of the solver
init	the initialization object

propagate()

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

inline

Callback to propagate consequences of the given literals.

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

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

Parameters

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

undo()

void Clingo::Propagator::undo ( 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

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