clingo_theory Struct Reference

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(*	configure )(void *self, char const *key, size_t key_size, char const *value, size_t value_size)
	Configure the theory passing key value pairs.
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]	self	the self pointer
[in]	thread_id	the thread that holds the assignment
[in]	index	the index to lookup
[out]	symbol	the resulting symbol (optional)
[out]	value	the resulting value (optional)
[out]	has_value	whether the index has a value (optional)

Returns

wether 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]	self	the self pointer
[in]	thread_id	the thread that holds the assignment
[in,out]	init	whether to advance or initialize the index
[out]	index	the resulting index
[out]	has_value	whether the index has a value

Returns

wether the call was successful

configure

bool(* clingo_theory::configure) (void *self, char const *key, size_t key_size, char const *value, size_t value_size)

Configure the theory passing key value pairs.

Parameters

[in]	self	the self pointer
[in]	key	the name of the option to set
[in]	key_size	the size of the name
[in]	value	the value to set
[in]	value_size	the size of the value

Returns

wether the call was successful

destroy

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

Destroy the theory.

Parameters

[in]

self

the 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]	self	the self pointer
[out]	name	the name of the theory (optional)
[out]	major	the major version component (optional)
[out]	minor	the minor version component (optional)
[out]	revision	the revision version component (optional)

Returns

wether 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]	self	the self pointer
[in]	symbol	the symbol to lookup
[out]	index	the resulting index (optional)
[out]	found	whether the symbol has been found (optional)

Returns

wether 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]	self	the self pointer
[in]	model	the current model

Returns

wether 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]	self	the self pointer
[in]	stats	the statistics object

Returns

wether 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]	self	the self pointer
[in]	control	the control object

Returns

wether 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]	self	the self pointer
[in]	control	the options object

Returns

wether 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]	self	the self pointer
[in]	control	the control object

Returns

wether 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]	self	the self pointer
[in]	statement	the statement to rewrite
[in]	callback	the callback to pass rewritten statements to
[in]	data	the user data for the callback

Returns

wether the call was successful

validate_options

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

Validate the options of the theory.

Parameters

[in]

self

the self pointer

Returns

wether the call was successful

---

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

• clingo/theory.h