clingo_propagator Struct Reference

Detailed Description

An instance of this struct has to be registered with a solver to implement a custom propagator.

Not all callbacks have to be implemented and can be set to NULL if not needed.

See also

Theory Propagation

Examples:

propagator.c.

Public Attributes
bool(*	init )(clingo_propagate_init_t *control, void *data)
	This function is called once before each solving step. More...
bool(*	propagate )(clingo_propagate_control_t *control, clingo_literal_t const *changes, size_t size, void *data)
	Can be used to propagate solver literals given a partial assignment. More...
bool(*	undo )(clingo_propagate_control_t *control, clingo_literal_t const *changes, size_t size, void *data)
	Called whenever a solver undoes assignments to watched solver literals. More...
bool(*	check )(clingo_propagate_control_t *control, void *data)
	This function is similar to clingo_propagate_control_propagate() but is only called on total assignments without a change set. More...

Member Data Documentation

bool(* clingo_propagator::check) (clingo_propagate_control_t *control, void *data)

This function is similar to clingo_propagate_control_propagate() but is only called on total assignments without a change set.

Note

This function is called even if no watches have been added.

Parameters

[in]	control	control object for the target solver
[in]	data	user data for the callback

Returns

whether the call was successful

See also

clingo_propagator_check_callback_t

bool(* clingo_propagator::init) (clingo_propagate_init_t *control, void *data)

This function is called once before each solving step.

It is used to map relevant program literals to solver literals, add watches for solver literals, and initialize the data structures used during propagation.

Note

This is the last point to access symbolic and theory atoms. Once the search has started, they are no longer accessible.

Parameters

[in]	control	control object for the target solver
[in]	data	user data for the callback

Returns

whether the call was successful

See also

clingo_propagator_init_callback_t

bool(* clingo_propagator::propagate) (clingo_propagate_control_t *control, clingo_literal_t const *changes, size_t size, void *data)

Can be used to propagate solver literals given a partial assignment.

Called during propagation with a non-empty array of watched solver literals that have been assigned to true since the last call to either propagate, undo, (or the start of the search) - the change set. Only watched solver literals are contained in the change set. Each literal in the change set is true w.r.t. the current assignment. clingo_propagate_control_add_clause() can be used to add clauses. If a clause is unit resulting, it can be propagated using clingo_propagate_control_propagate(). If the result of either of the two methods is false, the propagate function must return immediately.

The following snippet shows how to use the methods to add clauses and propagate consequences within the callback. The important point is to return true (true to indicate there was no error) if the result of either of the methods is false.

bool result;
clingo_literal_t clause[] = { ... };

// add a clause
if (!clingo_propagate_control_add_clause(control, clause, clingo_clause_type_learnt, &result) { return false; }
if (!result) { return true; }
// propagate its consequences
if (!clingo_propagate_control_propagate(control, &result) { return false; }
if (!result) { return true; }

// add further clauses and propagate them
...

return true;

Note

This function can be called from different solving threads. Each thread has its own assignment and id, which can be obtained using clingo_propagate_control_thread_id().

Parameters

[in]	control	control object for the target solver
[in]	changes	the change set
[in]	size	the size of the change set
[in]	data	user data for the callback

Returns

whether the call was successful

See also

clingo_propagator_propagate_callback_t

bool(* clingo_propagator::undo) (clingo_propagate_control_t *control, clingo_literal_t const *changes, size_t size, void *data)

Called whenever a solver undoes assignments to watched solver literals.

This callback is meant to update assignment dependent state in the propagator.

Note

No clauses must be propagated in this callback.

Parameters

[in]	control	control object for the target solver
[in]	changes	the change set
[in]	size	the size of the change set
[in]	data	user data for the callback

See also

clingo_propagator_undo_callback_t

---

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

• clingo.h