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_propagate_init	clingo_propagate_init_t
	Object to initialize a used-defined propagator before each solving step. More...

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

typedef int	clingo_clause_type_t
	Corresponding type to clingo_clause_type.

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 bool(*	clingo_propagator_undo_callback_t) (clingo_propagate_control_t , 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_clause_type { 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...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Typedef Documentation

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.

typedef struct clingo_propagate_init clingo_propagate_init_t

Object to initialize a used-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.

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

enum clingo_clause_type

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

Function Documentation

bool clingo_assignment_decision	(	clingo_assignment_t *	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

uint32_t clingo_assignment_decision_level ( clingo_assignment_t * assignment )

Get the current decision level.

Parameters

[in] assignment the target assignment

Returns: the decision level

bool clingo_assignment_has_conflict ( clingo_assignment_t * assignment )

Check if the given assignment is conflicting.

Parameters

[in] assignment the target assignment

Returns: whether the assignment is conflicting

bool clingo_assignment_has_literal	(	clingo_assignment_t *	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

bool clingo_assignment_is_false	(	clingo_assignment_t *	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()

bool clingo_assignment_is_fixed	(	clingo_assignment_t *	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

bool clingo_assignment_is_true	(	clingo_assignment_t *	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()

bool clingo_assignment_level	(	clingo_assignment_t *	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

bool clingo_assignment_truth_value	(	clingo_assignment_t *	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

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_assignment_t* clingo_propagate_control_assignment ( clingo_propagate_control_t * control )

Get the assignment associated with the underlying solver.

Parameters

[in] control the target

Returns: the assignment

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_id_t clingo_propagate_control_thread_id ( clingo_propagate_control_t * 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.

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
[out]	solver_literal	the solver literal

Returns: whether the call was successful

Examples:: propagator.c.

int clingo_propagate_init_number_of_threads ( clingo_propagate_init_t * 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.

bool clingo_propagate_init_solver_literal	(	clingo_propagate_init_t *	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.

bool clingo_propagate_init_symbolic_atoms	(	clingo_propagate_init_t *	init,
		clingo_symbolic_atoms_t **	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.

bool clingo_propagate_init_theory_atoms	(	clingo_propagate_init_t *	init,
		clingo_theory_atoms_t **	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

Initialization Functions

Assignment Functions

Propagation Functions

Typedef Documentation

Enumeration Type Documentation

Function Documentation