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)
 
stats statistics () const
 
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 1552 of file z3++.h.

Constructor & Destructor Documentation

optimize ( context c)
inline

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

1561 :object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
object(context &c)
Definition: z3++.h:275
~optimize ( )
inline

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

1562 { Z3_optimize_dec_ref(ctx(), m_opt); }
context & ctx() const
Definition: z3++.h:277
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 1564 of file z3++.h.

1564  {
1565  assert(e.is_bool());
1566  Z3_optimize_assert(ctx(), m_opt, e);
1567  }
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
context & ctx() const
Definition: z3++.h:277
handle add ( expr const &  e,
unsigned  weight 
)
inline

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

1568  {
1569  assert(e.is_bool());
1570  std::stringstream strm;
1571  strm << weight;
1572  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
1573  }
context & ctx() const
Definition: z3++.h:277
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
handle add ( expr const &  e,
char const *  weight 
)
inline

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

1574  {
1575  assert(e.is_bool());
1576  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
1577  }
context & ctx() const
Definition: z3++.h:277
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
check_result check ( )
inline

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

1590 { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.
context & ctx() const
Definition: z3++.h:277
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
void check_error() const
Definition: z3++.h:278
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1265
model get_model ( ) const
inline

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

1591 { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
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 1605 of file z3++.h.

1605 { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
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 1593 of file z3++.h.

Referenced by OptimizeObjective::value().

1593  {
1594  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
1595  check_error();
1596  return expr(ctx(), r);
1597  }
context & ctx() const
Definition: z3++.h:277
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i&#39;th optimization objective.
void check_error() const
Definition: z3++.h:278
handle maximize ( expr const &  e)
inline

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

1578  {
1579  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
1580  }
context & ctx() const
Definition: z3++.h:277
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
handle minimize ( expr const &  e)
inline

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

1581  {
1582  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
1583  }
context & ctx() const
Definition: z3++.h:277
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
operator Z3_optimize ( ) const
inline

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

1563 { return m_opt; }
void pop ( )
inline

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

1587  {
1588  Z3_optimize_pop(ctx(), m_opt);
1589  }
context & ctx() const
Definition: z3++.h:277
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
void push ( )
inline

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

1584  {
1585  Z3_optimize_push(ctx(), m_opt);
1586  }
context & ctx() const
Definition: z3++.h:277
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
void set ( params const &  p)
inline

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

1592 { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
stats statistics ( ) const
inline

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

1603 { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
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 upper ( handle const &  h)
inline

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

Referenced by OptimizeObjective::value().

1598  {
1599  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
1600  check_error();
1601  return expr(ctx(), r);
1602  }
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i&#39;th optimization objective.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278

Friends And Related Function Documentation

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

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

1604 { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.