Detailed Description

Inspection of theory atoms occurring in ground logic programs.

During grounding, theory atoms get consecutive numbers starting with zero. The total number of theory atoms can be obtained using clingo_theory_atoms_size().

Attention: All structural information about theory atoms, elements, and terms is reset after solving. If afterward fresh theory atoms are grounded, previously used ids are reused.

For an example, see theory-atoms.c.

Typedefs
typedef int	clingo_theory_term_type_t
	Corresponding type to clingo_theory_term_type_e.

typedef struct clingo_theory_atoms	clingo_theory_atoms_t
	Container that stores theory atoms, elements, and terms (see clingo_control_theory_atoms()).

Enumerations
enum	clingo_theory_term_type_e { clingo_theory_term_type_tuple = 0, clingo_theory_term_type_list = 1, clingo_theory_term_type_set = 2, clingo_theory_term_type_function = 3, clingo_theory_term_type_number = 4, clingo_theory_term_type_symbol = 5 }
	Enumeration of theory term types. More...

Theory Term Inspection
CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_type (clingo_theory_atoms_t const atoms, clingo_id_t term, clingo_theory_term_type_t type)
	Get the type of the given theory term. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_number (clingo_theory_atoms_t const atoms, clingo_id_t term, int number)
	Get the number of the given numeric theory term. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_name (clingo_theory_atoms_t const atoms, clingo_id_t term, char const *name)
	Get the name of the given constant or function theory term. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_arguments (clingo_theory_atoms_t const atoms, clingo_id_t term, clingo_id_t const arguments, size_t size)
	Get the arguments of the given function theory term. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_to_string_size (clingo_theory_atoms_t const atoms, clingo_id_t term, size_t size)
	Get the size of the string representation of the given theory term (including the terminating 0). More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_term_to_string (clingo_theory_atoms_t const atoms, clingo_id_t term, char string, size_t size)
	Get the string representation of the given theory term. More...

Theory Element Inspection
CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_element_tuple (clingo_theory_atoms_t const atoms, clingo_id_t element, clingo_id_t const tuple, size_t size)
	Get the tuple (array of theory terms) of the given theory element. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_element_condition (clingo_theory_atoms_t const atoms, clingo_id_t element, clingo_literal_t const condition, size_t size)
	Get the condition (array of aspif literals) of the given theory element. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_element_condition_id (clingo_theory_atoms_t const atoms, clingo_id_t element, clingo_literal_t condition)
	Get the id of the condition of the given theory element. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_element_to_string_size (clingo_theory_atoms_t const atoms, clingo_id_t element, size_t size)
	Get the size of the string representation of the given theory element (including the terminating 0). More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_element_to_string (clingo_theory_atoms_t const atoms, clingo_id_t element, char string, size_t size)
	Get the string representation of the given theory element. More...

Theory Atom Inspection
CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_size (clingo_theory_atoms_t const atoms, size_t size)
	Get the total number of theory atoms. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_term (clingo_theory_atoms_t const atoms, clingo_id_t atom, clingo_id_t term)
	Get the theory term associated with the theory atom. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_elements (clingo_theory_atoms_t const atoms, clingo_id_t atom, clingo_id_t const elements, size_t size)
	Get the theory elements associated with the theory atom. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_has_guard (clingo_theory_atoms_t const atoms, clingo_id_t atom, bool has_guard)
	Whether the theory atom has a guard. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_guard (clingo_theory_atoms_t const atoms, clingo_id_t atom, char const connective, clingo_id_t term)
	Get the guard consisting of a theory operator and a theory term of the given theory atom. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_literal (clingo_theory_atoms_t const atoms, clingo_id_t atom, clingo_literal_t literal)
	Get the aspif literal associated with the given theory atom. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_to_string_size (clingo_theory_atoms_t const atoms, clingo_id_t atom, size_t size)
	Get the size of the string representation of the given theory atom (including the terminating 0). More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_theory_atoms_atom_to_string (clingo_theory_atoms_t const atoms, clingo_id_t atom, char string, size_t size)
	Get the string representation of the given theory atom. More...

