Clingo C API
C API for clingo providing high level functions to control grounding and solving.
Modules | Classes | Typedefs | Enumerations | Enumerator | Functions
Grounding and Solving

Detailed Description

Functions to control the grounding and solving process.

For an example, see control.c.

Modules

 Model Inspection
 Inspection of models and a high-level interface to add constraints during solving.
 
 Iterative Solving
 Iterative enumeration of models (without using callbacks).
 
 Asynchronous Solving
 Solve in the background and notify about new models.
 
 Symbolic Atom Inspection
 Inspection of atoms occurring in ground logic programs.
 
 Theory Atom Inspection
 Inspection of theory atoms occurring in ground logic programs.
 
 Theory Propagation
 Extend the search with propagators for arbitrary theories.
 
 Program Building
 Add non-ground program representations (ASTs) to logic programs or extend the ground (aspif) program.
 
 Solver Configuration
 Configuration of search and enumeration algorithms.
 
 Statistics
 Inspect search and problem statistics.
 

Classes

struct  clingo_part
 Struct used to specify the program parts that have to be grounded. More...
 

Typedefs

typedef struct clingo_control clingo_control_t
 Control object holding grounding and solving state.
 
typedef struct clingo_part clingo_part_t
 Struct used to specify the program parts that have to be grounded. More...
 
typedef bool clingo_symbol_callback_t(clingo_symbol_t const *symbols, size_t symbols_size, void *data)
 Callback function to inject symbols. More...
 
typedef bool clingo_ground_callback_t(clingo_location_t location, char const *name, clingo_symbol_t const *arguments, size_t arguments_size, void *data, clingo_symbol_callback_t *symbol_callback, void *symbol_callback_data)
 Callback function to implement external functions. More...
 
typedef bool clingo_model_callback_t(clingo_model_t *model, void *data, bool *goon)
 Callback function to intercept models. More...
 
typedef bool clingo_finish_callback_t(clingo_solve_result_bitset_t result, void *data)
 Callback function called at the end of an asynchronous solve operation. More...
 
typedef unsigned clingo_solve_result_bitset_t
 Corresponding type to clingo_solve_result. More...
 

Enumerations

enum  clingo_solve_result { clingo_solve_result_satisfiable = 1, clingo_solve_result_unsatisfiable = 2, clingo_solve_result_exhausted = 4, clingo_solve_result_interrupted = 8 }
 Enumeration of bit masks for solve call results. More...
 

Functions

bool clingo_control_new (char const *const *arguments, size_t arguments_size, clingo_logger_t *logger, void *logger_data, unsigned message_limit, clingo_control_t **control)
 Create a new control object. More...
 
void clingo_control_free (clingo_control_t *control)
 Free a control object created with clingo_control_new(). More...
 

Grounding Functions

bool clingo_control_load (clingo_control_t *control, char const *file)
 Extend the logic program with a program in a file. More...
 
bool clingo_control_add (clingo_control_t *control, char const *name, char const *const *parameters, size_t parameters_size, char const *program)
 Extend the logic program with the given non-ground logic program in string form. More...
 
bool clingo_control_ground (clingo_control_t *control, clingo_part_t const *parts, size_t parts_size, clingo_ground_callback_t *ground_callback, void *ground_callback_data)
 Ground the selected parts of the current (non-ground) logic program. More...
 

Solving Functions

bool clingo_control_solve (clingo_control_t *control, clingo_model_callback_t *model_callback, void *model_callback_data, clingo_symbolic_literal_t const *assumptions, size_t assumptions_size, clingo_solve_result_bitset_t *result)
 Solve the currently grounded logic program. More...
 
bool clingo_control_solve_iteratively (clingo_control_t *control, clingo_symbolic_literal_t const *assumptions, size_t assumptions_size, clingo_solve_iteratively_t **handle)
 Solve the currently grounded logic program enumerating models iteratively. More...
 
bool clingo_control_solve_async (clingo_control_t *control, clingo_model_callback_t *model_callback, void *model_callback_data, clingo_finish_callback_t *finish_callback, void *finish_callback_data, clingo_symbolic_literal_t const *assumptions, size_t assumptions_size, clingo_solve_async_t **handle)
 Solve the currently grounded logic program asynchronously in the background. More...
 
