Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Data Structures | Public Member Functions | Friends
optimize Class Reference
+ Inheritance diagram for optimize:

Data Structures

class  handle
 

Public Member Functions

 optimize (context &c)
 
 optimize (optimize &o)
 
optimizeoperator= (optimize const &o)
 
 ~optimize ()
 
 operator Z3_optimize () const
 
void add (expr const &e)
 
handle add (expr const &e, unsigned weight)
 
void add (expr const &e, expr const &t)
 
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 ()
 
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 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
 
Z3_error_code 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 2755 of file z3++.h.

Constructor & Destructor Documentation

optimize ( context c)
inline

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

2765 :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:404
optimize ( optimize o)
inline

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

2766  :object(o) {
2767  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2768  m_opt = o.m_opt;
2769  }
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:404
~optimize ( )
inline

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

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

2779  {
2780  assert(e.is_bool());
2781  Z3_optimize_assert(ctx(), m_opt, e);
2782  }
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:406
handle add ( expr const &  e,
unsigned  weight 
)
inline

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

2783  {
2784  assert(e.is_bool());
2785  std::stringstream strm;
2786  strm << weight;
2787  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2788  }
context & ctx() const
Definition: z3++.h:406
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.
void add ( expr const &  e,
expr const &  t 
)
inline

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

2789  {
2790  assert(e.is_bool());
2791  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
2792  }
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
context & ctx() const
Definition: z3++.h:406
handle add ( expr const &  e,
char const *  weight 
)
inline

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

2794  {
2795  assert(e.is_bool());
2796  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2797  }
context & ctx() const
Definition: z3++.h:406
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.
expr_vector assertions ( ) const
inline

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

2835 { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
check_result check ( )
inline

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

2810 { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
Z3_error_code check_error() const
Definition: z3++.h:407
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
context & ctx() const
Definition: z3++.h:406
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:99
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:141
check_result check ( expr_vector const &  asms)
inline

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

2811  {
2812  unsigned n = asms.size();
2813  array<Z3_ast> _asms(n);
2814  for (unsigned i = 0; i < n; i++) {
2815  check_context(*this, asms[i]);
2816  _asms[i] = asms[i];
2817  }
2818  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
2819  check_error();
2820  return to_check_result(r);
2821  }
Z3_error_code check_error() const
Definition: z3++.h:407
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
context & ctx() const
Definition: z3++.h:406
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:99
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:141
void from_file ( char const *  filename)
inline

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

2839 { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
void from_string ( char const *  constraints)
inline

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

2840 { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
model get_model ( ) const
inline

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

2822 { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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 2841 of file z3++.h.

2841 { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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 2825 of file z3++.h.

2825  {
2826  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2827  check_error();
2828  return expr(ctx(), r);
2829  }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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'th optimization objective.
handle maximize ( expr const &  e)
inline

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

2798  {
2799  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2800  }
context & ctx() const
Definition: z3++.h:406
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 2801 of file z3++.h.

2801  {
2802  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2803  }
context & ctx() const
Definition: z3++.h:406
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
expr_vector objectives ( ) const
inline

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

2836 { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
operator Z3_optimize ( ) const
inline

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

2778 { return m_opt; }
optimize& operator= ( optimize const &  o)
inline

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

2770  {
2771  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2772  Z3_optimize_dec_ref(ctx(), m_opt);
2773  m_opt = o.m_opt;
2774  m_ctx = o.m_ctx;
2775  return *this;
2776  }
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
context & ctx() const
Definition: z3++.h:406
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
context * m_ctx
Definition: z3++.h:402
void pop ( )
inline

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

2807  {
2808  Z3_optimize_pop(ctx(), m_opt);
2809  }
context & ctx() const
Definition: z3++.h:406
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
void push ( )
inline

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

2804  {
2805  Z3_optimize_push(ctx(), m_opt);
2806  }
context & ctx() const
Definition: z3++.h:406
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 2824 of file z3++.h.

2824 { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
Z3_error_code check_error() const
Definition: z3++.h:407
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:406
stats statistics ( ) const
inline

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

2837 { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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_vector unsat_core ( ) const
inline

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

2823 { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
expr upper ( handle const &  h)
inline

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

2830  {
2831  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2832  check_error();
2833  return expr(ctx(), r);
2834  }
Z3_error_code check_error() const
Definition: z3++.h:407
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'th optimization objective.
context & ctx() const
Definition: z3++.h:406

Friends And Related Function Documentation

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

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

2843 { 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.