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

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.

typedef int	clingo_consequence_t
	Corresponding type to clingo_model_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_shown = 1 , clingo_show_type_atoms = 2 , clingo_show_type_terms = 4 , clingo_show_type_theory = 8 , clingo_show_type_all = 15 }
	Enumeration of bit flags to select symbols in models. More...

enum	clingo_consequence_e { clingo_consequence_false = 0 , clingo_consequence_true = 1 , clingo_consequence_unknown = 2 }
	Enumeration for the different consequence types. 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.

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

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_symbols (clingo_model_t const model, clingo_show_type_bitset_t show, clingo_symbol_callback_t callback, void data)
	Get the symbols of the selected types in the model.

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.

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.

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_is_consequence (clingo_model_t const model, clingo_literal_t literal, clingo_consequence_t result)
	Check if the given literal is a consequence.

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

CLINGO_VISIBILITY_DEFAULT bool	clingo_model_priority (clingo_model_t const model, clingo_weight_t const priorities, size_t size)
	Get the priorities of the costs.

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

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.

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

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

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_control_base (clingo_solve_control_t const control, clingo_base_t const *base)
	Get an object to inspect the symbolic atoms.

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.

Detailed Description

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

For an example, see model.c.

Enumeration Type Documentation

◆ clingo_consequence_e

enum clingo_consequence_e

Enumeration for the different consequence types.

Enumerator
clingo_consequence_false	The literal is not a consequence.
clingo_consequence_true	The literal is a consequence.
clingo_consequence_unknown	The literal might or might not be a consequence.

◆ 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_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.

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: wether the call was successful

◆ clingo_model_control()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_control	(	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: wether the call was successful

◆ clingo_model_cost()

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

Get the costs of a model.

Attention: The lifetime of the costs array is tied to the lifetime of the object.

Parameters

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

Returns: wether the call was successful

See also: clingo_model_optimality_proven()

◆ 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_handler_t are extendable.

Parameters

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

Returns: wether the call was successful

◆ clingo_model_is_consequence()

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

Check if the given literal is a consequence.

While enumerating cautious or brave consequences, there is partial information about which literals are consequences. The current state of a literal can be requested using this function. If this function is used during normal model enumeration, the function just returns whether a literal is true of false in the current model.

Parameters

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

Returns: wether 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: wether 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: wether the call was successful

◆ 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: wether the call was successful

See also: clingo_model_cost()

◆ clingo_model_priority()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_priority	(	clingo_model_t const *	model,
		clingo_weight_t const **	priorities,
		size_t *	size
	)

Get the priorities of the costs.

Attention: The lifetime of the costs array is tied to the lifetime of the object.

Parameters

[in]	model	the target
[out]	priorities	the resulting priorities
[out]	size	the size of the priorities array

Returns: wether the call was successful

◆ clingo_model_symbols()

CLINGO_VISIBILITY_DEFAULT bool clingo_model_symbols	(	clingo_model_t const *	model,
		clingo_show_type_bitset_t	show,
		clingo_symbol_callback_t	callback,
		void *	data
	)

Get the symbols of the selected types in the model.

Parameters

[in]	model	the target
[in]	show	which symbols to select
[out]	callback	callback to copy symbols
[in]	data	userdata for the callback

Returns: wether the call was successful

Examples: control.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: wether 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: wether 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: wether the call was successful

◆ clingo_solve_control_base()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_control_base	(	clingo_solve_control_t const *	control,
		clingo_base_t const **	base
	)

Get an object to inspect the symbolic atoms.

Parameters

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

Returns: wether the call was successful

Typedefs

Enumerations

Functions for Inspecting Models

Functions for Adding Clauses

Detailed Description

Enumeration Type Documentation

◆ clingo_consequence_e

◆ clingo_model_type_e

◆ clingo_show_type_e

Function Documentation

◆ clingo_model_contains()

◆ clingo_model_control()

◆ clingo_model_cost()

◆ clingo_model_extend()

◆ clingo_model_is_consequence()

◆ clingo_model_is_true()

◆ clingo_model_number()

◆ clingo_model_optimality_proven()

◆ clingo_model_priority()

◆ clingo_model_symbols()

◆ clingo_model_thread_id()

◆ clingo_model_type()

◆ clingo_solve_control_add_clause()

◆ clingo_solve_control_base()