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

Detailed Description

Interact with a running search.

A clingo_solve_handle_t objects can be used for both synchronous and asynchronous search, as well as iteratively receiving models and solve results.

For an example showing how to solve asynchronously, see solve-async.c.

Typedefs

typedef unsigned clingo_solve_mode_bitset_t
 Corresponding type to clingo_solve_mode_e.
 
typedef unsigned clingo_solve_event_type_t
 Corresponding type to clingo_solve_event_type_e.
 
typedef bool(* clingo_solve_event_callback_t) (clingo_solve_event_type_t type, void *event, void *data, bool *goon)
 Callback function called during search to notify when the search is finished or a model is ready. More...
 
typedef struct clingo_solve_handle clingo_solve_handle_t
 Search handle to a solve call. More...
 

Enumerations

enum  clingo_solve_mode_e { clingo_solve_mode_async = 1, clingo_solve_mode_yield = 2 }
 Enumeration of solve modes. More...
 
enum  clingo_solve_event_type_e { clingo_solve_event_type_model = 0, clingo_solve_event_type_unsat = 1, clingo_solve_event_type_statistics = 2, clingo_solve_event_type_finish = 3 }
 Enumeration of solve events. More...
 

Functions

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_get (clingo_solve_handle_t *handle, clingo_solve_result_bitset_t *result)
 Get the next solve result. More...
 
CLINGO_VISIBILITY_DEFAULT void clingo_solve_handle_wait (clingo_solve_handle_t *handle, double timeout, bool *result)
 Wait for the specified amount of time to check if the next result is ready. More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_model (clingo_solve_handle_t *handle, clingo_model_t const **model)
 Get the next model (or zero if there are no more models). More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core (clingo_solve_handle_t *handle, clingo_literal_t const **core, size_t *size)
 When a problem is unsatisfiable, get a subset of the assumptions that made the problem unsatisfiable. More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_resume (clingo_solve_handle_t *handle)
 Discards the last model and starts the search for the next one. More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_cancel (clingo_solve_handle_t *handle)
 Stop the running search and block until done. More...
 
CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_close (clingo_solve_handle_t *handle)
 Stops the running search and releases the handle. More...
 

Typedef Documentation

◆ clingo_solve_event_callback_t

typedef bool(* clingo_solve_event_callback_t) (clingo_solve_event_type_t type, void *event, void *data, bool *goon)

Callback function called during search to notify when the search is finished or a model is ready.

If a (non-recoverable) clingo API function fails in this callback, it must return false. In case of errors not related to clingo, set error code clingo_error_unknown and return false to stop solving with an error.

The event is either a pointer to a model, a pointer to an int64_t* and a size_t, a pointer to two statistics objects (per step and accumulated statistics), or a solve result.

Attention
If the search is finished, the model is NULL.
Parameters
[in]eventthe current event.
[in]datauser data of the callback
[out]gooncan be set to false to stop solving
Returns
whether the call was successful
See also
clingo_control_solve()

◆ clingo_solve_handle_t

typedef struct clingo_solve_handle clingo_solve_handle_t

Search handle to a solve call.

See also
clingo_control_solve()

Enumeration Type Documentation

◆ clingo_solve_event_type_e

Enumeration of solve events.

Enumerator
clingo_solve_event_type_model 

Issued if a model is found.

clingo_solve_event_type_unsat 

Issued if an optimization problem is found unsatisfiable.

clingo_solve_event_type_statistics 

Issued when the statistics can be updated.

clingo_solve_event_type_finish 

Issued if the search has completed.

◆ clingo_solve_mode_e

Enumeration of solve modes.

Enumerator
clingo_solve_mode_async 

Enable non-blocking search.

clingo_solve_mode_yield 

Yield models in calls to clingo_solve_handle_model.

Function Documentation

◆ clingo_solve_handle_cancel()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_cancel ( clingo_solve_handle_t handle)

Stop the running search and block until done.

Parameters
[in]handlethe target
Returns
whether the call was successful; might set one of the following error codes:

◆ clingo_solve_handle_close()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_close ( clingo_solve_handle_t handle)

Stops the running search and releases the handle.

Blocks until the search is stopped (as if an implicit cancel was called before the handle is released).

Parameters
[in]handlethe target
Returns
whether the call was successful; might set one of the following error codes:
Examples:
application.c, ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, statistics.c, and theory-atoms.c.

◆ clingo_solve_handle_core()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core ( clingo_solve_handle_t handle,
clingo_literal_t const **  core,
size_t *  size 
)

When a problem is unsatisfiable, get a subset of the assumptions that made the problem unsatisfiable.

If the program is not unsatisfiable, core is set to NULL and size to zero.

Parameters
[in]handlethe target
[out]corepointer where to store the core
[out]sizesize of the given array
Returns
whether the call was successful; might set one of the following error codes:

◆ clingo_solve_handle_get()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_get ( clingo_solve_handle_t handle,
clingo_solve_result_bitset_t result 
)

Get the next solve result.

Blocks until the result is ready. When yielding partial solve results can be obtained, i.e., when a model is ready, the result will be satisfiable but neither the search exhausted nor the optimality proven.

Parameters
[in]handlethe target
[out]resultthe solve result
Returns
whether the call was successful; might set one of the following error codes:
Examples:
application.c, ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, statistics.c, and theory-atoms.c.

◆ clingo_solve_handle_model()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_model ( clingo_solve_handle_t handle,
clingo_model_t const **  model 
)

Get the next model (or zero if there are no more models).

Parameters
[in]handlethe target
[out]modelthe model (it is NULL if there are no more models)
Returns
whether the call was successful; might set one of the following error codes:
Examples:
application.c, ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, statistics.c, and theory-atoms.c.

◆ clingo_solve_handle_resume()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_resume ( clingo_solve_handle_t handle)

Discards the last model and starts the search for the next one.

If the search has been started asynchronously, this function continues the search in the background.

Note
This function does not block.
Parameters
[in]handlethe target
Returns
whether the call was successful; might set one of the following error codes:
Examples:
application.c, ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, statistics.c, and theory-atoms.c.

◆ clingo_solve_handle_wait()

CLINGO_VISIBILITY_DEFAULT void clingo_solve_handle_wait ( clingo_solve_handle_t handle,
double  timeout,
bool *  result 
)

Wait for the specified amount of time to check if the next result is ready.

If the time is set to zero, this function can be used to poll if the search is still active. If the time is negative, the function blocks until the search is finished.

Parameters
[in]handlethe target
[in]timeoutthe maximum time to wait
[out]resultwhether the search has finished