Struct clingo_sys::clingo_propagator

#[repr(C)]
pub struct clingo_propagator {
    pub init: Option<unsafe extern "C" fn(init: *mut clingo_propagate_init_t, data: *mut c_void) -> bool>,
    pub propagate: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, changes: *const clingo_literal_t, size: usize, data: *mut c_void) -> bool>,
    pub undo: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, changes: *const clingo_literal_t, size: usize, data: *mut c_void) -> bool>,
    pub check: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, data: *mut c_void) -> bool>,
}

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 Propagator

Fields

init: Option<unsafe extern "C" fn(init: *mut clingo_propagate_init_t, data: *mut c_void) -> bool>

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.

@param[in] init initizialization object @param[in] data user data for the callback @return whether the call was successful @see ::clingo_propagator_init_callback_t

propagate: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, changes: *const clingo_literal_t, size: usize, data: *mut c_void) -> bool>

Can be used to propagate solver literals given a @link clingo_assignment_t partial assignment@endlink.

Called during propagation with a non-empty array of @link clingo_propagate_init_add_watch() watched solver literals@endlink 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 @link clingo_assignment_t assignment@endlink. @ref clingo_propagate_control_add_clause() can be used to add clauses. If a clause is unit resulting, it can be propagated using @ref 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 @ref clingo_propagate_control_thread_id().

@param[in] control control object for the target solver @param[in] changes the change set @param[in] size the size of the change set @param[in] data user data for the callback @return whether the call was successful @see ::clingo_propagator_propagate_callback_t

undo: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, changes: *const clingo_literal_t, size: usize, data: *mut c_void) -> bool>

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.

@param[in] control control object for the target solver @param[in] changes the change set @param[in] size the size of the change set @param[in] data user data for the callback @see ::clingo_propagator_undo_callback_t

check: Option<unsafe extern "C" fn(control: *mut clingo_propagate_control_t, data: *mut c_void) -> bool>

This function is similar to @ref 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 @ref clingo_propagate_init_set_check_mode() function.

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

@param[in] control control object for the target solver @param[in] data user data for the callback @return whether the call was successful @see ::clingo_propagator_check_callback_t

Trait Implementations

impl Clone for clingo_propagator

fn clone(&self) -> clingo_propagator

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for clingo_propagator

impl Debug for clingo_propagator

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.