1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
|
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3_optimization.h
Abstract:
Optimization facilities
Author:
Christoph M. Wintersteiger (cwinter) 2015-12-03
Notes:
--*/
#ifndef Z3_OPTIMIZATION_H_
#define Z3_OPTIMIZATION_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name Optimization facilities */
/*@{*/
/**
\brief Create a new optimize context.
\remark User must use #Z3_optimize_inc_ref and #Z3_optimize_dec_ref to manage optimize objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_optimize', OPTIMIZE, (_in(CONTEXT), ))
*/
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
/**
\brief Increment the reference counter of the given optimize context
def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
/**
\brief Decrement the reference counter of the given optimize context.
def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
/**
\brief Assert hard constraint to the optimization context.
\sa Z3_optimize_assert_soft
def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
/**
\brief Assert soft constraint to the optimization context.
\param c - context
\param o - optimization context
\param a - formula
\param weight - a positive weight, penalty for violating soft constraint
\param id - optional identifier to group soft constraints
\sa Z3_optimize_assert
def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
*/
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
/**
\brief Add a maximization constraint.
\param c - context
\param o - optimization context
\param t - arithmetical term
\sa Z3_optimize_minimize
def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
/**
\brief Add a minimization constraint.
\param c - context
\param o - optimization context
\param t - arithmetical term
\sa Z3_optimize_maximize
def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
/**
\brief Create a backtracking point.
The optimize solver contains a set of rules, added facts and assertions.
The set of rules, facts and assertions are restored upon calling #Z3_optimize_pop.
\sa Z3_optimize_pop
def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
/**
\brief Backtrack one level.
\sa Z3_optimize_push
\pre The number of calls to pop cannot exceed calls to push.
def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
/**
\brief Check consistency and produce optimal values.
\param c - context
\param o - optimization context
\param num_assumptions - number of additional assumptions
\param assumptions - the additional assumptions
\sa Z3_optimize_get_reason_unknown
\sa Z3_optimize_get_model
\sa Z3_optimize_get_statistics
\sa Z3_optimize_get_unsat_core
def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
*/
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
/**
\brief Retrieve a string that describes the last status returned by #Z3_optimize_check.
Use this method when #Z3_optimize_check returns \c Z3_L_UNDEF.
def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) ))
*/
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
/**
\brief Retrieve the model for the last #Z3_optimize_check
The error handler is invoked if a model is not available because
the commands above were not invoked for the given optimization
solver, or if the result was \c Z3_L_FALSE.
def_API('Z3_optimize_get_model', MODEL, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
/**
\brief Retrieve the unsat core for the last #Z3_optimize_check
The unsat core is a subset of the assumptions \c a.
def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
/**
\brief Set parameters on optimization context.
\param c - context
\param o - optimization context
\param p - parameters
\sa Z3_optimize_get_help
\sa Z3_optimize_get_param_descrs
def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS)))
*/
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
/**
\brief Return the parameter description set for the given optimize object.
\param c - context
\param o - optimization context
\sa Z3_optimize_get_help
\sa Z3_optimize_set_params
def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
/**
\brief Retrieve lower bound value or approximation for the i'th optimization objective.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
\sa Z3_optimize_get_upper
\sa Z3_optimize_get_lower_as_vector
\sa Z3_optimize_get_upper_as_vector
def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Retrieve upper bound value or approximation for the i'th optimization objective.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
\sa Z3_optimize_get_lower
\sa Z3_optimize_get_lower_as_vector
\sa Z3_optimize_get_upper_as_vector
def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Retrieve lower bound value or approximation for the i'th optimization objective.
The returned vector is of length 3. It always contains numerals.
The three numerals are coefficients \c a, \c b, \c c and encode the result of
#Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
\sa Z3_optimize_get_lower
\sa Z3_optimize_get_upper
\sa Z3_optimize_get_upper_as_vector
def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Retrieve upper bound value or approximation for the i'th optimization objective.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
\sa Z3_optimize_get_lower
\sa Z3_optimize_get_upper
\sa Z3_optimize_get_lower_as_vector
def_API('Z3_optimize_get_upper_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Print the current context as a string.
\param c - context.
\param o - optimization context.
\sa Z3_optimize_from_file
\sa Z3_optimize_from_string
def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
/**
\brief Parse an SMT-LIB2 string with assertions,
soft constraints and optimization objectives.
Add the parsed constraints and objectives to the optimization context.
\param c - context.
\param o - optimize context.
\param s - string containing SMT2 specification.
\sa Z3_optimize_from_file
\sa Z3_optimize_to_string
def_API('Z3_optimize_from_string', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
*/
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
/**
\brief Parse an SMT-LIB2 file with assertions,
soft constraints and optimization objectives.
Add the parsed constraints and objectives to the optimization context.
\param c - context.
\param o - optimize context.
\param s - path to file containing SMT2 specification.
\sa Z3_optimize_from_string
\sa Z3_optimize_to_string
def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
*/
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
/**
\brief Return a string containing a description of parameters accepted by optimize.
\sa Z3_optimize_get_param_descrs
\sa Z3_optimize_set_params
def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
/**
\brief Retrieve statistics information from the last call to #Z3_optimize_check
def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
/**
\brief Return the set of asserted formulas on the optimization context.
def_API('Z3_optimize_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
/**
\brief Return objectives on the optimization context.
If the objective function is a max-sat objective it is returned
as a Pseudo-Boolean (minimization) sum of the form \ccode{(+ (if f1 w1 0) (if f2 w2 0) ...)}
If the objective function is entered as a maximization objective, then return
the corresponding minimization objective. In this way the resulting objective
function is always returned as a minimization objective.
def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif
|
