optimize Class Reference

#include <z3++.h>

Inheritance diagram for optimize:

Data Structures
class	handle
struct	translate

Public Member Functions
	optimize (context &c)
	optimize (context &c, optimize const &src, translate)
	optimize (optimize const &o)
	optimize (context &c, optimize &src)
optimize &	operator= (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_vector	lower_as_vector (handle const &h) const
expr	upper (handle const &h)
expr_vector	upper_as_vector (handle const &h) const
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
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 3623 of file z3++.h.

Constructor & Destructor Documentation

optimize() [1/4]

optimize ( context &  c )

inline

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

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

optimize() [2/4]

optimize ( context &  c, optimize const &  src, translate    )

inline

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

                                                             : object(c) { 
            Z3_optimize o = Z3_optimize_translate(src.ctx(), src, c); 
            check_error(); 
            m_opt = o; 
            Z3_optimize_inc_ref(c, m_opt); 
        }

optimize() [3/4]

optimize ( optimize const &  o )

inline

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

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

optimize() [4/4]

optimize ( context &  c, optimize &  src  )

inline

Definition at line 3644 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()

~optimize ( )

inlineoverride

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

{ Z3_optimize_dec_ref(ctx(), m_opt); }

Member Function Documentation

add() [1/5]

void add ( expr const &  e )

inline

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

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

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

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

Referenced by Solver::__iadd__().

add() [3/5]

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

inline

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

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

Referenced by Solver::__iadd__().

add() [4/5]

handle add ( expr const &  e, unsigned  weight  )

inline

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

                                                   {
            return add_soft(e, weight);
        }

Referenced by Solver::__iadd__().

add() [5/5]

void add ( expr_vector const &  es )

inline

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

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

Referenced by Solver::__iadd__().

add_soft() [1/2]

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

inline

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

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

add_soft() [2/2]

handle add_soft ( expr const &  e, unsigned  weight  )

inline

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

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

Referenced by optimize::add().

assertions()

expr_vector assertions ( ) const

inline

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

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

check() [1/2]

check_result check ( )

inline

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

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

check() [2/2]

check_result check ( expr_vector const &  asms )

inline

Definition at line 3711 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);
        }

from_file()

void from_file ( char const *  filename )

inline

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

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

from_string()

void from_string ( char const *  constraints )

inline

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

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

get_model()

model get_model ( ) const

inline

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

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

help()

std::string help ( ) const

inline

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

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

lower()

expr lower ( handle const &  h )

inline

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

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

lower_as_vector()

expr_vector lower_as_vector ( handle const &  h ) const

inline

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

                                                           {
            Z3_ast_vector r = Z3_optimize_get_lower_as_vector(ctx(), m_opt, h.h());
            check_error();
            return expr_vector(ctx(), r);
        }

maximize()

handle maximize ( expr const &  e )

inline

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

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

minimize()

handle minimize ( expr const &  e )

inline

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

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

Referenced by optimize::optimize().

objectives()

expr_vector objectives ( ) const

inline

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

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

operator Z3_optimize()

operator Z3_optimize ( ) const

inline

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

{ return m_opt; }

operator=()

optimize & operator= ( optimize const &  o )

inline

Definition at line 3651 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;
        }

pop()

void pop ( )

inline

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

                   {
            Z3_optimize_pop(ctx(), m_opt);
        }

Referenced by Solver::__exit__().

push()

void push ( )

inline

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

                    {
            Z3_optimize_push(ctx(), m_opt);
        }

Referenced by Solver::__enter__().

set()

void set ( params const &  p )

inline

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

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

set_initial_value() [1/3]

void set_initial_value ( expr const &  var, bool  b  )

inline

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

                                                        {
            set_initial_value(var, ctx().bool_val(b));            
        }

set_initial_value() [2/3]

void set_initial_value ( expr const &  var, expr const &  value  )

inline

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

                                                                   {
            Z3_optimize_set_initial_value(ctx(), m_opt, var, value);
            check_error();
        }

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

                                                       {
            set_initial_value(var, ctx().num_val(i, var.get_sort()));
        }

statistics()

stats statistics ( ) const

inline

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

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

unsat_core()

expr_vector unsat_core ( ) const

inline

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

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

upper()

expr upper ( handle const &  h )

inline

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

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

upper_as_vector()

expr_vector upper_as_vector ( handle const &  h ) const

inline

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

                                                           {
            Z3_ast_vector r = Z3_optimize_get_upper_as_vector(ctx(), m_opt, h.h());
            check_error();
            return expr_vector(ctx(), r);
        }

Friends And Related Symbol Documentation

operator<<

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

friend

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

{ out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }