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.

typedef unsigned	clingo_show_type_bitset_t
	Corresponding type to clingo_show_type.

Enumerations
enum	clingo_model_type { 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 { clingo_show_type_csp = 1, clingo_show_type_shown = 2, clingo_show_type_atoms = 4, clingo_show_type_terms = 8, clingo_show_type_extra = 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 model, clingo_model_type_t type)
	Get the type of the model. More...

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

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_symbols_size (clingo_model_t 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 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 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 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 model, size_t size)
	Get the number of cost values of a model. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_cost (clingo_model_t 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 model, bool proven)
	Whether the optimality of a model has been proven. More...

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

Functions for Adding Clauses
CLINGO_VISIBILITY_DEFAULT bool	clingo_model_context (clingo_model_t 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 control, clingo_symbolic_atoms_t *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

enum clingo_model_type

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.

Examples:: model.c.

◆ clingo_show_type

enum clingo_show_type

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_extra	Select symbols added by extensions.
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 *	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 *	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 *	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 *	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_is_true()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_is_true	(	clingo_model_t *	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 *	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 *	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 *	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 *	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 *	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 *	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

◆ 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 *	control,
		clingo_symbolic_atoms_t **	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

◆ clingo_show_type

Function Documentation

◆ clingo_model_contains()

◆ clingo_model_context()

◆ clingo_model_cost()

◆ clingo_model_cost_size()

◆ 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()