bool clingo_control_cleanup (clingo_control_t *control)
 Clean up the domains of clingo's grounding component using the solving component's top level assignment. More...
 
bool clingo_control_assign_external (clingo_control_t *control, clingo_symbol_t atom, clingo_truth_value_t value)
 Assign a truth value to an external atom. More...
 
bool clingo_control_release_external (clingo_control_t *control, clingo_symbol_t atom)
 Release an external atom. More...
 
bool clingo_control_register_propagator (clingo_control_t *control, clingo_propagator_t propagator, void *data, bool sequential)
 Register a custom propagator with the control object. More...
 
bool clingo_control_statistics (clingo_control_t *control, clingo_statistics_t **statistics)
 Get a statistics object to inspect solver statistics. More...
 
void clingo_control_interrupt (clingo_control_t *control)
 Interrupt the active solve call (or the following solve call right at the beginning). More...
 

Configuration Functions

bool clingo_control_configuration (clingo_control_t *control, clingo_configuration_t **configuration)
 Get a configuration object to change the solver configuration. More...
 
bool clingo_control_use_enumeration_assumption (clingo_control_t *control, bool enable)
 Configure how learnt constraints are handled during enumeration. More...
 

Program Inspection Functions

bool clingo_control_get_const (clingo_control_t *control, char const *name, clingo_symbol_t *symbol)
 Return the symbol for a constant definition of form: #const name = symbol. More...
 
bool clingo_control_has_const (clingo_control_t *control, char const *name, bool *exists)
 Check if there is a constant definition for the given constant. More...
 
bool clingo_control_symbolic_atoms (clingo_control_t *control, clingo_symbolic_atoms_t **atoms)
 Get an object to inspect symbolic atoms (the relevant Herbrand base) used for grounding. More...
 
bool clingo_control_theory_atoms (clingo_control_t *control, clingo_theory_atoms_t **atoms)
 Get an object to inspect theory atoms that occur in the grounding. More...
 

Program Modification Functions

bool clingo_control_backend (clingo_control_t *control, clingo_backend_t **backend)
 Get an object to add ground directives to the program. More...
 
bool clingo_control_program_builder (clingo_control_t *control, clingo_program_builder_t **builder)
 Get an object to add non-ground directives to the program. More...
 

Typedef Documentation

typedef bool clingo_finish_callback_t(clingo_solve_result_bitset_t result, void *data)

Callback function called at the end of an asynchronous solve operation.

If a (non-recoverable) clingo API function fails in this callback, its error code shall be returned. In case of errors not related to clingo, this function can return clingo_error_unknown to stop solving with an error.

Parameters
[in]resultresult of the solve call
[in]datauser data of the callback
Returns
whether the call was successful
See also
clingo_control_solve_async()
Examples:
solve-async.c.
typedef bool clingo_ground_callback_t(clingo_location_t location, char const *name, clingo_symbol_t const *arguments, size_t arguments_size, void *data, clingo_symbol_callback_t *symbol_callback, void *symbol_callback_data)

Callback function to implement external functions.

If an external function of form @name(parameters) occurs in a logic program, then this function is called with its location, name, parameters, and a callback to inject symbols as arguments. The callback can be called multiple times; all symbols passed are injected.

If a (non-recoverable) clingo API function fails in this callback, for example, the symbol callback, its error code shall be returned. In case of errors not related to clingo, this function can return clingo_error_unknown to stop grounding with an error.

Parameters
[in]locationlocation from which the external function was called
[in]namename of the called external function
[in]argumentsarguments of the called external function
[in]arguments_sizenumber of arguments
[in]datauser data of the callback
[in]symbol_callbackfunction to inject symbols
[in]symbol_callback_datauser data for the symbol callback (must be passed untouched)
Returns
whether the call was successful
See also
clingo_control_ground()

The following example implements the external function @f() returning 42.

bool
ground_callback(clingo_location_t location,
char const *name,
clingo_symbol_t const *arguments,
size_t arguments_size,
void *data,
clingo_symbol_callback_t *symbol_callback,
void *symbol_callback_data) {
if (strcmp(name, "f") == 0 && arguments_size == 0) {
return symbol_callback(&sym, 1, symbol_callback_data);
}
clingo_set_error(clingo_error_runtime, "function not found");
return false;
}
typedef bool clingo_model_callback_t(clingo_model_t *model, void *data, bool *goon)

