Detailed Description

Extend the search with propagators for arbitrary theories.

For an example, see propagator.c.

Classes
struct	clingo_propagator
	An instance of this struct has to be registered with a solver to implement a custom propagator. More...

Typedefs
typedef struct clingo_assignment	clingo_assignment_t
	Represents a (partial) assignment of a particular solver. More...

typedef int	clingo_propagator_check_mode_t
	Corresponding type to clingo_propagator_check_mode_e.

typedef int	clingo_weight_constraint_type_t
	Corresponding type to clingo_weight_constraint_type_e.

typedef struct clingo_propagate_init	clingo_propagate_init_t
	Object to initialize a user-defined propagator before each solving step. More...

typedef int	clingo_clause_type_t
	Corresponding type to clingo_clause_type_e.

typedef struct clingo_propagate_control	clingo_propagate_control_t
	This object can be used to add clauses and propagate literals while solving.

typedef bool(*	clingo_propagator_init_callback_t) (clingo_propagate_init_t , void )
	Typedef for clingo_propagator::init().

typedef bool(*	clingo_propagator_propagate_callback_t) (clingo_propagate_control_t , clingo_literal_t const , size_t, void *)
	Typedef for clingo_propagator::propagate().

typedef void(*	clingo_propagator_undo_callback_t) (clingo_propagate_control_t const , clingo_literal_t const , size_t, void *)
	Typedef for clingo_propagator::undo().

typedef bool(*	clingo_propagator_check_callback_t) (clingo_propagate_control_t , void )
	Typedef for clingo_propagator::check().

typedef struct clingo_propagator	clingo_propagator_t
	An instance of this struct has to be registered with a solver to implement a custom propagator. More...

Enumerations
enum	clingo_propagator_check_mode_e { clingo_propagator_check_mode_none = 0, clingo_propagator_check_mode_total = 1, clingo_propagator_check_mode_fixpoint = 2, clingo_propagator_check_mode_both = 3 }
	Supported check modes for propagators. More...

enum	clingo_weight_constraint_type_e { clingo_weight_constraint_type_implication_left = -1, clingo_weight_constraint_type_implication_right = 1, clingo_weight_constraint_type_equivalence = 0 }
	Enumeration of weight_constraint_types. More...

enum	clingo_clause_type_e { clingo_clause_type_learnt = 0, clingo_clause_type_static = 1, clingo_clause_type_volatile = 2, clingo_clause_type_volatile_static = 3 }
	Enumeration of clause types determining the lifetime of a clause. More...

Assignment Functions
CLINGO_VISIBILITY_DEFAULT uint32_t	clingo_assignment_decision_level (clingo_assignment_t const *assignment)
	Get the current decision level. More...

CLINGO_VISIBILITY_DEFAULT uint32_t	clingo_assignment_root_level (clingo_assignment_t const *assignment)
	Get the current root level. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_has_conflict (clingo_assignment_t const *assignment)
	Check if the given assignment is conflicting. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_has_literal (clingo_assignment_t const *assignment, clingo_literal_t literal)
	Check if the given literal is part of a (partial) assignment. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_level (clingo_assignment_t const assignment, clingo_literal_t literal, uint32_t level)
	Determine the decision level of a given literal. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_decision (clingo_assignment_t const assignment, uint32_t level, clingo_literal_t literal)
	Determine the decision literal given a decision level. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_is_fixed (clingo_assignment_t const assignment, clingo_literal_t literal, bool is_fixed)
	Check if a literal has a fixed truth value. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_is_true (clingo_assignment_t const assignment, clingo_literal_t literal, bool is_true)
	Check if a literal is true. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_is_false (clingo_assignment_t const assignment, clingo_literal_t literal, bool is_false)
	Check if a literal has a fixed truth value. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_truth_value (clingo_assignment_t const assignment, clingo_literal_t literal, clingo_truth_value_t value)
	Determine the truth value of a given literal. More...

