Clingo
Loading...
Searching...
No Matches
Public Attributes | List of all members
clingo_theory Struct Reference
C API » External Theory Support

A theory object to extend solving. More...

#include <theory.h>

Public Attributes

bool(* info )(void *self, clingo_string_t *name, int *major, int *minor, int *revision)
 Get the name and version of the theory.
 
void(* destroy )(void *self)
 Destroy the theory.
 
bool(* register_theory )(void *self, clingo_control_t *control)
 Register the theory with the given control object.
 
bool(* rewrite_ast )(void *self, clingo_ast_t *statement, clingo_theory_ast_callback_t callback, void *data)
 Rewrite the given ast for the theory.
 
bool(* prepare )(void *self, clingo_control_t *control)
 Prepare the theory.
 
bool(* register_options )(void *self, clingo_options_t *options)
 Register the theory's options with the given application options object.
 
bool(* validate_options )(void *self)
 Validate the options of the theory.
 
bool(* on_model )(void *self, clingo_model_t *model)
 Inform the theory that a model has been found.
 
bool(* on_stats )(void *self, clingo_stats_t *stats)
 Add the theory's statistics to the given maps.
 
bool(* lookup_symbol )(void *self, clingo_symbol_t symbol, size_t *index, bool *found)
 Get the integer index of a symbol assigned by the theory when a model is found.
 
bool(* assignment_next )(void *self, uint32_t thread_id, bool *init, size_t *index, bool *has_value)
 Get the next index that has a value.
 
bool(* assignment_get_value )(void *self, uint32_t thread_id, size_t index, clingo_symbol_t *symbol, clingo_theory_value_t *value, bool *has_value)
 Get the value assigned to the given index.
 
void * self
 The userdata for the first value to the callabcks in this struct.
 

Detailed Description

A theory object to extend solving.

Member Data Documentation

◆ assignment_get_value

bool(* clingo_theory::assignment_get_value) (void *self, uint32_t thread_id, size_t index, clingo_symbol_t *symbol, clingo_theory_value_t *value, bool *has_value)

Get the value assigned to the given index.

Note that the caller of this function is responsible to release symbols.

Parameters
[in]selfthe self pointer
[in]thread_idthe thread that holds the assignment
[in]indexthe index to lookup
[out]symbolthe resulting symbol (optional)
[out]valuethe resulting value (optional)
[out]has_valuewhether the index has a value (optional)
Returns
whether the call was successful

◆ assignment_next

bool(* clingo_theory::assignment_next) (void *self, uint32_t thread_id, bool *init, size_t *index, bool *has_value)

Get the next index that has a value.

If init is true, an index to the first value in the assignment is returned and the value of init is set to false.

The returned index has a value if has_value is true. Otherwise, iteration must be stopped.

Parameters
[in]selfthe self pointer
[in]thread_idthe thread that holds the assignment
[in,out]initwhether to advance or initialize the index
[out]indexthe resulting index
[out]has_valuewhether the index has a value
Returns
whether the call was successful

◆ destroy

void(* clingo_theory::destroy) (void *self)

Destroy the theory.

Parameters
[in]selfthe self pointer

◆ info

bool(* clingo_theory::info) (void *self, clingo_string_t *name, int *major, int *minor, int *revision)

Get the name and version of the theory.

Parameters
[in]selfthe self pointer
[out]namethe name of the theory (optional)
[out]majorthe major version component (optional)
[out]minorthe minor version component (optional)
[out]revisionthe revision version component (optional)
Returns
whether the call was successful

◆ lookup_symbol

bool(* clingo_theory::lookup_symbol) (void *self, clingo_symbol_t symbol, size_t *index, bool *found)

Get the integer index of a symbol assigned by the theory when a model is found.

Using indices allows for efficent retrieval of values.

Parameters
[in]selfthe self pointer
[in]symbolthe symbol to lookup
[out]indexthe resulting index (optional)
[out]foundwhether the symbol has been found (optional)
Returns
whether the call was successful

◆ on_model

bool(* clingo_theory::on_model) (void *self, clingo_model_t *model)

Inform the theory that a model has been found.

Parameters
[in]selfthe self pointer
[in]modelthe current model
Returns
whether the call was successful

◆ on_stats

bool(* clingo_theory::on_stats) (void *self, clingo_stats_t *stats)

Add the theory's statistics to the given maps.

Parameters
[in]selfthe self pointer
[in]statsthe statistics object
Returns
whether the call was successful

◆ prepare

bool(* clingo_theory::prepare) (void *self, clingo_control_t *control)

Prepare the theory.

Must be called between ground and solve.

Parameters
[in]selfthe self pointer
[in]controlthe control object
Returns
whether the call was successful

◆ register_options

bool(* clingo_theory::register_options) (void *self, clingo_options_t *options)

Register the theory's options with the given application options object.

Parameters
[in]selfthe self pointer
[in]controlthe options object
Returns
whether the call was successful

◆ register_theory

bool(* clingo_theory::register_theory) (void *self, clingo_control_t *control)

Register the theory with the given control object.

A theory might register propagators or add theory definitions here.

Parameters
[in]selfthe self pointer
[in]controlthe control object
Returns
whether the call was successful

◆ rewrite_ast

bool(* clingo_theory::rewrite_ast) (void *self, clingo_ast_t *statement, clingo_theory_ast_callback_t callback, void *data)

Rewrite the given ast for the theory.

A theory might rewrite theory atoms.

Parameters
[in]selfthe self pointer
[in]statementthe statement to rewrite
[in]callbackthe callback to pass rewritten statements to
[in]datathe user data for the callback
Returns
whether the call was successful

◆ validate_options

bool(* clingo_theory::validate_options) (void *self)

Validate the options of the theory.

Parameters
[in]selfthe self pointer
Returns
whether the call was successful
The documentation for this struct was generated from the following file: