Solving

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.
typedef unsigned	clingo_solve_event_type_t
	Corresponding type to clingo_solve_event_type.
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 { clingo_solve_mode_async = 1, clingo_solve_mode_yield = 2 }
	Enumeration of solve modes. More...
enum	clingo_solve_event_type { clingo_solve_event_type_model = 0, clingo_solve_event_type_finish = 1 }
	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 **model)
	Get the next model (or zero if there are no more models). 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.

Attention

If the search is finished, the model is NULL.

Parameters

[in]	model	the current model
[in]	data	user data of the callback
[in]	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

enum clingo_solve_event_type

Enumeration of solve events.

Enumerator
clingo_solve_event_type_model	Issued if a model is found.
clingo_solve_event_type_finish	Issued if the search has completed.

clingo_solve_mode

enum clingo_solve_mode

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:

ast.c, backend.c, configuration.c, control.c, model.c, propagator.c, solve-async.c, statistics.c, and theory-atoms.c.

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:

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 **	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:

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:

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