CLINGO_VISIBILITY_DEFAULT size_t	clingo_assignment_size (clingo_assignment_t const *assignment)
	The number of (positive) literals in the assignment. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_at (clingo_assignment_t const assignment, size_t offset, clingo_literal_t literal)
	The (positive) literal at the given offset in the assignment. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_is_total (clingo_assignment_t const *assignment)
	Check if the assignment is total, i.e. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_trail_size (clingo_assignment_t const assignment, uint32_t size)
	Returns the number of literals in the trail, i.e., the number of assigned literals. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_trail_begin (clingo_assignment_t const assignment, uint32_t level, uint32_t offset)
	Returns the offset of the decision literal with the given decision level in the trail. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_trail_end (clingo_assignment_t const assignment, uint32_t level, uint32_t offset)
	Returns the offset following the last literal with the given decision level. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_assignment_trail_at (clingo_assignment_t const assignment, uint32_t offset, clingo_literal_t literal)
	Returns the literal at the given position in the trail. More...

Initialization Functions
CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_solver_literal (clingo_propagate_init_t const init, clingo_literal_t aspif_literal, clingo_literal_t solver_literal)
	Map the given program literal or condition id to its solver literal. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_watch (clingo_propagate_init_t *init, clingo_literal_t solver_literal)
	Add a watch for the solver literal in the given phase. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_watch_to_thread (clingo_propagate_init_t *init, clingo_literal_t solver_literal, clingo_id_t thread_id)
	Add a watch for the solver literal in the given phase to the given solver thread. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_remove_watch (clingo_propagate_init_t *init, clingo_literal_t solver_literal)
	Remove the watch for the solver literal in the given phase. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_remove_watch_from_thread (clingo_propagate_init_t *init, clingo_literal_t solver_literal, uint32_t thread_id)
	Remove the watch for the solver literal in the given phase from the given solver thread. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_freeze_literal (clingo_propagate_init_t *init, clingo_literal_t solver_literal)
	Freeze the given solver literal. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_symbolic_atoms (clingo_propagate_init_t const init, clingo_symbolic_atoms_t const *atoms)
	Get an object to inspect the symbolic atoms. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_theory_atoms (clingo_propagate_init_t const init, clingo_theory_atoms_t const *atoms)
	Get an object to inspect the theory atoms. More...

CLINGO_VISIBILITY_DEFAULT int	clingo_propagate_init_number_of_threads (clingo_propagate_init_t const *init)
	Get the number of threads used in subsequent solving. More...

CLINGO_VISIBILITY_DEFAULT void	clingo_propagate_init_set_check_mode (clingo_propagate_init_t *init, clingo_propagator_check_mode_t mode)
	Configure when to call the check method of the propagator. More...

CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t	clingo_propagate_init_get_check_mode (clingo_propagate_init_t const *init)
	Get the current check mode of the propagator. More...

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *	clingo_propagate_init_assignment (clingo_propagate_init_t const *init)
	Get the top level assignment solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_literal (clingo_propagate_init_t init, bool freeze, clingo_literal_t result)
	Add a literal to the solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_clause (clingo_propagate_init_t init, clingo_literal_t const clause, size_t size, bool *result)
	Add the given clause to the solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_weight_constraint (clingo_propagate_init_t init, clingo_literal_t literal, clingo_weighted_literal_t const literals, size_t size, clingo_weight_t bound, clingo_weight_constraint_type_t type, bool compare_equal, bool *result)
	Add the given weight constraint to the solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_add_minimize (clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weight_t weight, clingo_weight_t priority)
	Add the given literal to minimize to the solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_init_propagate (clingo_propagate_init_t init, bool result)
	Propagates consequences of the underlying problem excluding registered propagators. More...

Propagation Functions
CLINGO_VISIBILITY_DEFAULT clingo_id_t	clingo_propagate_control_thread_id (clingo_propagate_control_t const *control)
	Get the id of the underlying solver thread. More...

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *	clingo_propagate_control_assignment (clingo_propagate_control_t const *control)
	Get the assignment associated with the underlying solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_control_add_literal (clingo_propagate_control_t control, clingo_literal_t result)
	Adds a new volatile literal to the underlying solver thread. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_control_add_watch (clingo_propagate_control_t *control, clingo_literal_t literal)
	Add a watch for the solver literal in the given phase. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_control_has_watch (clingo_propagate_control_t const *control, clingo_literal_t literal)
	Check whether a literal is watched in the current solver thread. More...

CLINGO_VISIBILITY_DEFAULT void	clingo_propagate_control_remove_watch (clingo_propagate_control_t *control, clingo_literal_t literal)
	Removes the watch (if any) for the given solver literal. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_control_add_clause (clingo_propagate_control_t control, clingo_literal_t const clause, size_t size, clingo_clause_type_t type, bool *result)
	Add the given clause to the solver. More...

