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]	event	the current event.
[in]	data	user data of the callback
[out]	goon	can 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

enum 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

enum 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] handle the target

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc
clingo_error_runtime if solving fails

◆ 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] handle the target

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc
clingo_error_runtime if solving fails

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]	handle	the target
[out]	core	pointer where to store the core
[out]	size	size of the given array

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc

◆ 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]	handle	the target
[out]	result	the solve result

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc
clingo_error_runtime if solving fails

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]	handle	the target
[out]	model	the model (it is NULL if there are no more models)

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc
clingo_error_runtime if solving fails

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] handle the target

Returns

whether the call was successful; might set one of the following error codes:

clingo_error_bad_alloc
clingo_error_runtime if solving fails

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]	handle	the target
[in]	timeout	the maximum time to wait
[out]	result	whether the search has finished

Detailed Description

Typedefs

Enumerations

Functions

Typedef Documentation

◆ clingo_solve_event_callback_t

◆ clingo_solve_handle_t

Enumeration Type Documentation

◆ clingo_solve_event_type_e

◆ clingo_solve_mode_e

Function Documentation

◆ clingo_solve_handle_cancel()

◆ clingo_solve_handle_close()

◆ clingo_solve_handle_core()

◆ clingo_solve_handle_get()

◆ clingo_solve_handle_model()

◆ clingo_solve_handle_resume()

◆ clingo_solve_handle_wait()