Clingo
Loading...
Searching...
No Matches
Public Attributes | List of all members
clingo_propagator Struct Reference
C API » Grounding and Solving » Theory Propagation

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

#include <propagate.h>

Public Attributes

bool(* init )(clingo_assignment_t const *assignment, clingo_propagate_init_t *init, void *data)
 This function is called once before each solving step.
 
bool(* attach )(clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data)
 This function is called once for each solving thread before solving of the current step is started.
 
bool(* propagate )(clingo_assignment_t const *assignment, 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.
 
void(* undo )(clingo_assignment_t const *assignment, clingo_literal_t const *changes, size_t size, void *data)
 Called whenever a solver undoes assignments to watched solver literals.
 
bool(* check )(clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data)
 This function is similar to clingo_propagate_control_propagate() but is called without a change set on propagation fixpoints.
 
bool(* decide )(clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, clingo_literal_t *decision)
 This function allows a propagator to implement domain-specific heuristics.
 
void(* free )(void *data)
 Free the propagator.
 

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
Propagator

Member Data Documentation

◆ attach

bool(* clingo_propagator::attach) (clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data)

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

It can be used to add thread-specific watches and literals, or initialize thread-specific data structures.

Attention
Literals and watches added in this function are only valid within the current solving thread. Furthermore, added literals and clauses involving such literals are deleted after the current search.
Parameters
[in]assignmentthe current assignment of the target solver
[in]controlcontrol object for the target solver
[in]datauser data for the callback
Returns
whether the call was successful
See also
clingo_propagator_init_callback_t

◆ check

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

This function is similar to clingo_propagate_control_propagate() but is called without a change set on propagation fixpoints.

When exactly this function is called, can be configured using the clingo_propagate_init_set_check_mode() function.

Note
This function is called even if no watches have been added.
Parameters
[in]assignmentcurrent assignment of the target solver
[in]controlcontrol object for the target solver
[in]datauser data for the callback
Returns
whether the call was successful
See also
clingo_propagator_check_callback_t

◆ decide

bool(* clingo_propagator::decide) (clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, clingo_literal_t *decision)

This function allows a propagator to implement domain-specific heuristics.

It is called whenever propagation reaches a fixed point and should return a free solver literal that is to be assigned true. In case multiple propagators are registered, this function can return 0 to let a propagator registered later make a decision. If all propagators return 0, then the fallback literal is used.

Parameters
[in]assignmentthe assignment of the solver
[in]fallbackthe literal chosen by the solver's heuristic
[in]datauser data for the callback
[out]decisionthe literal to make true
Returns
whether the call was successful

◆ free

void(* clingo_propagator::free) (void *data)

Free the propagator.

Parameters
[in]datauser data for the callback

◆ init

bool(* clingo_propagator::init) (clingo_assignment_t const *assignment, clingo_propagate_init_t *init, 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]assignmentthe current assignment
[in]initinitialization object
[in]datauser data for the callback
Returns
whether the call was successful
See also
clingo_propagator_init_callback_t

◆ propagate

bool(* clingo_propagator::propagate) (clingo_assignment_t const *assignment, 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;
clingo_literal_t
int32_t clingo_literal_t
Signed integer type used for aspif and solver literals.
Definition core.h:73
clingo_propagate_control_propagate
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_propagate(clingo_propagate_control_t *control, bool *result)
Propagate implied literals (resulting from added clauses).
clingo_propagate_control_add_clause
CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_clause(clingo_propagate_control_t *control, clingo_literal_t const *literals, size_t size, clingo_clause_type_t type, bool *result)
Add the given clause to the solver.
clingo_clause_type_learnt
@ clingo_clause_type_learnt
clause is subject to the solvers deletion policy
Definition propagate.h:366
Note
This function can be called from different solving threads. Each thread has its own assignment and id, where thread ids are consecutive numbers starting with zero.
Parameters
[in]assignmentcurrent assignment of the target solver
[in]controlcontrol object for the target solver
[in]changesthe change set
[in]sizethe size of the change set
[in]datauser data for the callback
Returns
whether the call was successful
See also
clingo_propagator_propagate_callback_t

◆ undo

void(* clingo_propagator::undo) (clingo_assignment_t const *assignment, 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.

Parameters
[in]assignmentcurrent assignment of the target solver
[in]changesthe change set
[in]sizethe size of the change set
[in]datauser data for the callback
Returns
whether the call was successful
See also
clingo_propagator_undo_callback_t
The documentation for this struct was generated from the following file: