optimize Class Reference

Inheritance diagram for optimize:

Data Structures
class	handle
Public Member Functions
	optimize (context &c)
	~optimize ()
	operator Z3_optimize () const
void	add (expr const &e)
handle	add (expr const &e, unsigned weight)
handle	add (expr const &e, char const *weight)
handle	maximize (expr const &e)
handle	minimize (expr const &e)
void	push ()
void	pop ()
check_result	check ()
model	get_model () const
void	set (params const &p)
expr	lower (handle const &h)
expr	upper (handle const &h)
stats	statistics () const
std::string	help () const
Friends
std::ostream &	operator<< (std::ostream &out, optimize const &s)

---

Detailed Description

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

---

Constructor & Destructor Documentation

optimize

(

context &

c

)

[inline]

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

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

~optimize

(

)

[inline]

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

{ Z3_optimize_dec_ref(ctx(), m_opt); }

---

Member Function Documentation

void add

(

expr const &

e

)

[inline]

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

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

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

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

                                                   {
            assert(e.is_bool());
            std::stringstream strm;
            strm << weight; 
            return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0)); 
        }

handle add	(	expr const &	e,
		char const *	weight
	)		[inline]

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

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

check_result check

(

)

[inline]

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

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

model get_model

(

)

const [inline]

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

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

std::string help

(

)

const [inline]

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

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

expr lower

(

handle const &

h

)

[inline]

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

Referenced by OptimizeObjective::value().

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

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

handle minimize

(

expr const &

e

)

[inline]

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

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

operator Z3_optimize

(

)

const [inline]

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

{ return m_opt; }

void pop

(

)

[inline]

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

                   {
            Z3_optimize_pop(ctx(), m_opt);
        }

void push

(

)

[inline]

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

                    {
            Z3_optimize_push(ctx(), m_opt);
        }

void set

(

params const &

p

)

[inline]

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

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

stats statistics

(

)

const [inline]

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

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

expr upper

(

handle const &

h

)

[inline]

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

Referenced by OptimizeObjective::value().

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

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