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 3081 of file z3++.h.

Constructor & Destructor Documentation

optimize ( context & c )

inline

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

3091 :object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }

Z3_mk_optimize

Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)

Create a new optimize context.

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::object::object

object(context &c)

Definition: z3++.h:427

optimize ( optimize const & o )

inline

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

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

optimize	(	context &	c,
		optimize &	src
	)

inline

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

                                            :object(c) {
             m_opt = Z3_mk_optimize(c); 
             Z3_optimize_inc_ref(c, m_opt);
             add(expr_vector(c, src.assertions()));
             expr_vector v(c, src.objectives());
             for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
         }

~optimize ( )

inline

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

3109 { Z3_optimize_dec_ref(ctx(), m_opt); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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

void add ( expr const & e )

inline

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

Referenced by optimize::add(), and optimize::optimize().

                                 {
             assert(e.is_bool());
             Z3_optimize_assert(ctx(), m_opt, e);
         }

void add ( expr_vector const & es )

inline

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

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

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

inline

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

                                                {
             assert(e.is_bool());
             Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
         }

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

inline

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

                                                {
             assert(e.is_bool());
             add(e, ctx().bool_const(p));
         }

handle add	(	expr const &	e,
		unsigned	weight
	)

inline

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

                                                    {
             return add_soft(e, weight);
         }

handle add_soft	(	expr const &	e,
		unsigned	weight
	)

inline

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

Referenced by optimize::add().

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

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

inline

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

                                                            {
             assert(e.is_bool());
             return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
         }

expr_vector assertions ( ) const

inline

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

Referenced by optimize::optimize().

3175 { 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:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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.

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

check_result check ( )

inline

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

3150 { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

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.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_lbool

Lifted Boolean type: false, undefined, true.

Definition: z3_api.h:101

z3::to_check_result

check_result to_check_result(Z3_lbool l)

Definition: z3++.h:144

check_result check ( expr_vector const & asms )

inline

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

                                                     {
             unsigned n = asms.size();
             array<Z3_ast> _asms(n);
             for (unsigned i = 0; i < n; i++) {
                 check_context(*this, asms[i]);
                 _asms[i] = asms[i];
             }
             Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
             check_error();
             return to_check_result(r);
         }

void from_file ( char const * filename )

inline

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

3179 { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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. Add the parsed constraints and objectives to the optimization context.

void from_string ( char const * constraints )

inline

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

3180 { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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. Add the parsed constraints and objectives to the optimization context.

model get_model ( ) const

inline

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

3162 { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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.

std::string help ( ) const

inline

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

3181 { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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.

expr lower ( handle const & h )

inline

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

                                     {
             Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
             check_error();
             return expr(ctx(), r);
         }

handle maximize ( expr const & e )

inline

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

                                        {
             return handle(Z3_optimize_maximize(ctx(), m_opt, e));
         }

handle minimize ( expr const & e )

inline

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

Referenced by optimize::optimize().

                                        {
             return handle(Z3_optimize_minimize(ctx(), m_opt, e));
         }

expr_vector objectives ( ) const

inline

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

Referenced by optimize::optimize().

3176 { 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...

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

operator Z3_optimize ( ) const

inline

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

3110 { return m_opt; }

optimize& operator= ( optimize const & o )

inline

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

                                                {
             Z3_optimize_inc_ref(o.ctx(), o.m_opt);
             Z3_optimize_dec_ref(ctx(), m_opt);
             m_opt = o.m_opt;
             object::operator=(o);
             return *this;
         }

void pop ( )

inline

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

                    {
             Z3_optimize_pop(ctx(), m_opt);
         }

void push ( )

inline

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

                     {
             Z3_optimize_push(ctx(), m_opt);
         }

void set ( params const & p )

inline

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

3164 { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

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.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

stats statistics ( ) const

inline

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

3177 { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

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.

expr_vector unsat_core ( ) const

inline

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

3163 { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

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 ...

expr upper ( handle const & h )

inline

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

                                     {
             Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
             check_error();
             return expr(ctx(), r);
         }

Friends And Related Function Documentation

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

friend

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

3183 { 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.

Data Structures

Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation