Clingo
Loading...
Searching...
No Matches
solve.h
1#ifndef CLINGO_SOLVE_H
2#define CLINGO_SOLVE_H
3
4#include <clingo/core.h>
5#include <clingo/model.h>
6#include <clingo/stats.h>
7
8#ifdef __cplusplus
9extern "C" {
10#endif
11
12typedef struct clingo_control clingo_control_t;
13
34
44
62
72
81 bool (*model)(clingo_model_t *model, void *data, bool *goon);
88 bool (*unsat)(int64_t const *values, size_t size, void *data);
94 bool (*stats)(clingo_stats_t *stats, void *data);
102 void (*finish)(clingo_solve_result_bitset_t result, void *data);
106 void (*free)(void *data);
108
112typedef struct clingo_solve_handle clingo_solve_handle_t;
113
123CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_get(clingo_solve_handle_t *handle,
134CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_wait(clingo_solve_handle_t *handle, double timeout, bool *result);
140CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_model(clingo_solve_handle_t *handle, clingo_model_t const **model);
149CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core(clingo_solve_handle_t *handle,
150 clingo_literal_t const **literals, size_t *size);
159CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_last(clingo_solve_handle_t *handle, clingo_model_t const **model);
169CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_resume(clingo_solve_handle_t *handle);
174CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_cancel(clingo_solve_handle_t *handle);
181CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_close(clingo_solve_handle_t *handle);
182
195CLINGO_VISIBILITY_DEFAULT bool clingo_control_solve(clingo_control_t *control, clingo_solve_mode_bitset_t mode,
196 clingo_literal_t const *assumptions, size_t assumptions_size,
197 clingo_solve_event_handler_t const *handler, void *data,
198 clingo_solve_handle_t **handle);
199
201
202#ifdef __cplusplus
203}
204#endif
205
206#endif
int32_t clingo_literal_t
Signed integer type used for aspif and solver literals.
Definition core.h:73
struct clingo_model clingo_model_t
Object representing a model.
Definition model.h:43
struct clingo_solve_handle clingo_solve_handle_t
Search handle to a solve call.
Definition solve.h:112
clingo_solve_result_e
Enumeration of bit masks for solve call results.
Definition solve.h:53
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.
unsigned clingo_solve_result_bitset_t
Corresponding type to clingo_solve_result_e.
Definition solve.h:61
clingo_solve_mode_e
Enumeration of solve modes.
Definition solve.h:64
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_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.
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.
unsigned clingo_solve_mode_bitset_t
Corresponding type to clingo_solve_mode_e.
Definition solve.h:71
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_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_get(clingo_solve_handle_t *handle, clingo_solve_result_bitset_t *result)
Get the next solve result.
struct clingo_solve_event_handler clingo_solve_event_handler_t
The solve event handler interface.
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_solve_result_satisfiable
The last solve call found a solution.
Definition solve.h:55
@ clingo_solve_result_interrupted
The last solve call was interrupted.
Definition solve.h:58
@ clingo_solve_result_empty
An uninitialized solve result.
Definition solve.h:54
@ clingo_solve_result_exhausted
The last solve call completely exhausted the search space.
Definition solve.h:57
@ clingo_solve_result_unsatisfiable
The last solve call did not find a solution.
Definition solve.h:56
@ clingo_solve_mode_lock
Ensure callbacks are executed in lock-step.
Definition solve.h:68
@ clingo_solve_mode_yield
Yield models in calls to clingo_solve_handle_model.
Definition solve.h:67
@ clingo_solve_mode_default
The defalut solve mode.
Definition solve.h:65
@ clingo_solve_mode_async
Enable non-blocking search.
Definition solve.h:66
struct clingo_statistic clingo_stats_t
Handle for the solver stats.
Definition stats.h:59
The solve event handler interface.
Definition solve.h:74
bool(* unsat)(int64_t const *values, size_t size, void *data)
Callback to interept lower bounds.
Definition solve.h:88
bool(* stats)(clingo_stats_t *stats, void *data)
Callback to extend statistics.
Definition solve.h:94
bool(* model)(clingo_model_t *model, void *data, bool *goon)
Call back to intercept models.
Definition solve.h:81
void(* free)(void *data)
Callback to free the userdata of the handler.
Definition solve.h:106
void(* finish)(clingo_solve_result_bitset_t result, void *data)
Callback to notify that the search has finished.
Definition solve.h:102