CLINGO_VISIBILITY_DEFAULT bool	clingo_propagate_control_propagate (clingo_propagate_control_t control, bool result)
	Propagate implied literals (resulting from added clauses). More...

Typedef Documentation

◆ clingo_assignment_t

typedef struct clingo_assignment clingo_assignment_t

Represents a (partial) assignment of a particular solver.

An assignment assigns truth values to a set of literals. A literal is assigned to either true or false, or is unassigned. Furthermore, each assigned literal is associated with a decision level. There is exactly one decision literal for each decision level greater than zero. Assignments to all other literals on the same level are consequences implied by the current and possibly previous decisions. Assignments on level zero are immediate consequences of the current program. Decision levels are consecutive numbers starting with zero up to and including the current decision level.

◆ clingo_propagate_init_t

typedef struct clingo_propagate_init clingo_propagate_init_t

Object to initialize a user-defined propagator before each solving step.

Each symbolic or theory atom is uniquely associated with an aspif atom in form of a positive integer (clingo_literal_t). Aspif literals additionally are signed to represent default negation. Furthermore, there are non-zero integer solver literals (also represented using clingo_literal_t). There is a surjective mapping from program atoms to solver literals.

All methods called during propagation use solver literals whereas clingo_symbolic_atoms_literal() and clingo_theory_atoms_atom_literal() return program literals. The function clingo_propagate_init_solver_literal() can be used to map program literals or condition ids to solver literals.

◆ clingo_propagator_t

typedef struct clingo_propagator clingo_propagator_t

An instance of this struct has to be registered with a solver to implement a custom propagator.

Not all callbacks have to be implemented and can be set to NULL if not needed.

See also: Theory Propagation

Enumeration Type Documentation

◆ clingo_clause_type_e

enum clingo_clause_type_e

Enumeration of clause types determining the lifetime of a clause.

Clauses in the solver are either cleaned up based on a configurable deletion policy or at the end of a solving step. The values of this enumeration determine if a clause is subject to one of the above deletion strategies.

Enumerator
clingo_clause_type_learnt	clause is subject to the solvers deletion policy
clingo_clause_type_static	clause is not subject to the solvers deletion policy
clingo_clause_type_volatile	like clingo_clause_type_learnt but the clause is deleted after a solving step
clingo_clause_type_volatile_static	like clingo_clause_type_static but the clause is deleted after a solving step

◆ clingo_propagator_check_mode_e

enum clingo_propagator_check_mode_e

Supported check modes for propagators.

Note that total checks are subject to the lock when a model is found. This means that information from previously found models can be used to discard assignments in check calls.

Enumerator
clingo_propagator_check_mode_none	do not call clingo_propagator::check() at all
clingo_propagator_check_mode_total	call clingo_propagator::check() on total assignments
clingo_propagator_check_mode_fixpoint	call clingo_propagator::check() on propagation fixpoints
clingo_propagator_check_mode_both	call clingo_propagator::check() on propagation fixpoints and total assignments

◆ clingo_weight_constraint_type_e

enum clingo_weight_constraint_type_e

Enumeration of weight_constraint_types.

Enumerator
clingo_weight_constraint_type_implication_left	the weight constraint implies the literal
clingo_weight_constraint_type_implication_right	the literal implies the weight constraint
clingo_weight_constraint_type_equivalence	the weight constraint is equivalent to the literal

Function Documentation

◆ clingo_assignment_at()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_at	(	clingo_assignment_t const *	assignment,
		size_t	offset,
		clingo_literal_t *	literal
	)

The (positive) literal at the given offset in the assignment.

Parameters

[in]	assignment	the target
[in]	offset	the offset of the literal
[out]	literal	the literal

Returns: whether the call was successful

◆ clingo_assignment_decision()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_decision	(	clingo_assignment_t const *	assignment,
		uint32_t	level,
		clingo_literal_t *	literal
	)

Determine the decision literal given a decision level.

Parameters

[in]	assignment	the target assignment
[in]	level	the level
[out]	literal	the resulting literal

Returns: whether the call was successful

◆ clingo_assignment_decision_level()

CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_decision_level ( clingo_assignment_t const * assignment )

Get the current decision level.

Parameters

[in] assignment the target assignment

Returns: the decision level

◆ clingo_assignment_has_conflict()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict ( clingo_assignment_t const * assignment )

Check if the given assignment is conflicting.

Parameters

[in] assignment the target assignment

Returns: whether the assignment is conflicting

◆ clingo_assignment_has_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_literal	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal
	)

Check if the given literal is part of a (partial) assignment.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal

Returns: whether the literal is valid

◆ clingo_assignment_is_false()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_false	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal,
		bool *	is_false
	)

Check if a literal has a fixed truth value.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal
[out]	is_false	whether the literal is false

Returns: whether the call was successful

See also: clingo_assignment_truth_value()

◆ clingo_assignment_is_fixed()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_fixed	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal,
		bool *	is_fixed
	)

Check if a literal has a fixed truth value.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal
[out]	is_fixed	whether the literal is fixed

Returns: whether the call was successful

◆ clingo_assignment_is_total()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total ( clingo_assignment_t const * assignment )

Check if the assignment is total, i.e.

there are no free literal.

Parameters

[in] assignment the target

Returns: wheather the assignment is total

◆ clingo_assignment_is_true()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_true	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal,
		bool *	is_true
	)

Check if a literal is true.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal
[out]	is_true	whether the literal is true

Returns: whether the call was successful

See also: clingo_assignment_truth_value()

◆ clingo_assignment_level()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_level	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal,
		uint32_t *	level
	)

Determine the decision level of a given literal.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal
[out]	level	the resulting level

Returns: whether the call was successful

◆ clingo_assignment_root_level()

CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_root_level ( clingo_assignment_t const * assignment )

Get the current root level.

Decisions levels smaller or equal to the root level are not backtracked during solving.

Parameters

[in] assignment the target assignment

Returns: the decision level

◆ clingo_assignment_size()

CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_size ( clingo_assignment_t const * assignment )

The number of (positive) literals in the assignment.

Parameters

[in] assignment the target

Returns: the number of literals

◆ clingo_assignment_trail_at()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_at	(	clingo_assignment_t const *	assignment,
		uint32_t	offset,
		clingo_literal_t *	literal
	)

Returns the literal at the given position in the trail.

Parameters

[in]	assignment	the target
[in]	offset	the offset of the literal
[out]	literal	the literal

Returns: whether the call was successful

◆ clingo_assignment_trail_begin()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_begin	(	clingo_assignment_t const *	assignment,
		uint32_t	level,
		uint32_t *	offset
	)

Returns the offset of the decision literal with the given decision level in the trail.

Note: Literals in the trail are ordered by decision levels, where the first literal with a larger level than the previous literals is a decision; the following literals with same level are implied by this decision literal. Each decision level up to and including the current decision level has a valid offset in the trail.

Parameters

[in]	assignment	the target
[in]	level	the decision level
[out]	offset	the offset of the decision literal

Returns: whether the call was successful

◆ clingo_assignment_trail_end()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_end	(	clingo_assignment_t const *	assignment,
		uint32_t	level,
		uint32_t *	offset
	)

Returns the offset following the last literal with the given decision level.

Note: This function is the counter part to clingo_assignment_trail_begin().

Parameters

[in]	assignment	the target
[in]	level	the decision level
[out]	offset	the offset

Returns: whether the call was successful

◆ clingo_assignment_trail_size()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_size	(	clingo_assignment_t const *	assignment,
		uint32_t *	size
	)

Returns the number of literals in the trail, i.e., the number of assigned literals.

Parameters

[in]	assignment	the target
[out]	size	the number of literals in the trail

Returns: whether the call was successful

◆ clingo_assignment_truth_value()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_truth_value	(	clingo_assignment_t const *	assignment,
		clingo_literal_t	literal,
		clingo_truth_value_t *	value
	)

Determine the truth value of a given literal.

Parameters

[in]	assignment	the target assignment
[in]	literal	the literal
[out]	value	the resulting truth value

Returns: whether the call was successful

◆ clingo_propagate_control_add_clause()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_clause	(	clingo_propagate_control_t *	control,
		clingo_literal_t const *	clause,
		size_t	size,
		clingo_clause_type_t	type,
		bool *	result
	)

Add the given clause to the solver.

This method sets its result to false if the current propagation must be stopped for the solver to backtrack.

Attention: No further calls on the control object or functions on the assignment should be called when the result of this method is false.

Parameters

