#include <z3++.h>
Definition at line 3287 of file z3++.h.
◆ optimize() [1/3]
Definition at line 3297 of file z3++.h.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
Referenced by operator<<, operator=(), optimize(), and optimize().
◆ optimize() [2/3]
Definition at line 3298 of file z3++.h.
3298 :object(o), m_opt(o.m_opt) {
3300 }
◆ optimize() [3/3]
Definition at line 3301 of file z3++.h.
3301 :object(c) {
3306 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3307 }
ast_vector_tpl< expr > expr_vector
◆ ~optimize()
Definition at line 3315 of file z3++.h.
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
◆ add() [1/5]
void add |
( |
expr const & | e | ) |
|
|
inline |
Definition at line 3317 of file z3++.h.
3317 {
3318 assert(e.is_bool());
3320 }
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Referenced by add(), add(), and optimize().
◆ add() [2/5]
void add |
( |
expr const & | e, |
|
|
char const * | p ) |
|
inline |
Definition at line 3328 of file z3++.h.
3328 {
3329 assert(e.is_bool());
3330 add(e, ctx().bool_const(p));
3331 }
◆ add() [3/5]
void add |
( |
expr const & | e, |
|
|
expr const & | t ) |
|
inline |
Definition at line 3324 of file z3++.h.
3324 {
3325 assert(e.is_bool());
3327 }
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.
◆ add() [4/5]
Definition at line 3341 of file z3++.h.
3341 {
3342 return add_soft(e, weight);
3343 }
◆ add() [5/5]
Definition at line 3321 of file z3++.h.
3321 {
3322 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3323 }
◆ add_soft() [1/2]
handle add_soft |
( |
expr const & | e, |
|
|
char const * | weight ) |
|
inline |
Definition at line 3337 of file z3++.h.
3337 {
3338 assert(e.is_bool());
3340 }
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.
◆ add_soft() [2/2]
handle add_soft |
( |
expr const & | e, |
|
|
unsigned | weight ) |
|
inline |
Definition at line 3332 of file z3++.h.
3332 {
3333 assert(e.is_bool());
3334 auto str = std::to_string(weight);
3336 }
Referenced by add().
◆ assertions()
Definition at line 3392 of file z3++.h.
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().
◆ check() [1/2]
Definition at line 3367 of file z3++.h.
Z3_lbool
Lifted Boolean type: false, undefined, true.
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.
check_result to_check_result(Z3_lbool l)
◆ check() [2/2]
Definition at line 3368 of file z3++.h.
3368 {
3369 unsigned n = asms.size();
3370 array<Z3_ast> _asms(n);
3371 for (unsigned i = 0; i < n; i++) {
3373 _asms[i] = asms[i];
3374 }
3376 check_error();
3378 }
void check_context(object const &a, object const &b)
◆ from_file()
void from_file |
( |
char const * | filename | ) |
|
|
inline |
Definition at line 3396 of file z3++.h.
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....
◆ from_string()
void from_string |
( |
char const * | constraints | ) |
|
|
inline |
Definition at line 3397 of file z3++.h.
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....
◆ get_model()
model get_model |
( |
| ) |
const |
|
inline |
Definition at line 3379 of file z3++.h.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
◆ help()
std::string help |
( |
| ) |
const |
|
inline |
Definition at line 3398 of file z3++.h.
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.
◆ lower()
Definition at line 3382 of file z3++.h.
3382 {
3384 check_error();
3385 return expr(ctx(), r);
3386 }
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.
◆ maximize()
Definition at line 3355 of file z3++.h.
3355 {
3357 }
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
◆ minimize()
Definition at line 3358 of file z3++.h.
3358 {
3360 }
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Referenced by optimize().
◆ objectives()
Definition at line 3393 of file z3++.h.
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...
Referenced by optimize().
◆ operator Z3_optimize()
operator Z3_optimize |
( |
| ) |
const |
|
inline |
◆ operator=()
Definition at line 3308 of file z3++.h.
3308 {
3311 m_opt = o.m_opt;
3312 object::operator=(o);
3313 return *this;
3314 }
◆ pop()
Definition at line 3364 of file z3++.h.
3364 {
3366 }
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
◆ push()
Definition at line 3361 of file z3++.h.
3361 {
3363 }
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
◆ set()
Definition at line 3381 of file z3++.h.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
◆ set_initial_value() [1/3]
void set_initial_value |
( |
expr const & | var, |
|
|
bool | b ) |
|
inline |
Definition at line 3351 of file z3++.h.
3351 {
3352 set_initial_value(var, ctx().bool_val(b));
3353 }
◆ set_initial_value() [2/3]
void set_initial_value |
( |
expr const & | var, |
|
|
expr const & | value ) |
|
inline |
Definition at line 3344 of file z3++.h.
3344 {
3346 check_error();
3347 }
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...
Referenced by set_initial_value(), and set_initial_value().
◆ set_initial_value() [3/3]
void set_initial_value |
( |
expr const & | var, |
|
|
int | i ) |
|
inline |
Definition at line 3348 of file z3++.h.
3348 {
3349 set_initial_value(var, ctx().num_val(i, var.get_sort()));
3350 }
◆ statistics()
stats statistics |
( |
| ) |
const |
|
inline |
Definition at line 3394 of file z3++.h.
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.
◆ unsat_core()
Definition at line 3380 of file z3++.h.
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 ...
◆ upper()
Definition at line 3387 of file z3++.h.
3387 {
3389 check_error();
3390 return expr(ctx(), r);
3391 }
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.
◆ operator<<
std::ostream & operator<< |
( |
std::ostream & | out, |
|
|
optimize const & | s ) |
|
friend |
Definition at line 3400 of file z3++.h.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.