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

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

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

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

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]assignmentthe target
[in]offsetthe offset of the literal
[out]literalthe 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]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 const *  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 const *  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 const *  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 const *  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 const *  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 const *  assignment)

Check if the assignment is total, i.e.

there are no free literal.

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 const *  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 const *  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_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]assignmentthe 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]assignmentthe 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]assignmentthe target
[in]offsetthe offset of the literal
[out]literalthe 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]assignmentthe target
[in]levelthe decision level
[out]offsetthe 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]assignmentthe target
[in]levelthe decision level
[out]offsetthe 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]assignmentthe target
[out]sizethe 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]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 const* clingo_propagate_control_assignment ( clingo_propagate_control_t const *  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 const *  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 const *  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_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]initthe target
[in]clausethe clause to add
[in]sizethe size of the clause
[out]resultresult indicating whether the problem became unsatisfiable
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]initthe target
[in]freezewhether to freeze the literal
[out]resultthe added literal
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]initthe target
[in]literalthe literal to minimize
[in]weightthe weight of the literal
[in]prioritythe priority of the literal
Returns
whether the call was successful; might set one of the following error codes:

◆ 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,
clingo_id_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_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]initthe target
[in]literalthe literal of the constraint
[in]literalsthe weighted literals
[in]sizethe number of weighted literals
[in]boundthe bound of the constraint
[in]typethe type of the weight constraint
[in]compare_equalif true compare equal instead of less than equal
[out]resultresult indicating whether the problem became unsatisfiable
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]initthe 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]initthe target
[in]solver_literalthe 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]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 const *  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_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]initthe target
[out]resultresult indicating whether the problem became unsatisfiable
Returns
whether the call was successful; might set one of the following error codes:

◆ 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]initthe target
[in]solver_literalthe 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]initthe target
[in]solver_literalthe solver literal
[in]thread_idthe 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]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 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]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 const *  init,
clingo_symbolic_atoms_t const **  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 const *  init,
clingo_theory_atoms_t const **  atoms 
)

Get an object to inspect the theory atoms.

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