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)
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)
	object (object const &s)
context &	ctx () const
void	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 2005 of file z3++.h.

Constructor & Destructor Documentation

optimize()

optimize ( context &  c )

inline

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

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

~optimize()

~optimize ( )

inline

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

{ Z3_optimize_dec_ref(ctx(), m_opt); }

Member Function Documentation

add() [1/3]

void add ( expr const &  e )

inline

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

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

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

add() [2/3]

handle add ( expr const &  e, unsigned  weight  )

inline

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

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

add() [3/3]

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

inline

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

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

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

assertions()

expr_vector assertions ( ) const

inline

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

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

Referenced by Solver::to_smt2().

check()

check_result check ( )

inline

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

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

from_file()

void from_file ( char const *  filename )

inline

Definition at line 2060 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 2061 of file z3++.h.

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

get_model()

model get_model ( ) const

inline

Definition at line 2044 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 2062 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 2046 of file z3++.h.

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

Referenced by OptimizeObjective::value().

maximize()

handle maximize ( expr const &  e )

inline

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

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

minimize()

handle minimize ( expr const &  e )

inline

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

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

objectives()

expr_vector objectives ( ) const

inline

Definition at line 2057 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 2016 of file z3++.h.

{ return m_opt; }

pop()

void pop ( )

inline

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

                   {
            Z3_optimize_pop(ctx(), m_opt);
        }

push()

void push ( )

inline

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

                    {
            Z3_optimize_push(ctx(), m_opt);
        }

set()

void set ( params const &  p )

inline

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

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

statistics()

stats statistics ( ) const

inline

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

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

upper()

expr upper ( handle const &  h )

inline

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

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

Referenced by OptimizeObjective::value().

Friends And Related Function Documentation

operator<<

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

friend

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

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