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]	result	result of the solve call
[in]	data	user 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]	location	location from which the external function was called
[in]	name	name of the called external function
[in]	arguments	arguments of the called external function
[in]	arguments_size	number of arguments
[in]	data	user data of the callback
[in]	symbol_callback	function to inject symbols
[in]	symbol_callback_data	user 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) {
    clingo_symbol_t sym;
    clingo_symbol_create_number(42, &sym);
    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]	model	the current model
[in]	data	user data of the callback
[out]	goon	whether 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()

clingo_solve_result_bitset_t

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

symbols	array of symbols
symbols_size	size of the symbol array
data	user data of the callback

Returns

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

clingo_error_bad_alloc

See also: clingo_ground_callback_t

Enumeration Type Documentation

enum clingo_solve_result

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]	control	the target
[in]	name	name of the program block
[in]	parameters	string array of parameters of the program block
[in]	parameters_size	number of parameters
[in]	program	string representation of the program

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if parsing fails

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]	control	the target
[in]	atom	atom to assign
[in]	value	the truth value

Returns

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

clingo_error_bad_alloc

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]	control	the target
[out]	backend	the backend object

Returns

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

clingo_error_bad_alloc

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] control the target

Returns

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

clingo_error_bad_alloc

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]	control	the target
[out]	configuration	the 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] control the 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]	control	the target
[in]	name	the name of the constant
[out]	symbol	the 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]	control	the target
[in]	parts	array of parts to ground
[in]	parts_size	size of the parts array
[in]	ground_callback	callback to implement external functions
[in]	ground_callback_data	user data for ground_callback

Returns

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

clingo_error_bad_alloc
error code of ground callback

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]	control	the target
[in]	name	the name of the constant
[out]	exists	whether a matching constant definition exists

Returns

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

clingo_error_runtime if constant definition does not exist

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] control the target

bool clingo_control_load	(	clingo_control_t *	control,
		char const *	file
	)

Extend the logic program with a program in a file.

Parameters

[in]	control	the target
[in]	file	path to the file

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if parsing or checking fails

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]	arguments	C string array of command line arguments
[in]	arguments_size	size of the arguments array
[in]	logger	callback functions for warnings and info messages
[in]	logger_data	user data for the logger callback
[in]	message_limit	maximum number of times the logger callback is called
[out]	control	resulting control object

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if argument parsing fails

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]	control	the target
[out]	builder	the 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]	control	the target
[in]	propagator	the propagator
[in]	data	user data passed to the propagator functions
[in]	sequential	whether the propagator should be called sequentially

Returns

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

clingo_error_bad_alloc

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]	control	the target
[in]	atom	atom to release

Returns

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

clingo_error_bad_alloc

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]	control	the target
[in]	model_callback	optional callback to intercept models
[in]	model_callback_data	user data for model callback
[in]	assumptions	array of assumptions to solve under
[in]	assumptions_size	number of assumptions
[out]	result	the result of the search

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if solving fails
error code of model callback

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]	control	the target
[in]	model_callback	optional callback to intercept models
[in]	model_callback_data	user data for model callback
[in]	finish_callback	optional callback called just before the end of the search
[in]	finish_callback_data	user data for finish callback
[in]	assumptions	array of assumptions to solve under
[in]	assumptions_size	number of assumptions
[out]	handle	handle to the current search

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if solving could not be started

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]	control	the target
[in]	assumptions	array of assumptions to solve under
[in]	assumptions_size	number of assumptions
[out]	handle	handle to the current search to enumerate models

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if solving could not be started

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]	control	the target
[out]	statistics	the statistics object

Returns

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

clingo_error_bad_alloc

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]	control	the target
[out]	atoms	the 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]	control	the target
[out]	atoms	the 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]	control	the target
[in]	enable	whether to enable the assumption

Returns: whether the call was successful

Detailed Description

Modules

Classes

Typedefs

Enumerations

Functions

Grounding Functions

Solving Functions

Configuration Functions

Program Inspection Functions

Program Modification Functions

Typedef Documentation

Enumeration Type Documentation

Function Documentation