Clingo C API
C API for clingo providing high level functions to control grounding and solving.
|
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_t * | clingo_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_t * | clingo_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 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 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.
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.
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 |
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 |
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.
[in] | assignment | the target assignment |
[in] | level | the level |
[out] | literal | the resulting literal |
CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_decision_level | ( | clingo_assignment_t * | assignment | ) |
Get the current decision level.
[in] | assignment | the target assignment |
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict | ( | clingo_assignment_t * | assignment | ) |
Check if the given assignment is conflicting.
[in] | assignment | the target assignment |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
[out] | is_false | whether the literal is false |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
[out] | is_fixed | whether the literal is fixed |
CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total | ( | clingo_assignment_t * | assignment | ) |
Check if the assignmen is total, i.e.
[in] | assignment | the target |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
[out] | is_true | whether the literal is true |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
[out] | level | the resulting level |
CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_max_size | ( | clingo_assignment_t * | assignment | ) |
The maximum size of the assignment (if all literals are assigned).
[in] | assignment | the target |
CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_size | ( | clingo_assignment_t * | assignment | ) |
The number of assigned literals in the assignment.
[in] | assignment | the target |
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.
[in] | assignment | the target assignment |
[in] | literal | the literal |
[out] | value | the resulting truth value |
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.
[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 |
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.
[in] | control | the target |
[out] | result | the (positive) solver literal |
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.
[in] | control | the target |
[in] | literal | the literal to watch |
CLINGO_VISIBILITY_DEFAULT clingo_assignment_t* clingo_propagate_control_assignment | ( | clingo_propagate_control_t * | control | ) |
Get the assignment associated with the underlying solver.
[in] | control | the target |
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.
[in] | control | the target |
[in] | literal | the literal to check |
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.
[in] | control | the target |
[out] | result | result indicating whether propagation has to be stopped |
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.
[in] | control | the target |
[in] | literal | the literal to remove |
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.
[in] | control | the target |
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.
[in] | init | the target |
[in] | solver_literal | the solver literal |
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.
[in] | init | the target |
[in] | solver_literal | the solver literal |
[in] | thread_id | the id of the solver thread |
CLINGO_VISIBILITY_DEFAULT clingo_assignment_t* clingo_propagate_init_assignment | ( | clingo_propagate_init_t * | init | ) |
Get the top level assignment solver.
[in] | init | the target |
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.
[in] | init | the target |
CLINGO_VISIBILITY_DEFAULT int clingo_propagate_init_number_of_threads | ( | clingo_propagate_init_t * | init | ) |
Get the number of threads used in subsequent solving.
[in] | init | the target |
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.
[in] | init | the target |
[in] | mode | bitmask when to call the propagator |
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.
[in] | init | the target |
[in] | aspif_literal | the aspif literal to map |
[out] | solver_literal | the resulting solver literal |
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.
[in] | init | the target |
[out] | atoms | the resulting object |
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.
[in] | init | the target |
[out] | atoms | the resulting object |