[in]	control	the target
[in]	clause	the clause to add
[in]	size	the size of the clause
[in]	type	the clause type determining its lifetime
[out]	result	result indicating whether propagation has to be stopped

Returns

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

clingo_error_bad_alloc

Examples:: propagator.c.

◆ clingo_propagate_control_add_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_literal	(	clingo_propagate_control_t *	control,
		clingo_literal_t *	result
	)

Adds a new volatile literal to the underlying solver thread.

Attention: The literal is only valid within the current solving step and solver thread. All volatile literals and clauses involving a volatile literal are deleted after the current search.

Parameters

[in]	control	the target
[out]	result	the (positive) solver literal

Returns

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

clingo_error_bad_alloc
clingo_error_logic if the assignment is conflicting

◆ clingo_propagate_control_add_watch()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_watch	(	clingo_propagate_control_t *	control,
		clingo_literal_t	literal
	)

Add a watch for the solver literal in the given phase.

Note: Unlike clingo_propagate_init_add_watch() this does not add a watch to all solver threads but just the current one.

Parameters

[in]	control	the target
[in]	literal	the literal to watch

Returns

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

clingo_error_bad_alloc
clingo_error_logic if the literal is invalid

See also: clingo_propagate_control_remove_watch()

◆ clingo_propagate_control_assignment()

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const* clingo_propagate_control_assignment ( clingo_propagate_control_t const * control )

Get the assignment associated with the underlying solver.

Parameters

[in] control the target

Returns: the assignment

◆ clingo_propagate_control_has_watch()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_has_watch	(	clingo_propagate_control_t const *	control,
		clingo_literal_t	literal
	)

Check whether a literal is watched in the current solver thread.

Parameters

[in]	control	the target
[in]	literal	the literal to check

Returns: whether the literal is watched

◆ clingo_propagate_control_propagate()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_propagate	(	clingo_propagate_control_t *	control,
		bool *	result
	)

Propagate implied literals (resulting from added clauses).

This method sets its result to false if the current propagation must be stopped for the solver to backtrack.

Attention: No further calls on the control object or functions on the assignment should be called when the result of this method is false.

Parameters

[in]	control	the target
[out]	result	result indicating whether propagation has to be stopped

Returns

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

clingo_error_bad_alloc

Examples:: propagator.c.

◆ clingo_propagate_control_remove_watch()

CLINGO_VISIBILITY_DEFAULT void clingo_propagate_control_remove_watch	(	clingo_propagate_control_t *	control,
		clingo_literal_t	literal
	)

Removes the watch (if any) for the given solver literal.

Note: Similar to clingo_propagate_init_add_watch() this just removes the watch in the current solver thread.

Parameters

[in]	control	the target
[in]	literal	the literal to remove

◆ clingo_propagate_control_thread_id()

CLINGO_VISIBILITY_DEFAULT clingo_id_t clingo_propagate_control_thread_id ( clingo_propagate_control_t const * control )

Get the id of the underlying solver thread.

Thread ids are consecutive numbers starting with zero.

Parameters

[in] control the target

Returns: the thread id

Examples:: propagator.c.

◆ clingo_propagate_init_add_clause()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_clause	(	clingo_propagate_init_t *	init,
		clingo_literal_t const *	clause,
		size_t	size,
		bool *	result
	)

Add the given clause to the solver.

Attention: No further calls on the init object or functions on the assignment should be called when the result of this method is false.

Parameters

[in]	init	the target
[in]	clause	the clause to add
[in]	size	the size of the clause
[out]	result	result indicating whether the problem became unsatisfiable

Returns

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

clingo_error_bad_alloc

◆ clingo_propagate_init_add_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_literal	(	clingo_propagate_init_t *	init,
		bool	freeze,
		clingo_literal_t *	result
	)

Add a literal to the solver.

To be able to use the variable in clauses during propagation or add watches to it, it has to be frozen. Otherwise, it might be removed during preprocessing.

Attention: If varibales were added, subsequent calls to functions adding constraints or clingo_propagate_init_propagate() are expensive. It is best to add varables in batches.

Parameters

[in]	init	the target
[in]	freeze	whether to freeze the literal
[out]	result	the added literal

Returns

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

clingo_error_bad_alloc

◆ clingo_propagate_init_add_minimize()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_minimize	(	clingo_propagate_init_t *	init,
		clingo_literal_t	literal,
		clingo_weight_t	weight,
		clingo_weight_t	priority
	)