Enumeration Type Documentation

◆ clingo_theory_term_type_e

enum clingo_theory_term_type_e

Enumeration of theory term types.

Enumerator
clingo_theory_term_type_tuple	a tuple term, e.g., `(1,2,3)`
clingo_theory_term_type_list	a list term, e.g., `[1,2,3]`
clingo_theory_term_type_set	a set term, e.g., `{1,2,3}`
clingo_theory_term_type_function	a function term, e.g., `f(1,2,3)`
clingo_theory_term_type_number	a number term, e.g., `42`
clingo_theory_term_type_symbol	a symbol term, e.g., `c`

Function Documentation

◆ clingo_theory_atoms_atom_elements()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_elements	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		clingo_id_t const **	elements,
		size_t *	size
	)

Get the theory elements associated with the theory atom.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the atom
[out]	elements	the resulting array of elements
[out]	size	the number of elements

Returns: whether the call was successful

◆ clingo_theory_atoms_atom_guard()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_guard	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		char const **	connective,
		clingo_id_t *	term
	)

Get the guard consisting of a theory operator and a theory term of the given theory atom.

Note: The lifetime of the string is tied to the current solve step.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the atom
[out]	connective	the resulting theory operator
[out]	term	the resulting term

Returns: whether the call was successful

◆ clingo_theory_atoms_atom_has_guard()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_has_guard	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		bool *	has_guard
	)

Whether the theory atom has a guard.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the atom
[out]	has_guard	whether the theory atom has a guard

Returns: whether the call was successful

Examples:: theory-atoms.c.

◆ clingo_theory_atoms_atom_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_literal	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		clingo_literal_t *	literal
	)

Get the aspif literal associated with the given theory atom.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the atom
[out]	literal	the resulting literal

Returns: whether the call was successful

Examples:: theory-atoms.c.

◆ clingo_theory_atoms_atom_term()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_term	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		clingo_id_t *	term
	)

Get the theory term associated with the theory atom.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the atom
[out]	term	the resulting term id

Returns: whether the call was successful

Examples:: theory-atoms.c.

◆ clingo_theory_atoms_atom_to_string()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_to_string	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		char *	string,
		size_t	size
	)

Get the string representation of the given theory atom.

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the element
[out]	string	the resulting string
[in]	size	the size of the string

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_runtime if the size is too small
clingo_error_bad_alloc

◆ clingo_theory_atoms_atom_to_string_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_to_string_size	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	atom,
		size_t *	size
	)

Get the size of the string representation of the given theory atom (including the terminating 0).

Parameters

[in]	atoms	container where the atom is stored
[in]	atom	id of the element
[out]	size	the resulting size

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc

◆ clingo_theory_atoms_element_condition()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_condition	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	element,
		clingo_literal_t const **	condition,
		size_t *	size
	)

Get the condition (array of aspif literals) of the given theory element.

Parameters

[in]	atoms	container where the element is stored
[in]	element	id of the element
[out]	condition	the resulting array of aspif literals
[out]	size	the number of term literals

Returns: whether the call was successful

◆ clingo_theory_atoms_element_condition_id()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_condition_id	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	element,
		clingo_literal_t *	condition
	)

Get the id of the condition of the given theory element.

Note: This id can be mapped to a solver literal using clingo_propagate_init_solver_literal(). This id is not (necessarily) an aspif literal; to get aspif literals use clingo_theory_atoms_element_condition().

Parameters

[in]	atoms	container where the element is stored
[in]	element	id of the element
[out]	condition	the resulting condition id

Returns: whether the call was successful

◆ clingo_theory_atoms_element_to_string()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_to_string	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	element,
		char *	string,
		size_t	size
	)

Get the string representation of the given theory element.

Parameters

[in]	atoms	container where the element is stored
[in]	element	id of the element
[out]	string	the resulting string
[in]	size	the size of the string

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_runtime if the size is too small
clingo_error_bad_alloc

