Z3 |

Data Structures | Public Member Functions | Friends
optimize Class Reference

`#include <z3++.h>`

Inheritance diagram for optimize:

## Data Structures
class | handle

## Public Member Functions
| optimize (context &c)
| optimize (optimize const &o)
| optimize (context &c, optimize &src)
optimize & | operator= (optimize const &o)
| ~optimize ()
| operator Z3_optimize () const
void | add (expr const &e)
void | add (expr_vector const &es)
void | add (expr const &e, expr const &t)
void | add (expr const &e, char const *p)
handle | add_soft (expr const &e, unsigned weight)
handle | add_soft (expr const &e, char const *weight)
handle | add (expr const &e, unsigned weight)
handle | maximize (expr const &e)
handle | minimize (expr const &e)
void | push ()
void | pop ()
check_result | check ()
check_result | check (expr_vector const &asms)
model | get_model () const
expr_vector | unsat_core () const
void | set (params const &p)
expr | lower (handle const &h)
expr | upper (handle const &h)
expr_vector | assertions () const
expr_vector | objectives () const
stats | statistics () const
void | from_file (char const *filename)
void | from_string (char const *constraints)
std::string | help () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Friends
std::ostream & | operator<< (std::ostream &out, optimize const &s)

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

Definition at line 3014 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ optimize() [1/3]

optimize | ( | context & | c | ) |
| inline

Definition at line 3024 of file z3++.h.

3024:object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_optimize_inc_ref
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_mk_optimize
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.

Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().

## ◆ optimize() [2/3]

optimize | ( | optimize const & | o | ) |
| inline

Definition at line 3025 of file z3++.h.

3025 :object(o), m_opt(o.m_opt) {
3026 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3027 }

Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().

## ◆ optimize() [3/3]

optimize | ( | context & | c,
|  | optimize & | src
| ) |  |
| inline

Definition at line 3028 of file z3++.h.

3028 :object(c) {
3029 m_opt = Z3_mk_optimize(c);
3030 Z3_optimize_inc_ref(c, m_opt);
3031 add(expr_vector(c, src.assertions()));
3032 expr_vector v(c, src.objectives());
3033 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3034 }
z3::optimize::add
void add(expr const &e)
Definition: z3++.h:3044
z3::optimize::minimize
handle minimize(expr const &e)
Definition: z3++.h:3074
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73

Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().

## ◆ ~optimize()

~optimize | ( |  | ) |
| inline

Definition at line 3042 of file z3++.h.

3042{ Z3_optimize_dec_ref(ctx(), m_opt); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_optimize_dec_ref
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.

## Member Function Documentation

## ◆ add() [1/5]

void add | ( | expr const & | e | ) |
| inline

Definition at line 3044 of file z3++.h.

3044 {
3045 assert(e.is_bool());
3046 Z3_optimize_assert(ctx(), m_opt, e);
3047 }
Z3_optimize_assert
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), Optimize::__iadd__(), optimize::add(), and optimize::optimize().

## ◆ add() [2/5]

void add | ( | expr const & | e,
|  | char const * | p
| ) |  |
| inline

Definition at line 3055 of file z3++.h.

3055 {
3056 assert(e.is_bool());
3057 add(e, ctx().bool_const(p));
3058 }

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ add() [3/5]

void add | ( | expr const & | e,
|  | expr const & | t
| ) |  |
| inline

Definition at line 3051 of file z3++.h.

3051 {
3052 assert(e.is_bool());
3053 Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3054 }
Z3_optimize_assert_and_track
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 Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ add() [4/5]

handle add | ( | expr const & | e,
|  | unsigned | weight
| ) |  |
| inline

Definition at line 3068 of file z3++.h.

3068 {
3069 return add_soft(e, weight);
3070 }
z3::optimize::add_soft
handle add_soft(expr const &e, unsigned weight)
Definition: z3++.h:3059

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ add() [5/5]

void add | ( | expr_vector const & | es | ) |
| inline

Definition at line 3048 of file z3++.h.

3048 {
3049 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3050 }

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ add_soft() [1/2]

handle add_soft | ( | expr const & | e,
|  | char const * | weight
| ) |  |
| inline

Definition at line 3064 of file z3++.h.

3064 {
3065 assert(e.is_bool());
3066 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
3067 }
Z3_optimize_assert_soft
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 3059 of file z3++.h.