Callback function to intercept models.

The model callback is invoked once for each model found by clingo (asynchronously).

If a (non-recoverable) clingo API function fails in this callback, its error code shall be returned. In case of errors not related to clingo, clingo_error_unknown, this function can return clingo_error_unknown to stop solving with an error.

Parameters
[in]modelthe current model
[in]datauser data of the callback
[out]goonwhether to continue search
Returns
whether the call was successful
See also
clingo_control_solve()
clingo_control_solve_async()
Examples:
model.c.
typedef struct clingo_part clingo_part_t

Struct used to specify the program parts that have to be grounded.

Programs may be structured into parts, which can be grounded independently with clingo_control_ground. Program parts are mainly interesting for incremental grounding and multi-shot solving. For single-shot solving, program parts are not needed.

Note
Parts of a logic program without an explicit #program specification are by default put into a program called base without arguments.
See also
clingo_control_ground()

Corresponding type to clingo_solve_result.

typedef bool clingo_symbol_callback_t(clingo_symbol_t const *symbols, size_t symbols_size, void *data)

Callback function to inject symbols.

Parameters
symbolsarray of symbols
symbols_sizesize of the symbol array
datauser data of the callback
Returns
whether the call was successful; might set one of the following error codes:
See also
clingo_ground_callback_t

Enumeration Type Documentation

Enumeration of bit masks for solve call results.

Note
Neither clingo_solve_result_satisfiable nor clingo_solve_result_exhausted is set if the search is interrupted and no model was found.
Enumerator
clingo_solve_result_satisfiable 

The last solve call found a solution.

clingo_solve_result_unsatisfiable 

The last solve call did not find a solution.

clingo_solve_result_exhausted 

The last solve call completely exhausted the search space.

clingo_solve_result_interrupted 

The last solve call was interrupted.

See also
clingo_control_interrupt()

Function Documentation

bool clingo_control_add ( clingo_control_t control,
char const *  name,
char const *const *  parameters,
size_t  parameters_size,
char const *  program 
)

Extend the logic program with the given non-ground logic program in string form.

This function puts the given program into a block of form: #program name(parameters).

After extending the logic program, the corresponding program parts are typically grounded with clingo_control_ground.

Parameters
[in]controlthe target
[in]namename of the program block
[in]parametersstring array of parameters of the program block
[in]parameters_sizenumber of parameters
[in]programstring representation of the program
Returns
whether the call was successful; might set one of the following error codes:
Examples:
backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, solve-iteratively.c, statistics.c, symbolic-atoms.c, and theory-atoms.c.
bool clingo_control_assign_external ( clingo_control_t control,
clingo_symbol_t  atom,
clingo_truth_value_t  value 
)

Assign a truth value to an external atom.

If the atom does not exist or is not external, this is a noop.

Parameters
[in]controlthe target
[in]atomatom to assign
[in]valuethe truth value
Returns
whether the call was successful; might set one of the following error codes:
Examples:
ast.c.
bool clingo_control_backend ( clingo_control_t control,
clingo_backend_t **  backend 
)

Get an object to add ground directives to the program.

See the Program Building module for more information.

Parameters
[in]controlthe target
[out]backendthe backend object
Returns
whether the call was successful; might set one of the following error codes:
Examples:
backend.c, and theory-atoms.c.
bool clingo_control_cleanup ( clingo_control_t control)

Clean up the domains of clingo's grounding component using the solving component's top level assignment.

This function removes atoms from domains that are false and marks atoms as facts that are true. With multi-shot solving, this can result in smaller groundings because less rules have to be instantiated and more simplifications can be applied.

Parameters
[in]controlthe target
Returns
whether the call was successful; might set one of the following error codes:
bool clingo_control_configuration ( clingo_control_t control,
clingo_configuration_t **  configuration 
)

Get a configuration object to change the solver configuration.

See the Solver Configuration module for more information.

Parameters
[in]controlthe target
[out]configurationthe configuration object
Returns
whether the call was successful
Examples:
configuration.c, and statistics.c.
void clingo_control_free ( clingo_control_t control)

Free a control object created with clingo_control_new().

Parameters
[in]controlthe target
Examples:
ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, solve-iteratively.c, statistics.c, symbolic-atoms.c, and theory-atoms.c.
bool clingo_control_get_const ( clingo_control_t control,
char const *  name,
clingo_symbol_t symbol 
)

Return the symbol for a constant definition of form: #const name = symbol.

Parameters
[in]controlthe target
[in]namethe name of the constant
[out]symbolthe resulting symbol
Returns
whether the call was successful
bool clingo_control_ground ( clingo_control_t control,
clingo_part_t const *  parts,
size_t  parts_size,
clingo_ground_callback_t ground_callback,
void *  ground_callback_data 
)

Ground the selected parts of the current (non-ground) logic program.

After grounding, logic programs can be solved with clingo_control_solve.

Note
Parts of a logic program without an explicit #program specification are by default put into a program called base without arguments.
Parameters
[in]controlthe target
[in]partsarray of parts to ground
[in]parts_sizesize of the parts array
[in]ground_callbackcallback to implement external functions
[in]ground_callback_datauser data for ground_callback
Returns
whether the call was successful; might set one of the following error codes:
See also
clingo_part
Examples:
ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, solve-iteratively.c, statistics.c, symbolic-atoms.c, and theory-atoms.c.
bool clingo_control_has_const ( clingo_control_t control,
char const *  name,
bool *  exists 
)

Check if there is a constant definition for the given constant.

Parameters
[in]controlthe target
[in]namethe name of the constant
[out]existswhether a matching constant definition exists
Returns
whether the call was successful; might set one of the following error codes:
See also
clingo_control_get_const()
void clingo_control_interrupt ( clingo_control_t control)

Interrupt the active solve call (or the following solve call right at the beginning).

Parameters
[in]controlthe target
bool clingo_control_load ( clingo_control_t control,
char const *  file 
)

Extend the logic program with a program in a file.

Parameters
[in]controlthe target
[in]filepath to the file
Returns
whether the call was successful; might set one of the following error codes:
bool clingo_control_new ( char const *const *  arguments,
size_t  arguments_size,
clingo_logger_t logger,
void *  logger_data,
unsigned  message_limit,
clingo_control_t **  control 
)

Create a new control object.

A control object has to be freed using clingo_control_free().

Note
Only gringo options (without --text) and clasp's search options are supported as arguments. Furthermore, a control object is blocked while a search call is active; you must not call any member function during search.

If the logger is NULL, messages are printed to stderr.

Parameters
[in]argumentsC string array of command line arguments
[in]arguments_sizesize of the arguments array
[in]loggercallback functions for warnings and info messages
[in]logger_datauser data for the logger callback
[in]message_limitmaximum number of times the logger callback is called
[out]controlresulting control object
Returns
whether the call was successful; might set one of the following error codes:
Examples:
ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, solve-iteratively.c, statistics.c, symbolic-atoms.c, and theory-atoms.c.
bool clingo_control_program_builder ( clingo_control_t control,
clingo_program_builder_t **  builder 
)

Get an object to add non-ground directives to the program.

See the Program Building module for more information.

Parameters
[in]controlthe target
[out]builderthe program builder object
Returns
whether the call was successful
Examples:
ast.c.
bool clingo_control_register_propagator ( clingo_control_t control,
clingo_propagator_t  propagator,
void *  data,
bool  sequential 
)

Register a custom propagator with the control object.

If the sequential flag is set to true, the propagator is called sequentially when solving with multiple threads.

See the Theory Propagation module for more information.

Parameters
[in]controlthe target
[in]propagatorthe propagator
[in]datauser data passed to the propagator functions
[in]sequentialwhether the propagator should be called sequentially
Returns
whether the call was successful; might set one of the following error codes:
Examples:
propagator.c.
bool clingo_control_release_external ( clingo_control_t control,
clingo_symbol_t  atom 
)

Release an external atom.

After this call, an external atom is no longer external and subject to program simplifications. If the atom does not exist or is not external, this is a noop.