Add the given literal to minimize to the solver.

This corresponds to a weak constraint of form :~ literal. [weight@priority].

Parameters

[in]	init	the target
[in]	literal	the literal to minimize
[in]	weight	the weight of the literal
[in]	priority	the priority of the literal

Returns

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

clingo_error_bad_alloc

◆ clingo_propagate_init_add_watch()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_watch	(	clingo_propagate_init_t *	init,
		clingo_literal_t	solver_literal
	)

Add a watch for the solver literal in the given phase.

Parameters

[in]	init	the target
[in]	solver_literal	the solver literal

Returns: whether the call was successful

Examples:: propagator.c.

◆ clingo_propagate_init_add_watch_to_thread()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_watch_to_thread	(	clingo_propagate_init_t *	init,
		clingo_literal_t	solver_literal,
		clingo_id_t	thread_id
	)

Add a watch for the solver literal in the given phase to the given solver thread.

Parameters

[in]	init	the target
[in]	solver_literal	the solver literal
[in]	thread_id	the id of the solver thread

Returns: whether the call was successful

◆ clingo_propagate_init_add_weight_constraint()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_weight_constraint	(	clingo_propagate_init_t *	init,
		clingo_literal_t	literal,
		clingo_weighted_literal_t const *	literals,
		size_t	size,
		clingo_weight_t	bound,
		clingo_weight_constraint_type_t	type,
		bool	compare_equal,
		bool *	result
	)

Add the given weight constraint to the solver.

This function adds a constraint of form literal <=> { lit=weight | (lit, weight) in literals } >= bound to the solver. Depending on the type the <=> connective can be either a left implication, right implication, or equivalence.

Attention: No further calls on the init object or functions on the assignment should be called when the result of this method is false.

Parameters

[in]	init	the target
[in]	literal	the literal of the constraint
[in]	literals	the weighted literals
[in]	size	the number of weighted literals
[in]	bound	the bound of the constraint
[in]	type	the type of the weight constraint
[in]	compare_equal	if true compare equal instead of less than equal
[out]	result	result indicating whether the problem became unsatisfiable

Returns

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

clingo_error_bad_alloc

◆ clingo_propagate_init_assignment()

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const* clingo_propagate_init_assignment ( clingo_propagate_init_t const * init )

Get the top level assignment solver.

Parameters

[in] init the target

Returns: the assignment

◆ clingo_propagate_init_freeze_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_freeze_literal	(	clingo_propagate_init_t *	init,
		clingo_literal_t	solver_literal
	)

Freeze the given solver literal.

Any solver literal that is not frozen is subject to simplification and might be removed in a preprocessing step after propagator initialization. A propagator should freeze all literals over which it might add clauses during propagation. Note that any watched literal is automatically frozen and that it does not matter which phase of the literal is frozen.

Parameters

[in]	init	the target
[in]	solver_literal	the solver literal

Returns: whether the call was successful

◆ clingo_propagate_init_get_check_mode()

CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_get_check_mode ( clingo_propagate_init_t const * init )

Get the current check mode of the propagator.

Parameters

[in] init the target

Returns: bitmask when to call the propagator

See also: clingo_propagate_init_set_check_mode()

◆ clingo_propagate_init_number_of_threads()

CLINGO_VISIBILITY_DEFAULT int clingo_propagate_init_number_of_threads ( clingo_propagate_init_t const * init )

Get the number of threads used in subsequent solving.

Parameters

[in] init the target

Returns: the number of threads

See also: clingo_propagate_control_thread_id()

Examples:: propagator.c.

◆ clingo_propagate_init_propagate()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_propagate	(	clingo_propagate_init_t *	init,
		bool *	result
	)

Propagates consequences of the underlying problem excluding registered propagators.

Note: The function has no effect if SAT-preprocessing is enabled.

Attention: No further calls on the init object or functions on the assignment should be called when the result of this method is false.

Parameters

[in]	init	the target
[out]	result	result indicating whether the problem became unsatisfiable

Returns

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

clingo_error_bad_alloc

◆ clingo_propagate_init_remove_watch()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_remove_watch	(	clingo_propagate_init_t *	init,
		clingo_literal_t	solver_literal
	)

Remove the watch for the solver literal in the given phase.

Parameters

