Go to the source code of this file.
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... | |
Z3_optimize Z3_API Z3_mk_optimize | ( | Z3_context | c | ) |
Create a new optimize context.
Referenced by optimize::optimize().
void Z3_API Z3_optimize_assert | ( | Z3_context | c, |
Z3_optimize | o, | ||
Z3_ast | a | ||
) |
Assert hard constraint to the optimization context.
Referenced by optimize::add(), and Optimize::assert_exprs().
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.
Referenced by optimize::add(), and Optimize::assert_and_track().
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.
c | - context |
o | - optimization context |
a | - formula |
weight | - a positive weight, penalty for violating soft constraint |
id | - optional identifier to group soft constraints |
Referenced by optimize::add(), and Optimize::add_soft().
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.
c | - context |
o | - optimization context |
num_assumptions | - number of additional assumptions |
assumptions | - the additional assumptions |
Referenced by optimize::check(), and Optimize::check().
void Z3_API Z3_optimize_dec_ref | ( | Z3_context | c, |
Z3_optimize | d | ||
) |
Decrement the reference counter of the given optimize context.
Referenced by Optimize::__del__(), optimize::operator=(), and optimize::~optimize().
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.
c | - context. |
o | - optimize context. |
s | - path to file containing SMT2 specification. |
Referenced by optimize::from_file(), and Optimize::from_file().
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.
c | - context. |
o | - optimize context. |
s | - string containing SMT2 specification. |
Referenced by optimize::from_string(), and Optimize::from_string().
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.
Referenced by optimize::assertions(), and Optimize::assertions().
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.
Referenced by optimize::help(), and Optimize::help().
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.
c | - context |
o | - optimization context |
idx | - index of optimization objective |
Referenced by optimize::lower(), and OptimizeObjective::lower().
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
.
c | - context |
o | - optimization context |
idx | - index of optimization objective |
Referenced by OptimizeObjective::lower_values().
Z3_model Z3_API Z3_optimize_get_model | ( | Z3_context | c, |
Z3_optimize | o | ||
) |
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 Z3_L_FALSE
.
Referenced by optimize::get_model(), and Optimize::model().
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.
Referenced by optimize::objectives(), and Optimize::objectives().
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.
c | - context |
o | - optimization context |
Referenced by Optimize::param_descrs().
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.
Use this method when Z3_optimize_check returns Z3_L_UNDEF
.
Referenced by Optimize::reason_unknown().
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.
Referenced by optimize::statistics(), and Optimize::statistics().
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
.
Referenced by optimize::unsat_core(), and Optimize::unsat_core().
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.
c | - context |
o | - optimization context |
idx | - index of optimization objective |
Referenced by optimize::upper(), and OptimizeObjective::upper().
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.
c | - context |
o | - optimization context |
idx | - index of optimization objective |
Referenced by OptimizeObjective::upper_values().
void Z3_API Z3_optimize_inc_ref | ( | Z3_context | c, |
Z3_optimize | d | ||
) |
Increment the reference counter of the given optimize context.
Referenced by optimize::operator=(), and optimize::optimize().
unsigned Z3_API Z3_optimize_maximize | ( | Z3_context | c, |
Z3_optimize | o, | ||
Z3_ast | t | ||
) |
Add a maximization constraint.
c | - context |
o | - optimization context |
t | - arithmetical term |
Referenced by optimize::maximize(), and Optimize::maximize().
unsigned Z3_API Z3_optimize_minimize | ( | Z3_context | c, |
Z3_optimize | o, | ||
Z3_ast | t | ||
) |
Add a minimization constraint.
c | - context |
o | - optimization context |
t | - arithmetical term |
Referenced by optimize::minimize(), and Optimize::minimize().
void Z3_API Z3_optimize_pop | ( | Z3_context | c, |
Z3_optimize | d | ||
) |
Backtrack one level.
Referenced by optimize::pop(), and Optimize::pop().
void Z3_API Z3_optimize_push | ( | Z3_context | c, |
Z3_optimize | d | ||
) |
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.
Referenced by optimize::push(), and Optimize::push().
void Z3_API Z3_optimize_set_params | ( | Z3_context | c, |
Z3_optimize | o, | ||
Z3_params | p | ||
) |
Set parameters on optimization context.
c | - context |
o | - optimization context |
p | - parameters |
Referenced by optimize::set(), and Optimize::set().
Z3_string Z3_API Z3_optimize_to_string | ( | Z3_context | c, |
Z3_optimize | o | ||
) |
Print the current context as a string.
c | - context. |
o | - optimization context. |
Referenced by Optimize::sexpr().