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 #ifndef Z3_OPTIMIZATION_H_
20 #define Z3_OPTIMIZATION_H_
21 
22 #ifdef __cplusplus
23 extern "C" {
24 #endif // __cplusplus
25 
28 
38  Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
39 
44  void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
45 
50  void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
51 
59  void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
60 
61 
69  void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t);
70 
83  unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
84 
94  unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
95 
105  unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
106 
116  void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
117 
126  void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
127 
141  Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
142 
143 
150  Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
151 
160  Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
161 
167  Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
168 
180  void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
181 
192  Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
193 
206  Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
207 
220  Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
221 
222 
238  Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
239 
252  Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
253 
254 
264  Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
265 
279  void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
280 
294  void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
295 
303  Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
304 
309  Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
310 
315  Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
316 
326  Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
327 
330 
331 #ifdef __cplusplus
332 }
333 #endif // __cplusplus
334 
335 #endif
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_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 Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
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.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
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.
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.
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
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_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:99
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
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_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
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_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_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_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.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
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.
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_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_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 ...
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
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....
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:82