Clingo C API
C API for clingo providing high level functions to control grounding and solving.
Typedefs | Enumerations
Theory Atom Inspection

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

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]atomscontainer where the atom is stored
[in]atomid of the atom
[out]elementsthe resulting array of elements
[out]sizethe 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]atomscontainer where the atom is stored
[in]atomid of the atom
[out]connectivethe resulting theory operator
[out]termthe 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]atomscontainer where the atom is stored
[in]atomid of the atom
[out]has_guardwhether 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]atomscontainer where the atom is stored
[in]atomid of the atom
[out]literalthe 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]atomscontainer where the atom is stored
[in]atomid of the atom
[out]termthe 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]atomscontainer where the atom is stored
[in]atomid of the element
[out]stringthe resulting string
[in]sizethe size of the string
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]atomscontainer where the atom is stored
[in]atomid of the element
[out]sizethe resulting size
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]atomscontainer where the element is stored
[in]elementid of the element
[out]conditionthe resulting array of aspif literals
[out]sizethe 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]atomscontainer where the element is stored
[in]elementid of the element
[out]conditionthe 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]atomscontainer where the element is stored
[in]elementid of the element
[out]stringthe resulting string
[in]sizethe size of the string
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]atomscontainer where the element is stored
[in]elementid of the element
[out]sizethe resulting size
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]atomscontainer where the element is stored
[in]elementid of the element
[out]tuplethe resulting array of term ids
[out]sizethe 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]atomsthe target
[out]sizethe 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]atomscontainer where the term is stored
[in]termid of the term
[out]argumentsthe resulting arguments in form of an array of term ids
[out]sizethe 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]atomscontainer where the term is stored
[in]termid of the term
[out]namethe 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]atomscontainer where the term is stored
[in]termid of the term
[out]numberthe 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]atomscontainer where the term is stored
[in]termid of the term
[out]stringthe resulting string
[in]sizethe size of the string
Returns
whether the call was successful; might set one of the following error codes:
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]atomscontainer where the term is stored
[in]termid of the term
[out]sizethe resulting size
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]atomscontainer where the term is stored
[in]termid of the term
[out]typethe resulting type
Returns
whether the call was successful