Model Inspection

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
bool	clingo_model_type (clingo_model_t *model, clingo_model_type_t *type)
	Get the type of the model. More...
bool	clingo_model_number (clingo_model_t *model, uint64_t *number)
	Get the running number of the model. More...
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...
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...
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...
bool	clingo_model_cost_size (clingo_model_t *model, size_t *size)
	Get the number of cost values of a model. More...
bool	clingo_model_cost (clingo_model_t *model, int64_t *costs, size_t size)
	Get the cost vector of a model. More...
bool	clingo_model_optimality_proven (clingo_model_t *model, bool *proven)
	Whether the optimality of a model has been proven. More...

Functions for Adding Clauses
bool	clingo_model_context (clingo_model_t *model, clingo_solve_control_t **control)
	Get the associated solve control object of a model. More...
bool	clingo_solve_control_thread_id (clingo_solve_control_t *control, clingo_id_t *id)
	Get the id of the solver thread that found the model. More...
bool	clingo_solve_control_add_clause (clingo_solve_control_t *control, clingo_symbolic_literal_t const *clause, size_t size)
	Add a clause that applies to the current solving step during model enumeration. More...

Enumeration Type Documentation

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.

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

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

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

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

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

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.

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

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, solve-iteratively.c, statistics.c, and theory-atoms.c.

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, solve-iteratively.c, statistics.c, and theory-atoms.c.

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

bool clingo_solve_control_add_clause	(	clingo_solve_control_t *	control,
		clingo_symbolic_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

bool clingo_solve_control_thread_id	(	clingo_solve_control_t *	control,
		clingo_id_t *	id
	)

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

Parameters

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

Returns

whether the call was successful