Parameters
[in]controlthe target
[in]atomatom to release
Returns
whether the call was successful; might set one of the following error codes:
bool clingo_control_solve ( clingo_control_t control,
clingo_model_callback_t model_callback,
void *  model_callback_data,
clingo_symbolic_literal_t const *  assumptions,
size_t  assumptions_size,
clingo_solve_result_bitset_t result 
)

Solve the currently grounded logic program.

Parameters
[in]controlthe target
[in]model_callbackoptional callback to intercept models
[in]model_callback_datauser data for model callback
[in]assumptionsarray of assumptions to solve under
[in]assumptions_sizenumber of assumptions
[out]resultthe result of the search
Returns
whether the call was successful; might set one of the following error codes:
Examples:
ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, statistics.c, and theory-atoms.c.
bool clingo_control_solve_async ( clingo_control_t control,
clingo_model_callback_t model_callback,
void *  model_callback_data,
clingo_finish_callback_t finish_callback,
void *  finish_callback_data,
clingo_symbolic_literal_t const *  assumptions,
size_t  assumptions_size,
clingo_solve_async_t **  handle 
)

Solve the currently grounded logic program asynchronously in the background.

See the Asynchronous Solving module for more information.

Parameters
[in]controlthe target
[in]model_callbackoptional callback to intercept models
[in]model_callback_datauser data for model callback
[in]finish_callbackoptional callback called just before the end of the search
[in]finish_callback_datauser data for finish callback
[in]assumptionsarray of assumptions to solve under
[in]assumptions_sizenumber of assumptions
[out]handlehandle to the current search
Returns
whether the call was successful; might set one of the following error codes:
Examples:
solve-async.c.
bool clingo_control_solve_iteratively ( clingo_control_t control,
clingo_symbolic_literal_t const *  assumptions,
size_t  assumptions_size,
clingo_solve_iteratively_t **  handle 
)

Solve the currently grounded logic program enumerating models iteratively.

See the Iterative Solving module for more information.

Parameters
[in]controlthe target
[in]assumptionsarray of assumptions to solve under
[in]assumptions_sizenumber of assumptions
[out]handlehandle to the current search to enumerate models
Returns
whether the call was successful; might set one of the following error codes:
Examples:
solve-iteratively.c.
bool clingo_control_statistics ( clingo_control_t control,
clingo_statistics_t **  statistics 
)

Get a statistics object to inspect solver statistics.

Statistics are updated after a solve call.

See the Statistics module for more information.

Attention
The level of detail of the statistics depends on the stats option (which can be set using Solver Configuration module or passed as an option when creating the control object). The default level zero only provides basic statistics, level one provides extended and accumulated statistics, and level two provides per-thread statistics.
Parameters
[in]controlthe target
[out]statisticsthe statistics object
Returns
whether the call was successful; might set one of the following error codes:
Examples:
statistics.c.
bool clingo_control_symbolic_atoms ( clingo_control_t control,
clingo_symbolic_atoms_t **  atoms 
)

Get an object to inspect symbolic atoms (the relevant Herbrand base) used for grounding.

See the Symbolic Atom Inspection module for more information.

Parameters
[in]controlthe target
[out]atomsthe symbolic atoms object
Returns
whether the call was successful
Examples:
backend.c, and symbolic-atoms.c.
bool clingo_control_theory_atoms ( clingo_control_t control,
clingo_theory_atoms_t **  atoms 
)

Get an object to inspect theory atoms that occur in the grounding.

See the Theory Atom Inspection module for more information.

Parameters
[in]controlthe target
[out]atomsthe theory atoms object
Returns
whether the call was successful
Examples:
theory-atoms.c.
bool clingo_control_use_enumeration_assumption ( clingo_control_t control,
bool  enable 
)

Configure how learnt constraints are handled during enumeration.

If the enumeration assumption is enabled, then all information learnt from the solver's various enumeration modes is removed after a solve call. This includes enumeration of cautious or brave consequences, enumeration of answer sets with or without projection, or finding optimal models, as well as clauses added with clingo_solve_control_add_clause().

Attention
For practical purposes, this option is only interesting for single-shot solving or before the last solve call to squeeze out a tiny bit of performance. Initially, the enumeration assumption is enabled.
Parameters
[in]controlthe target
[in]enablewhether to enable the assumption
Returns
whether the call was successful