[in]	init	the target
[in]	solver_literal	the solver literal

Returns: whether the call was successful

◆ clingo_propagate_init_remove_watch_from_thread()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_remove_watch_from_thread	(	clingo_propagate_init_t *	init,
		clingo_literal_t	solver_literal,
		uint32_t	thread_id
	)

Remove the watch for the solver literal in the given phase from the given solver thread.

Parameters

[in]	init	the target
[in]	solver_literal	the solver literal
[in]	thread_id	the id of the solver thread

Returns: whether the call was successful

◆ clingo_propagate_init_set_check_mode()

CLINGO_VISIBILITY_DEFAULT void clingo_propagate_init_set_check_mode	(	clingo_propagate_init_t *	init,
		clingo_propagator_check_mode_t	mode
	)

Configure when to call the check method of the propagator.

Parameters

[in]	init	the target
[in]	mode	bitmask when to call the propagator

See also: clingo_propagator::check()

◆ clingo_propagate_init_solver_literal()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_solver_literal	(	clingo_propagate_init_t const *	init,
		clingo_literal_t	aspif_literal,
		clingo_literal_t *	solver_literal
	)

Map the given program literal or condition id to its solver literal.

Parameters

[in]	init	the target
[in]	aspif_literal	the aspif literal to map
[out]	solver_literal	the resulting solver literal

Returns: whether the call was successful

Examples:: propagator.c.

◆ clingo_propagate_init_symbolic_atoms()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_symbolic_atoms	(	clingo_propagate_init_t const *	init,
		clingo_symbolic_atoms_t const **	atoms
	)

Get an object to inspect the symbolic atoms.

Parameters

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

Returns: whether the call was successful

Examples:: propagator.c.

◆ clingo_propagate_init_theory_atoms()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_theory_atoms	(	clingo_propagate_init_t const *	init,
		clingo_theory_atoms_t const **	atoms
	)

Get an object to inspect the theory atoms.

Parameters

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

Returns: whether the call was successful

Detailed Description

Classes

Typedefs

Enumerations

Assignment Functions

Initialization Functions

Propagation Functions

Typedef Documentation

◆ clingo_assignment_t

◆ clingo_propagate_init_t

◆ clingo_propagator_t

Enumeration Type Documentation

◆ clingo_clause_type_e

◆ clingo_propagator_check_mode_e

◆ clingo_weight_constraint_type_e

Function Documentation

◆ clingo_assignment_at()

◆ clingo_assignment_decision()

◆ clingo_assignment_decision_level()

◆ clingo_assignment_has_conflict()

◆ clingo_assignment_has_literal()

◆ clingo_assignment_is_false()

◆ clingo_assignment_is_fixed()

◆ clingo_assignment_is_total()

◆ clingo_assignment_is_true()

◆ clingo_assignment_level()

◆ clingo_assignment_root_level()

◆ clingo_assignment_size()

◆ clingo_assignment_trail_at()

◆ clingo_assignment_trail_begin()

◆ clingo_assignment_trail_end()

◆ clingo_assignment_trail_size()

◆ clingo_assignment_truth_value()

◆ clingo_propagate_control_add_clause()

◆ clingo_propagate_control_add_literal()

◆ clingo_propagate_control_add_watch()

◆ clingo_propagate_control_assignment()

◆ clingo_propagate_control_has_watch()

◆ clingo_propagate_control_propagate()

◆ clingo_propagate_control_remove_watch()

◆ clingo_propagate_control_thread_id()

◆ clingo_propagate_init_add_clause()

◆ clingo_propagate_init_add_literal()

◆ clingo_propagate_init_add_minimize()

◆ clingo_propagate_init_add_watch()

◆ clingo_propagate_init_add_watch_to_thread()

◆ clingo_propagate_init_add_weight_constraint()

◆ clingo_propagate_init_assignment()

◆ clingo_propagate_init_freeze_literal()

◆ clingo_propagate_init_get_check_mode()

◆ clingo_propagate_init_number_of_threads()

◆ clingo_propagate_init_propagate()

◆ clingo_propagate_init_remove_watch()

◆ clingo_propagate_init_remove_watch_from_thread()

◆ clingo_propagate_init_set_check_mode()

◆ clingo_propagate_init_solver_literal()

◆ clingo_propagate_init_symbolic_atoms()

◆ clingo_propagate_init_theory_atoms()