Z3
Data Structures | Public Member Functions | Friends
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)
 
contextctx () const
 
void 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 2005 of file z3++.h.

Constructor & Destructor Documentation

§ optimize()

optimize ( context c)
inline

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

2014 :object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
object(context &c)
Definition: z3++.h:330

§ ~optimize()

~optimize ( )
inline

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

2015 { Z3_optimize_dec_ref(ctx(), m_opt); }
context & ctx() const
Definition: z3++.h:332

Member Function Documentation

§ add() [1/3]

void add ( expr const &  e)
inline

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

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

2017  {
2018  assert(e.is_bool());
2019  Z3_optimize_assert(ctx(), m_opt, e);
2020  }
context & ctx() const
Definition: z3++.h:332

§ add() [2/3]

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

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

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

2021  {
2022  assert(e.is_bool());
2023  std::stringstream strm;
2024  strm << weight;
2025  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2026  }
context & ctx() const
Definition: z3++.h:332

§ add() [3/3]

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

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

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

2027  {
2028  assert(e.is_bool());
2029  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2030  }
context & ctx() const
Definition: z3++.h:332

§ assertions()

expr_vector assertions ( ) const
inline

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

Referenced by Solver::to_smt2().

2056 { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
void check_error() const
Definition: z3++.h:333

§ check()

check_result check ( )
inline

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

2043 { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
context & ctx() const
Definition: z3++.h:332
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
void check_error() const
Definition: z3++.h:333

§ from_file()

void from_file ( char const *  filename)
inline

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

2060 { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ from_string()

void from_string ( char const *  constraints)
inline

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

2061 { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ get_model()

model get_model ( ) const
inline

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

2044 { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ help()

std::string help ( ) const
inline

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

2062 { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ lower()

expr lower ( handle const &  h)
inline

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

Referenced by OptimizeObjective::value().

2046  {
2047  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2048  check_error();
2049  return expr(ctx(), r);
2050  }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ maximize()

handle maximize ( expr const &  e)
inline

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

2031  {
2032  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2033  }
context & ctx() const
Definition: z3++.h:332

§ minimize()

handle minimize ( expr const &  e)
inline

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

2034  {
2035  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2036  }
context & ctx() const
Definition: z3++.h:332

§ objectives()

expr_vector objectives ( ) const
inline

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

2057 { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
void check_error() const
Definition: z3++.h:333

§ operator Z3_optimize()

operator Z3_optimize ( ) const
inline

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

2016 { return m_opt; }

§ pop()

void pop ( )
inline

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

2040  {
2041  Z3_optimize_pop(ctx(), m_opt);
2042  }
context & ctx() const
Definition: z3++.h:332

§ push()

void push ( )
inline

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

2037  {
2038  Z3_optimize_push(ctx(), m_opt);
2039  }
context & ctx() const
Definition: z3++.h:332

§ set()

void set ( params const &  p)
inline

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

2045 { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ statistics()

stats statistics ( ) const
inline

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

2058 { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ upper()

expr upper ( handle const &  h)
inline

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

Referenced by OptimizeObjective::value().

2051  {
2052  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2053  check_error();
2054  return expr(ctx(), r);
2055  }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

Friends And Related Function Documentation

§ operator<<

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

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

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