3059 {
3060 assert(e.is_bool());
3061 auto str = std::to_string(weight);
3062 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3063 }

Referenced by optimize::add().

## ◆ assertions()

expr_vector assertions | ( |  | ) | const
| inline

Definition at line 3108 of file z3++.h.

3108{ Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_optimize_get_assertions
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::optimize(), and Solver::to_smt2().

## ◆ check() [1/2]

check_result check | ( |  | ) |
| inline

Definition at line 3083 of file z3++.h.

3083{ Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
z3::to_check_result
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:144
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_optimize_check
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() [2/2]

check_result check | ( | expr_vector const & | asms | ) |
| inline

Definition at line 3084 of file z3++.h.

3084 {
3085 unsigned n = asms.size();
3086 array<Z3_ast> _asms(n);
3087 for (unsigned i = 0; i < n; i++) {
3088 check_context(*this, asms[i]);
3089 _asms[i] = asms[i];
3090 }
3091 Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3092 check_error();
3093 return to_check_result(r);
3094 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426

## ◆ from_file()

void from_file | ( | char const * | filename | ) |
| inline

Definition at line 3112 of file z3++.h.

3112{ Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
Z3_optimize_from_file
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 3113 of file z3++.h.

3113{ Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
Z3_optimize_from_string
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 3095 of file z3++.h.

3095{ Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
Z3_optimize_get_model
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 3114 of file z3++.h.

3114{ char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
Z3_optimize_get_help
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()

expr lower | ( | handle const & | h | ) |
| inline

Definition at line 3098 of file z3++.h.

3098 {
3099 Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3100 check_error();
3101 return expr(ctx(), r);
3102 }
Z3_optimize_get_lower
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.

Referenced by OptimizeObjective::value().

## ◆ maximize()

handle maximize | ( | expr const & | e | ) |
| inline

Definition at line 3071 of file z3++.h.

3071 {
3072 return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3073 }
Z3_optimize_maximize
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.

## ◆ minimize()

handle minimize | ( | expr const & | e | ) |
| inline

Definition at line 3074 of file z3++.h.

3074 {
3075 return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3076 }
Z3_optimize_minimize
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.

Referenced by optimize::optimize().

## ◆ objectives()

expr_vector objectives | ( |  | ) | const
| inline

Definition at line 3109 of file z3++.h.

3109{ Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_optimize_get_objectives
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::optimize().

## ◆ operator Z3_optimize()

operator Z3_optimize | ( |  | ) | const
| inline

Definition at line 3043 of file z3++.h.

3043{ return m_opt; }

## ◆ operator=()

optimize & operator= | ( | optimize const & | o | ) |
| inline

Definition at line 3035 of file z3++.h.

3035 {
3036 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3037 Z3_optimize_dec_ref(ctx(), m_opt);
3038 m_opt = o.m_opt;
3039 object::operator=(o);
3040 return *this;
3041 }

## ◆ pop()

void pop | ( |  | ) |
| inline

Definition at line 3080 of file z3++.h.

3080 {
3081 Z3_optimize_pop(ctx(), m_opt);
3082 }
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.

## ◆ push()

void push | ( |  | ) |
| inline

Definition at line 3077 of file z3++.h.

3077 {
3078 Z3_optimize_push(ctx(), m_opt);
3079 }
Z3_optimize_push
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.

## ◆ set()

void set | ( | params const & | p | ) |
| inline

Definition at line 3097 of file z3++.h.

3097{ Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
Z3_optimize_set_params
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

## ◆ statistics()

stats statistics | ( |  | ) | const
| inline

Definition at line 3110 of file z3++.h.

3110{ Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
Z3_optimize_get_statistics
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()

expr_vector unsat_core | ( |  | ) | const
| inline

Definition at line 3096 of file z3++.h.

3096{ Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_optimize_get_unsat_core
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()

expr upper | ( | handle const & | h | ) |
| inline

Definition at line 3103 of file z3++.h.

3103 {
3104 Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3105 check_error();
3106 return expr(ctx(), r);
3107 }
Z3_optimize_get_upper
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.

Referenced by OptimizeObjective::value().

## Friends And Related Function Documentation

## ◆ operator<<

std::ostream & operator<< | ( | std::ostream & | out,
|  | optimize const & | s
| ) |  |
| friend

Definition at line 3116 of file z3++.h.

3116{ out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.