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 (optimize const &o)
 
 optimize (context &c, optimize &src)
 
optimizeoperator= (optimize const &o)
 
 ~optimize ()
 
 operator Z3_optimize () const
 
void add (expr const &e)
 
void add (expr_vector const &es)
 
void add (expr const &e, expr const &t)
 
void add (expr const &e, char const *p)
 
handle add_soft (expr const &e, unsigned weight)
 
handle add_soft (expr const &e, char const *weight)
 
handle add (expr const &e, unsigned 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)
 
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 3126 of file z3++.h.

Constructor & Destructor Documentation

◆ optimize() [1/3]

optimize ( context c)
inline

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

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

◆ optimize() [2/3]

optimize ( optimize const &  o)
inline

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

3137  :object(o), m_opt(o.m_opt) {
3138  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3139  }

◆ optimize() [3/3]

optimize ( context c,
optimize src 
)
inline

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

3140  :object(c) {
3141  m_opt = Z3_mk_optimize(c);
3142  Z3_optimize_inc_ref(c, m_opt);
3143  add(expr_vector(c, src.assertions()));
3144  expr_vector v(c, src.objectives());
3145  for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3146  }

◆ ~optimize()

~optimize ( )
inline

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

3154 { Z3_optimize_dec_ref(ctx(), m_opt); }

Member Function Documentation

◆ add() [1/5]

void add ( expr const &  e)
inline

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

3156  {
3157  assert(e.is_bool());
3158  Z3_optimize_assert(ctx(), m_opt, e);
3159  }

Referenced by optimize::add(), and optimize::optimize().

◆ add() [2/5]

void add ( expr const &  e,
char const *  p 
)
inline

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

3167  {
3168  assert(e.is_bool());
3169  add(e, ctx().bool_const(p));
3170  }

◆ add() [3/5]

void add ( expr const &  e,
expr const &  t 
)
inline

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

3163  {
3164  assert(e.is_bool());
3165  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3166  }

◆ add() [4/5]

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

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

3180  {
3181  return add_soft(e, weight);
3182  }

◆ add() [5/5]

void add ( expr_vector const &  es)
inline

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

3160  {
3161  for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3162  }

◆ add_soft() [1/2]

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

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

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

◆ add_soft() [2/2]

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

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

3171  {
3172  assert(e.is_bool());
3173  auto str = std::to_string(weight);
3174  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3175  }

Referenced by optimize::add().

◆ assertions()

expr_vector assertions ( ) const
inline

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

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

Referenced by optimize::optimize().

◆ check() [1/2]

check_result check ( )
inline

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

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

◆ check() [2/2]

check_result check ( expr_vector const &  asms)
inline

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

3196  {
3197  unsigned n = asms.size();
3198  array<Z3_ast> _asms(n);
3199  for (unsigned i = 0; i < n; i++) {
3200  check_context(*this, asms[i]);
3201  _asms[i] = asms[i];
3202  }
3203  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3204  check_error();
3205  return to_check_result(r);
3206  }

◆ from_file()

void from_file ( char const *  filename)
inline

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

3224 { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }

◆ from_string()

void from_string ( char const *  constraints)
inline

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

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

◆ get_model()

model get_model ( ) const
inline

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

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

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

◆ lower()

expr lower ( handle const &  h)
inline

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

3210  {
3211  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3212  check_error();
3213  return expr(ctx(), r);
3214  }

◆ maximize()

handle maximize ( expr const &  e)
inline

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

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

◆ minimize()

handle minimize ( expr const &  e)
inline

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

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

Referenced by optimize::optimize().

◆ objectives()

expr_vector objectives ( ) const
inline

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

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

Referenced by optimize::optimize().

◆ operator Z3_optimize()

operator Z3_optimize ( ) const
inline

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

3155 { return m_opt; }

◆ operator=()

optimize& operator= ( optimize const &  o)
inline

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

3147  {
3148  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3149  Z3_optimize_dec_ref(ctx(), m_opt);
3150  m_opt = o.m_opt;
3151  object::operator=(o);
3152  return *this;
3153  }

◆ pop()

void pop ( )
inline

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

3192  {
3193  Z3_optimize_pop(ctx(), m_opt);
3194  }

◆ push()

void push ( )
inline

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

3189  {
3190  Z3_optimize_push(ctx(), m_opt);
3191  }

◆ set()

void set ( params const &  p)
inline

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

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

◆ statistics()

stats statistics ( ) const
inline

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

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

◆ unsat_core()

expr_vector unsat_core ( ) const
inline

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

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

◆ upper()

expr upper ( handle const &  h)
inline

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

3215  {
3216  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3217  check_error();
3218  return expr(ctx(), r);
3219  }

Friends And Related Function Documentation

◆ operator<<

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

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

3228 { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
Z3_optimize_get_objectives
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...
Microsoft.Z3.Z3_stats
System.IntPtr Z3_stats
Definition: NativeContext.cs:34
Z3_optimize_get_unsat_core
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 ...
Z3_optimize_maximize
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_optimize_check
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.
Z3_optimize_assert
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Z3_optimize_minimize
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_optimize_inc_ref
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Microsoft.Z3.Z3_model
System.IntPtr Z3_model
Definition: NativeFuncInterp.cs:31
Z3_optimize_get_assertions
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.
Z3_optimize_push
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_optimize_assert_and_track
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.
z3::object::object
object(context &c)
Definition: z3++.h:450
Z3_optimize_dec_ref
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_optimize_get_lower
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.
Microsoft.Z3.Z3_ast_vector
System.IntPtr Z3_ast_vector
Definition: NativeContext.cs:29
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:59
Z3_optimize_assert_soft
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.
Z3_optimize_get_statistics
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.
Z3_optimize_set_params
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
z3::optimize::add
void add(expr const &e)
Definition: z3++.h:3156
Z3_optimize_get_upper
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.
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:75
Z3_mk_optimize
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:455
z3::to_check_result
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:146
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
Z3_optimize_get_help
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.
z3::optimize::minimize
handle minimize(expr const &e)
Definition: z3++.h:3186
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:452
Z3_optimize_get_model
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
z3::optimize::add_soft
handle add_soft(expr const &e, unsigned weight)
Definition: z3++.h:3171
Z3_optimize_from_file
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....
z3::object::ctx
context & ctx() const
Definition: z3++.h:451
Z3_optimize_from_string
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....