◆ clingo_theory_atoms_element_to_string_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_to_string_size	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	element,
		size_t *	size
	)

Get the size of the string representation of the given theory element (including the terminating 0).

Parameters

[in]	atoms	container where the element is stored
[in]	element	id of the element
[out]	size	the resulting size

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc

◆ clingo_theory_atoms_element_tuple()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_tuple	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	element,
		clingo_id_t const **	tuple,
		size_t *	size
	)

Get the tuple (array of theory terms) of the given theory element.

Parameters

[in]	atoms	container where the element is stored
[in]	element	id of the element
[out]	tuple	the resulting array of term ids
[out]	size	the number of term ids

Returns: whether the call was successful

◆ clingo_theory_atoms_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_size	(	clingo_theory_atoms_t const *	atoms,
		size_t *	size
	)

Get the total number of theory atoms.

Parameters

[in]	atoms	the target
[out]	size	the resulting number

Returns: whether the call was successful

Examples:: theory-atoms.c.

◆ clingo_theory_atoms_term_arguments()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_arguments	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		clingo_id_t const **	arguments,
		size_t *	size
	)

Get the arguments of the given function theory term.

Precondition: The term must be of type clingo_theory_term_type_function.

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	arguments	the resulting arguments in form of an array of term ids
[out]	size	the number of arguments

Returns: whether the call was successful

◆ clingo_theory_atoms_term_name()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_name	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		char const **	name
	)

Get the name of the given constant or function theory term.

Note: The lifetime of the string is tied to the current solve step.

Precondition: The term must be of type clingo_theory_term_type_function or clingo_theory_term_type_symbol.

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	name	the resulting name

Returns: whether the call was successful

Examples:: theory-atoms.c.

◆ clingo_theory_atoms_term_number()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_number	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		int *	number
	)

Get the number of the given numeric theory term.

Precondition: The term must be of type clingo_theory_term_type_number.

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	number	the resulting number

Returns: whether the call was successful

◆ clingo_theory_atoms_term_to_string()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_to_string	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		char *	string,
		size_t	size
	)

Get the string representation of the given theory term.

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	string	the resulting string
[in]	size	the size of the string

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_runtime if the size is too small
clingo_error_bad_alloc

See also: clingo_theory_atoms_term_to_string_size()

◆ clingo_theory_atoms_term_to_string_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_to_string_size	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		size_t *	size
	)

Get the size of the string representation of the given theory term (including the terminating 0).

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	size	the resulting size

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc

◆ clingo_theory_atoms_term_type()

CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_type	(	clingo_theory_atoms_t const *	atoms,
		clingo_id_t	term,
		clingo_theory_term_type_t *	type
	)

Get the type of the given theory term.

Parameters

[in]	atoms	container where the term is stored
[in]	term	id of the term
[out]	type	the resulting type

Returns: whether the call was successful

Detailed Description

Typedefs

Enumerations

Theory Term Inspection

Theory Element Inspection

Theory Atom Inspection

Enumeration Type Documentation

◆ clingo_theory_term_type_e

Function Documentation

◆ clingo_theory_atoms_atom_elements()

◆ clingo_theory_atoms_atom_guard()

◆ clingo_theory_atoms_atom_has_guard()

◆ clingo_theory_atoms_atom_literal()

◆ clingo_theory_atoms_atom_term()

◆ clingo_theory_atoms_atom_to_string()

◆ clingo_theory_atoms_atom_to_string_size()

◆ clingo_theory_atoms_element_condition()

◆ clingo_theory_atoms_element_condition_id()

◆ clingo_theory_atoms_element_to_string()

◆ clingo_theory_atoms_element_to_string_size()

◆ clingo_theory_atoms_element_tuple()

◆ clingo_theory_atoms_size()

◆ clingo_theory_atoms_term_arguments()

◆ clingo_theory_atoms_term_name()

◆ clingo_theory_atoms_term_number()

◆ clingo_theory_atoms_term_to_string()

◆ clingo_theory_atoms_term_to_string_size()

◆ clingo_theory_atoms_term_type()