Z3
 
Loading...
Searching...
No Matches
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)
 
optimizeoperator= (optimize const &o)
 
 ~optimize () override
 
 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)
 
void set_initial_value (expr const &var, expr const &value)
 
void set_initial_value (expr const &var, int i)
 
void set_initial_value (expr const &var, bool b)
 
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)
 
virtual ~object ()=default
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ optimize() [1/3]

optimize ( context & c)
inline

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

3297:object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
object(context &c)
Definition z3++.h:472
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.

◆ optimize() [2/3]

optimize ( optimize const & o)
inline

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

3298 :object(o), m_opt(o.m_opt) {
3299 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3300 }

◆ optimize() [3/3]

optimize ( context & c,
optimize & src )
inline

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

3301 :object(c) {
3302 m_opt = Z3_mk_optimize(c);
3303 Z3_optimize_inc_ref(c, m_opt);
3304 add(expr_vector(c, src.assertions()));
3305 expr_vector v(c, src.objectives());
3306 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3307 }
void add(expr const &e)
Definition z3++.h:3317
handle minimize(expr const &e)
Definition z3++.h:3358
ast_vector_tpl< expr > expr_vector
Definition z3++.h:76

◆ ~optimize()

~optimize ( )
inlineoverride

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

3315{ Z3_optimize_dec_ref(ctx(), m_opt); }
context & ctx() const
Definition z3++.h:474
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 3317 of file z3++.h.

3317 {
3318 assert(e.is_bool());
3319 Z3_optimize_assert(ctx(), m_opt, e);
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 Solver::__iadd__(), optimize::add(), optimize::add(), and optimize::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 }

Referenced by Solver::__iadd__().

◆ 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());
3326 Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
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.

Referenced by Solver::__iadd__().

◆ add() [4/5]

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

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

3341 {
3342 return add_soft(e, weight);
3343 }
handle add_soft(expr const &e, unsigned weight)
Definition z3++.h:3332

Referenced by Solver::__iadd__().

◆ add() [5/5]

void add ( expr_vector const & es)
inline

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

3321 {
3322 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3323 }

Referenced by Solver::__iadd__().

◆ 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());
3339 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
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);
3335 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3336 }

Referenced by optimize::add().

◆ assertions()

expr_vector assertions ( ) const
inline

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

3392{ Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_error_code check_error() const
Definition z3++.h:475
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().

◆ check() [1/2]

check_result check ( )
inline

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

3367{ Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition z3_api.h:61
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)
Definition z3++.h:147

◆ check() [2/2]

check_result check ( expr_vector const & asms)
inline

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++) {
3372 check_context(*this, asms[i]);
3373 _asms[i] = asms[i];
3374 }
3375 Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3376 check_error();
3377 return to_check_result(r);
3378 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478

◆ from_file()

void from_file ( char const * filename)
inline

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

3396{ Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
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.

3397{ Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
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.

3379{ Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
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.

3398{ char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
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 3382 of file z3++.h.

3382 {
3383 Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
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()

handle maximize ( expr const & e)
inline

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

3355 {
3356 return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3357 }
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 3358 of file z3++.h.

3358 {
3359 return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3360 }
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 3393 of file z3++.h.

3393{ Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
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 3316 of file z3++.h.

3316{ return m_opt; }

◆ operator=()

optimize & operator= ( optimize const & o)
inline

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

3308 {
3309 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3310 Z3_optimize_dec_ref(ctx(), m_opt);
3311 m_opt = o.m_opt;
3312 object::operator=(o);
3313 return *this;
3314 }

◆ pop()

void pop ( )
inline

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

3364 {
3365 Z3_optimize_pop(ctx(), m_opt);
3366 }
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.

Referenced by Solver::__exit__().

◆ push()

void push ( )
inline

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

3361 {
3362 Z3_optimize_push(ctx(), m_opt);
3363 }
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.

Referenced by Solver::__enter__().

◆ set()

void set ( params const & p)
inline

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

3381{ Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
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 }
void set_initial_value(expr const &var, expr const &value)
Definition z3++.h:3344

◆ 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 {
3345 Z3_optimize_set_initial_value(ctx(), m_opt, var, value);
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 optimize::set_initial_value(), and optimize::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.

3394{ Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
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 3380 of file z3++.h.

3380{ Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
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 3387 of file z3++.h.

3387 {
3388 Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
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.

Friends And Related Symbol Documentation

◆ operator<<

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

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

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