Z3 |

z3_optimization.h
Go to the documentation of this file.
1/*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 Module Name:
5
6 z3_optimization.h
7
8 Abstract:
9
10 Optimization facilities
11
12 Author:
13
14 Christoph M. Wintersteiger (cwinter) 2015-12-03
15
16 Notes:
17
18--*/
19#pragma once
20
24 typedef void Z3_model_eh(void* ctx);
25
26#ifdef __cplusplus
27 extern "C" {
28#endif // __cplusplus
29
32
42 Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
43
48 void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
49
54 void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
55
63 void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
64
65
73 void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t);
74
87 unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
88
98 unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
99
109 unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
110
120 void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
121
130 void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
131
145 Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
146
147
154 Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
155
164 Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
165
171 Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
172
184 void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
185
196 Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
197
210 Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
211
224 Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
225
226
242 Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
243
256 Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
257
258
268 Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
269
283 void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
284
298 void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
299
307 Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
308
313 Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
314
319 Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
320
330 Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
331
332
336 void Z3_API Z3_optimize_register_model_eh(
337 Z3_context c,
338 Z3_optimize o,
339 Z3_model m,
340 void* ctx,
341 Z3_model_eh model_eh);
342
343
346
347#ifdef __cplusplus
348}
349#endif // __cplusplus
350
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_optimize_get_assertions
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
Z3_optimize_get_unsat_core
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_optimize_get_upper_as_vector
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_optimize_get_lower
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
Z3_optimize_get_model
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
Z3_optimize_from_file
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_optimize_get_lower_as_vector
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector ...
Z3_optimize_assert_and_track
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
Z3_optimize_assert_soft
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
Z3_optimize_get_param_descrs
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)
Return the parameter description set for the given optimize object.
Z3_optimize_inc_ref
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_optimize_get_upper
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_optimize_set_params
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_optimize_push
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_model_eh
void Z3_model_eh(void *ctx)
callback functions for models.
Definition: z3_optimization.h:24
Z3_optimize_get_objectives
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_optimize_assert
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_mk_optimize
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
Z3_optimize_dec_ref
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_optimize_get_help
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_optimize_get_statistics
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_optimize_minimize
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Z3_optimize_maximize
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_optimize_get_reason_unknown
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d)
Retrieve a string that describes the last status returned by Z3_optimize_check.
Z3_optimize_from_string
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_optimize_register_model_eh
void Z3_API Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)
register a model event handler for new models.
Z3_optimize_check
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.