Detailed Description

Inspection of models and a high-level interface to add constraints during solving.

For an example, see model.c.

Typedefs
typedef struct clingo_solve_control	clingo_solve_control_t
	Object to add clauses during search.

typedef struct clingo_model	clingo_model_t
	Object representing a model.

typedef int	clingo_model_type_t
	Corresponding type to clingo_model_type_e.

typedef unsigned	clingo_show_type_bitset_t
	Corresponding type to clingo_show_type_e.

Enumerations
enum	clingo_model_type_e { clingo_model_type_stable_model = 0, clingo_model_type_brave_consequences = 1, clingo_model_type_cautious_consequences = 2 }
	Enumeration for the different model types. More...

enum	clingo_show_type_e { clingo_show_type_csp = 1, clingo_show_type_shown = 2, clingo_show_type_atoms = 4, clingo_show_type_terms = 8, clingo_show_type_theory = 16, clingo_show_type_all = 31, clingo_show_type_complement = 32 }
	Enumeration of bit flags to select symbols in models. More...

Functions for Inspecting Models
CLINGO_VISIBILITY_DEFAULT bool	clingo_model_type (clingo_model_t const model, clingo_model_type_t type)
	Get the type of the model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_number (clingo_model_t const model, uint64_t number)
	Get the running number of the model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_symbols_size (clingo_model_t const model, clingo_show_type_bitset_t show, size_t size)
	Get the number of symbols of the selected types in the model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_symbols (clingo_model_t const model, clingo_show_type_bitset_t show, clingo_symbol_t symbols, size_t size)
	Get the symbols of the selected types in the model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_contains (clingo_model_t const model, clingo_symbol_t atom, bool contained)
	Constant time lookup to test whether an atom is in a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_is_true (clingo_model_t const model, clingo_literal_t literal, bool result)
	Check if a program literal is true in a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_cost_size (clingo_model_t const model, size_t size)
	Get the number of cost values of a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_cost (clingo_model_t const model, int64_t costs, size_t size)
	Get the cost vector of a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_optimality_proven (clingo_model_t const model, bool proven)
	Whether the optimality of a model has been proven. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_thread_id (clingo_model_t const model, clingo_id_t id)
	Get the id of the solver thread that found the model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_extend (clingo_model_t model, clingo_symbol_t const symbols, size_t size)
	Add symbols to the model. More...

Functions for Adding Clauses
CLINGO_VISIBILITY_DEFAULT bool	clingo_model_context (clingo_model_t const model, clingo_solve_control_t *control)
	Get the associated solve control object of a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_control_symbolic_atoms (clingo_solve_control_t const control, clingo_symbolic_atoms_t const *atoms)
	Get an object to inspect the symbolic atoms. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_control_add_clause (clingo_solve_control_t control, clingo_literal_t const clause, size_t size)
	Add a clause that applies to the current solving step during model enumeration. More...

Enumeration Type Documentation

◆ clingo_model_type_e

enum clingo_model_type_e

Enumeration for the different model types.

Enumerator
clingo_model_type_stable_model	The model represents a stable model.
clingo_model_type_brave_consequences	The model represents a set of brave consequences.
clingo_model_type_cautious_consequences	The model represents a set of cautious consequences.

◆ clingo_show_type_e

enum clingo_show_type_e

Enumeration of bit flags to select symbols in models.

Enumerator
clingo_show_type_csp	Select CSP assignments.
clingo_show_type_shown	Select shown atoms and terms.
clingo_show_type_atoms	Select all atoms.
clingo_show_type_terms	Select all terms.
clingo_show_type_theory	Select symbols added by theory.
clingo_show_type_all	Select everything.
clingo_show_type_complement	Select false instead of true atoms (clingo_show_type_atoms) or terms (clingo_show_type_terms).

Function Documentation

◆ clingo_model_contains()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_contains	(	clingo_model_t const *	model,
		clingo_symbol_t	atom,
		bool *	contained
	)

Constant time lookup to test whether an atom is in a model.

Parameters

[in]	model	the target
[in]	atom	the atom to lookup
[out]	contained	whether the atom is contained

Returns: whether the call was successful

◆ clingo_model_context()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_context	(	clingo_model_t const *	model,
		clingo_solve_control_t **	control
	)

Get the associated solve control object of a model.

This object allows for adding clauses during model enumeration.

Parameters

[in]	model	the target
[out]	control	the resulting solve control object

Returns: whether the call was successful

◆ clingo_model_cost()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_cost	(	clingo_model_t const *	model,
		int64_t *	costs,
		size_t	size
	)

Get the cost vector of a model.

Parameters

[in]	model	the target
[out]	costs	the resulting costs
[in]	size	the number of costs

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if the size is too small

See also: clingo_model_cost_size(); clingo_model_optimality_proven()

