|
Z3
|
|
|
Z3
|
|
Go to the source code of this file.
Typedefs | |
| typedef void | Z3_model_eh(void *ctx) |
| callback functions for models. More... | |
Functions | |
Optimization facilities | |
| Z3_optimize Z3_API | Z3_mk_optimize (Z3_context c) |
| Create a new optimize context. More... | |
| void Z3_API | Z3_optimize_inc_ref (Z3_context c, Z3_optimize d) |
| Increment the reference counter of the given optimize context. More... | |
| void Z3_API | Z3_optimize_dec_ref (Z3_context c, Z3_optimize d) |
| Decrement the reference counter of the given optimize context. More... | |
| void Z3_API | Z3_optimize_assert (Z3_context c, Z3_optimize o, Z3_ast a) |
| Assert hard constraint to the optimization context. More... | |
| 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. More... | |
| 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. More... | |
| unsigned Z3_API | Z3_optimize_maximize (Z3_context c, Z3_optimize o, Z3_ast t) |
| Add a maximization constraint. More... | |
| unsigned Z3_API | Z3_optimize_minimize (Z3_context c, Z3_optimize o, Z3_ast t) |
| Add a minimization constraint. More... | |
| void Z3_API | Z3_optimize_push (Z3_context c, Z3_optimize d) |
| Create a backtracking point. More... | |
| void Z3_API | Z3_optimize_pop (Z3_context c, Z3_optimize d) |
| Backtrack one level. More... | |
| 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. More... | |
| 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. More... | |
| Z3_model Z3_API | Z3_optimize_get_model (Z3_context c, Z3_optimize o) |
| Retrieve the model for the last Z3_optimize_check. More... | |
| 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 a. More... | |
| void Z3_API | Z3_optimize_set_params (Z3_context c, Z3_optimize o, Z3_params p) |
| Set parameters on optimization context. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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 is of length 3. It always contains numerals. The three numerals are coefficients a, b, c and encode the result of Z3_optimize_get_lower a * infinity + b + c * epsilon. More... | |
| 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. More... | |
| Z3_string Z3_API | Z3_optimize_to_string (Z3_context c, Z3_optimize o) |
| Print the current context as a string. More... | |
| 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. Add the parsed constraints and objectives to the optimization context. More... | |
| 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. Add the parsed constraints and objectives to the optimization context. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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 returned as a Pseudo-Boolean (minimization) sum of the form (+ (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. More... | |
| 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. More... | |
| typedef void Z3_model_eh(void *ctx) |
callback functions for models.
Definition at line 24 of file z3_optimization.h.
1.9.1