Clingo C API
C API for clingo providing high level functions to control grounding and solving.
Classes | Typedefs | Enumerations
Theory Propagation

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.
 
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.
 
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_propagator_check_mode { clingo_propagator_check_mode_none = 0, clingo_propagator_check_mode_total = 1, clingo_propagator_check_mode_fixpoint = 2 }
 Supported check modes for propagators. More...
 
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...
 

Assignment Functions

CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_decision_level (clingo_assignment_t *assignment)
 Get the current decision level. More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict (clingo_assignment_t *assignment)
 Check if the given assignment is conflicting. More...
 
CLINGO_VISIBILITY_DEFAULT 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...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_level (clingo_assignment_t *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 *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 *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 *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 *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 *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 *assignment)
 The number of assigned literals in the assignment. More...
 
CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_max_size (clingo_assignment_t *assignment)
 The maximum size of the assignment (if all literals are assigned). More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total (clingo_assignment_t *assignment)
 Check if the assignmen is total, i.e. More...
 

Initialization Functions

CLINGO_VISIBILITY_DEFAULT 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...
 
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, uint32_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_symbolic_atoms (clingo_propagate_init_t *init, clingo_symbolic_atoms_t **atoms)
 Get an object to inspect the symbolic atoms. More...
 
CLINGO_VISIBILITY_DEFAULT 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...
 
CLINGO_VISIBILITY_DEFAULT int clingo_propagate_init_number_of_threads (clingo_propagate_init_t *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 *init)
 Get the current check mode of the propagator. More...
 
CLINGO_VISIBILITY_DEFAULT clingo_assignment_tclingo_propagate_init_assignment (clingo_propagate_init_t *init)
 Get the top level assignment solver. More...
 

Propagation Functions

CLINGO_VISIBILITY_DEFAULT clingo_id_t clingo_propagate_control_thread_id (clingo_propagate_control_t *control)
 Get the id of the underlying solver thread. More...
 
CLINGO_VISIBILITY_DEFAULT clingo_assignment_tclingo_propagate_control_assignment (clingo_propagate_control_t *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 *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

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

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

Supported check modes for propagators.

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 assignment

clingo_propagator_check_mode_fixpoint 

call clingo_propagator::check() on propagation fixpoints

Function Documentation

◆ clingo_assignment_decision()

CLINGO_VISIBILITY_DEFAULT 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]assignmentthe target assignment
[in]levelthe level
[out]literalthe resulting literal
Returns
whether the call was successful

◆ clingo_assignment_decision_level()

CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_decision_level ( clingo_assignment_t assignment)

Get the current decision level.

Parameters
[in]assignmentthe target assignment
Returns
the decision level

◆ clingo_assignment_has_conflict()

CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict ( clingo_assignment_t assignment)

Check if the given assignment is conflicting.

Parameters
[in]assignmentthe target assignment
Returns
whether the assignment is conflicting

◆ clingo_assignment_has_literal()

CLINGO_VISIBILITY_DEFAULT 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]assignmentthe target assignment
[in]literalthe literal
Returns
whether the literal is valid

◆ clingo_assignment_is_false()

CLINGO_VISIBILITY_DEFAULT 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]assignmentthe target assignment
[in]literalthe literal
[out]is_falsewhether 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 assignment,
clingo_literal_t  literal,
bool *  is_fixed 
)

Check if a literal has a fixed truth value.

Parameters
[in]assignmentthe target assignment
[in]literalthe literal
[out]is_fixedwhether 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 assignment)

Check if the assignmen is total, i.e.

  • size == max_size.
Parameters
[in]assignmentthe target
Returns
wheather the assignment is total

◆ clingo_assignment_is_true()

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

Check if a literal is true.

Parameters
[in]assignmentthe target assignment
[in]literalthe literal
[out]is_truewhether 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 assignment,
clingo_literal_t  literal,
uint32_t *  level 
)

Determine the decision level of a given literal.

Parameters
[in]assignmentthe target assignment
[in]literalthe literal
[out]levelthe resulting level
Returns
whether the call was successful

◆ clingo_assignment_max_size()

CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_max_size ( clingo_assignment_t assignment)

The maximum size of the assignment (if all literals are assigned).

Parameters
[in]assignmentthe target
Returns
the maximum size

◆ clingo_assignment_size()

CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_size ( clingo_assignment_t assignment)

The number of assigned literals in the assignment.

Parameters
[in]assignmentthe target
Returns
the number of literals

◆ clingo_assignment_truth_value()

CLINGO_VISIBILITY_DEFAULT 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]assignmentthe target assignment
[in]literalthe literal
[out]valuethe 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]controlthe target
[in]clausethe clause to add
[in]sizethe size of the clause
[in]typethe clause type determining its lifetime
[out]resultresult indicating whether propagation has to be stopped
Returns
whether the call was successful; might set one of the following error codes:
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]controlthe target
[out]resultthe (positive) solver literal
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]controlthe target
[in]literalthe literal to watch
Returns
whether the call was successful; might set one of the following error codes:
See also
clingo_propagate_control_remove_watch()

◆ clingo_propagate_control_assignment()

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t* clingo_propagate_control_assignment ( clingo_propagate_control_t control)

Get the assignment associated with the underlying solver.

Parameters
[in]controlthe target
Returns
the assignment

◆ clingo_propagate_control_has_watch()

CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_has_watch ( clingo_propagate_control_t control,
clingo_literal_t  literal 
)

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

Parameters
[in]controlthe target
[in]literalthe 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]controlthe target
[out]resultresult indicating whether propagation has to be stopped
Returns
whether the call was successful; might set one of the following error codes:
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]controlthe target
[in]literalthe literal to remove

◆ clingo_propagate_control_thread_id()

CLINGO_VISIBILITY_DEFAULT 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]controlthe target
Returns
the thread id
Examples:
propagator.c.

◆ 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]initthe target
[in]solver_literalthe 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,
uint32_t  thread_id 
)

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

Parameters
[in]initthe target
[in]solver_literalthe solver literal
[in]thread_idthe id of the solver thread
Returns
whether the call was successful

◆ clingo_propagate_init_assignment()

CLINGO_VISIBILITY_DEFAULT clingo_assignment_t* clingo_propagate_init_assignment ( clingo_propagate_init_t init)

Get the top level assignment solver.

Parameters
[in]initthe target
Returns
the assignment

◆ clingo_propagate_init_get_check_mode()

CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_get_check_mode ( clingo_propagate_init_t init)

Get the current check mode of the propagator.

Parameters
[in]initthe 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 init)

Get the number of threads used in subsequent solving.

Parameters
[in]initthe target
Returns
the number of threads
See also
clingo_propagate_control_thread_id()
Examples:
propagator.c.

◆ 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]initthe target
[in]modebitmask 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 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]initthe target
[in]aspif_literalthe aspif literal to map
[out]solver_literalthe 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 init,
clingo_symbolic_atoms_t **  atoms 
)

Get an object to inspect the symbolic atoms.

Parameters
[in]initthe target
[out]atomsthe 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 init,
clingo_theory_atoms_t **  atoms 
)

Get an object to inspect the theory atoms.

Parameters
[in]initthe target
[out]atomsthe resulting object
Returns
whether the call was successful