◆ clingo_model_cost_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_cost_size	(	clingo_model_t const *	model,
		size_t *	size
	)

Get the number of cost values of a model.

Parameters

[in]	model	the target
[out]	size	the number of costs

Returns: whether the call was successful

◆ clingo_model_extend()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_extend	(	clingo_model_t *	model,
		clingo_symbol_t const *	symbols,
		size_t	size
	)

Add symbols to the model.

These symbols will appear in clingo's output, which means that this function is only meaningful if there is an underlying clingo application. Only models passed to the clingo_solve_event_callback_t are extendable.

Parameters

[in]	model	the target
[in]	symbols	the symbols to add
[in]	size	the number of symbols to add

Returns: whether the call was successful

◆ clingo_model_is_true()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_is_true	(	clingo_model_t const *	model,
		clingo_literal_t	literal,
		bool *	result
	)

Check if a program literal is true in a model.

Parameters

[in]	model	the target
[in]	literal	the literal to lookup
[out]	result	whether the literal is true

Returns: whether the call was successful

◆ clingo_model_number()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_number	(	clingo_model_t const *	model,
		uint64_t *	number
	)

Get the running number of the model.

Parameters

[in]	model	the target
[out]	number	the number of the model

Returns: whether the call was successful

Examples:: model.c.

◆ clingo_model_optimality_proven()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_optimality_proven	(	clingo_model_t const *	model,
		bool *	proven
	)

Whether the optimality of a model has been proven.

Parameters

[in]	model	the target
[out]	proven	whether the optimality has been proven

Returns: whether the call was successful

See also: clingo_model_cost()

◆ clingo_model_symbols()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_symbols	(	clingo_model_t const *	model,
		clingo_show_type_bitset_t	show,
		clingo_symbol_t *	symbols,
		size_t	size
	)

Get the symbols of the selected types in the model.

Note: CSP assignments are represented using functions with name "$" where the first argument is the name of the CSP variable and the second one its value.

Parameters

[in]	model	the target
[in]	show	which symbols to select
[out]	symbols	the resulting symbols
[in]	size	the number of selected symbols

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if the size is too small

See also: clingo_model_symbols_size()

Examples:: ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, statistics.c, and theory-atoms.c.

◆ clingo_model_symbols_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_symbols_size	(	clingo_model_t const *	model,
		clingo_show_type_bitset_t	show,
		size_t *	size
	)

Get the number of symbols of the selected types in the model.

Parameters

[in]	model	the target
[in]	show	which symbols to select
[out]	size	the number symbols

Returns

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

clingo_error_bad_alloc

Examples:: ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, statistics.c, and theory-atoms.c.

◆ clingo_model_thread_id()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_thread_id	(	clingo_model_t const *	model,
		clingo_id_t *	id
	)

Get the id of the solver thread that found the model.

Parameters

[in]	model	the target
[out]	id	the resulting thread id

Returns: whether the call was successful

◆ clingo_model_type()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_type	(	clingo_model_t const *	model,
		clingo_model_type_t *	type
	)

Get the type of the model.

Parameters

[in]	model	the target
[out]	type	the type of the model

Returns: whether the call was successful

Examples:: model.c.

◆ clingo_solve_control_add_clause()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_control_add_clause	(	clingo_solve_control_t *	control,
		clingo_literal_t const *	clause,
		size_t	size
	)

Add a clause that applies to the current solving step during model enumeration.

Note: The Theory Propagation module provides a more sophisticated interface to add clauses - even on partial assignments.

Parameters

[in]	control	the target
[in]	clause	array of literals representing the clause
[in]	size	the size of the literal array

Returns

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

clingo_error_bad_alloc
clingo_error_runtime if adding the clause fails

◆ clingo_solve_control_symbolic_atoms()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_control_symbolic_atoms	(	clingo_solve_control_t const *	control,
		clingo_symbolic_atoms_t const **	atoms
	)

Get an object to inspect the symbolic atoms.

Parameters

[in]	control	the target
[out]	atoms	the resulting object

Returns: whether the call was successful

Detailed Description

Typedefs

Enumerations

Functions for Inspecting Models

Functions for Adding Clauses

Enumeration Type Documentation

◆ clingo_model_type_e

◆ clingo_show_type_e

Function Documentation

◆ clingo_model_contains()

◆ clingo_model_context()

◆ clingo_model_cost()

◆ clingo_model_cost_size()

◆ clingo_model_extend()

◆ clingo_model_is_true()

◆ clingo_model_number()

◆ clingo_model_optimality_proven()

◆ clingo_model_symbols()

◆ clingo_model_symbols_size()

◆ clingo_model_thread_id()

◆ clingo_model_type()

◆ clingo_solve_control_add_clause()

◆ clingo_solve_control_symbolic_atoms()