|
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... | |
| void Z3_API | Z3_optimize_set_initial_value (Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val) |
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that represents a variable. If the variable is Boolean, the initial phase is set according to value. If the variable is an integer or real, the initial Simplex tableau is recalibrated to attempt to follow the value assignment. 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