Interact with a running search. More...

Classes
struct	clingo_solve_event_handler
	The solve event handler interface. More...

Typedefs
typedef unsigned	clingo_solve_result_bitset_t
	Corresponding type to clingo_solve_result_e.

typedef unsigned	clingo_solve_mode_bitset_t
	Corresponding type to clingo_solve_mode_e.

typedef struct clingo_solve_event_handler	clingo_solve_event_handler_t
	The solve event handler interface.

typedef struct clingo_solve_handle	clingo_solve_handle_t
	Search handle to a solve call.

Enumerations
enum	clingo_solve_result_e { clingo_solve_result_satisfiable = 1 , clingo_solve_result_unsatisfiable = 2 , clingo_solve_result_exhausted = 4 , clingo_solve_result_interrupted = 8 }
	Enumeration of bit masks for solve call results. More...

enum	clingo_solve_mode_e { clingo_solve_mode_async = 1 , clingo_solve_mode_yield = 2 , clingo_solve_mode_lock = 4 }
	Enumeration of solve modes. 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.

CLINGO_VISIBILITY_DEFAULT bool	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.

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).

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_handle_core (clingo_solve_handle_t handle, clingo_literal_t const literals, size_t size)
	When a problem is unsatisfiable, get a subset of the assumptions that made the problem unsatisfiable.

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_handle_last (clingo_solve_handle_t handle, clingo_model_t const *model)
	When a problem is satisfiable and the search is finished, get the last computed model.

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.

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_handle_cancel (clingo_solve_handle_t *handle)
	Stop the running search and block until done.

CLINGO_VISIBILITY_DEFAULT bool	clingo_solve_handle_close (clingo_solve_handle_t *handle)
	Stops the running search and releases the handle.

CLINGO_VISIBILITY_DEFAULT bool	clingo_control_solve (clingo_control_t control, clingo_solve_mode_bitset_t mode, clingo_literal_t const assumptions, size_t assumptions_size, clingo_solve_event_handler_t const handler, void data, clingo_solve_handle_t **handle)
	Solve the currently grounded logic program enumerating its models.

Detailed Description

Interact with a running search.

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.c.

Typedef Documentation

◆ 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_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.
clingo_solve_mode_lock	Ensure callbacks are executed in lock-step.

◆ clingo_solve_result_e

enum clingo_solve_result_e

Enumeration of bit masks for solve call results.

Note: Neither clingo_solve_result_satisfiable nor clingo_solve_result_exhausted is set if the search is interrupted and no model was found.

See also: clingo_control_interrupt()

Enumerator
clingo_solve_result_satisfiable	The last solve call found a solution.
clingo_solve_result_unsatisfiable	The last solve call did not find a solution.
clingo_solve_result_exhausted	The last solve call completely exhausted the search space.
clingo_solve_result_interrupted	The last solve call was interrupted.

Function Documentation

◆ clingo_control_solve()

CLINGO_VISIBILITY_DEFAULT bool clingo_control_solve	(	clingo_control_t *	control,
		clingo_solve_mode_bitset_t	mode,
		clingo_literal_t const *	assumptions,
		size_t	assumptions_size,
		clingo_solve_event_handler_t const *	handler,
		void *	data,
		clingo_solve_handle_t **	handle
	)

Solve the currently grounded logic program enumerating its models.

See the Solving module for more information.

Parameters

[in]	control	the target
[in]	mode	configures the search mode
[in]	assumptions	array of assumptions to solve under
[in]	assumptions_size	number of assumptions
[in]	handler	the event handler to register
[in]	data	the user data for the event handler
[out]	handle	handle to the current search to enumerate models

Returns: wether the call was successful

Examples: control.c.

◆ 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: wether the call was successful

◆ 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: wether the call was successful

◆ clingo_solve_handle_core()

CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core	(	clingo_solve_handle_t *	handle,
		clingo_literal_t const **	literals,
		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, an empty core is returned.

Parameters

[in]	handle	the target
[out]	literals	array of literals in the core
[out]	size	the size of the core

Returns: wether the call was successful

◆ 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: wether the call was successful

Examples: control.c.

◆ clingo_solve_handle_last()

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

When a problem is satisfiable and the search is finished, get the last computed model.

If the program is unsatisfiable or the search is not finished, model is set to NULL.

Parameters

[in]	handle	the target
[out]	model	the last computed model (or NULL if the program is unsatisfiable or the search is still ongoing)

Returns: wether the call was successful

◆ 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: wether the call was successful

◆ 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: wether the call was successful

◆ clingo_solve_handle_wait()

CLINGO_VISIBILITY_DEFAULT bool 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

Returns: wether the call was successful

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ clingo_solve_handle_t

Enumeration Type Documentation

◆ clingo_solve_mode_e

◆ clingo_solve_result_e

Function Documentation

◆ clingo_control_solve()

◆ clingo_solve_handle_cancel()

◆ clingo_solve_handle_close()

◆ clingo_solve_handle_core()

◆ clingo_solve_handle_get()

◆ clingo_solve_handle_last()

◆ clingo_solve_handle_model()

◆ clingo_solve_handle_resume()

◆ clingo_solve_handle_wait()