Z3 |

Typedefs
z3_optimization.h File Reference

Go to the source code of this file.

## Typedefs
typedef void | Z3_model_eh(void *ctx)
| callback functions for models. More...

## Functions
Optimization facilities
Z3_optimize Z3_API | Z3_mk_optimize (Z3_context c)
| Create a new optimize context. More...
void Z3_API | Z3_optimize_inc_ref (Z3_context c, Z3_optimize d)
| Increment the reference counter of the given optimize context. More...
void Z3_API | Z3_optimize_dec_ref (Z3_context c, Z3_optimize d)
| Decrement the reference counter of the given optimize context. More...
void Z3_API | Z3_optimize_assert (Z3_context c, Z3_optimize o, Z3_ast a)
| Assert hard constraint to the optimization context. More...
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. More...
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. More...
unsigned Z3_API | Z3_optimize_maximize (Z3_context c, Z3_optimize o, Z3_ast t)
| Add a maximization constraint. More...
unsigned Z3_API | Z3_optimize_minimize (Z3_context c, Z3_optimize o, Z3_ast t)
| Add a minimization constraint. More...
void Z3_API | Z3_optimize_push (Z3_context c, Z3_optimize d)
| Create a backtracking point. More...
void Z3_API | Z3_optimize_pop (Z3_context c, Z3_optimize d)
| Backtrack one level. More...
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. More...
Z3_string Z3_API | Z3_optimize_get_reason_unknown (Z3_context c, Z3_optimize d)
| Retrieve a string that describes the last status returned by Z3_optimize_check. More...
Z3_model Z3_API | Z3_optimize_get_model (Z3_context c, Z3_optimize o)
| Retrieve the model for the last Z3_optimize_check. More...
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 `a`. More...
void Z3_API | Z3_optimize_set_params (Z3_context c, Z3_optimize o, Z3_params p)
| Set parameters on optimization context. More...
Z3_param_descrs Z3_API | Z3_optimize_get_param_descrs (Z3_context c, Z3_optimize o)
| Return the parameter description set for the given optimize object. More...
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. More...
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. More...
Z3_ast_vector Z3_API | Z3_optimize_get_lower_as_vector (Z3_context c, Z3_optimize o, unsigned idx)
| Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients `a`, `b`, `c` and encode the result of Z3_optimize_get_lower `a * infinity + b + c * epsilon`. More...
Z3_ast_vector Z3_API | Z3_optimize_get_upper_as_vector (Z3_context c, Z3_optimize o, unsigned idx)
| Retrieve upper bound value or approximation for the i'th optimization objective. More...
Z3_string Z3_API | Z3_optimize_to_string (Z3_context c, Z3_optimize o)
| Print the current context as a string. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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 returned as a Pseudo-Boolean (minimization) sum of the form `(+ (if f1 w1 0) (if f2 w2 0) ...)` If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective. More...
void Z3_API | Z3_optimize_register_model_eh (Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)
| register a model event handler for new models. More...

## Typedef Documentation

## ◆ Z3_model_eh

typedef void Z3_model_eh(void *ctx)

callback functions for models.

Definition at line 24 of file z3_optimization.h.

## Function Documentation

## ◆ Z3_mk_optimize()

Z3_optimize Z3_API Z3_mk_optimize | ( | Z3_context | c | ) |

Create a new optimize context.

Remarks
  User must use Z3_optimize_inc_ref and Z3_optimize_dec_ref to manage optimize objects. Even if the context was created using Z3_mk_context instead of Z3_mk_context_rc.

Referenced by optimize::optimize().

## ◆ 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.

See also
  Z3_optimize_assert_soft
  Z3_optimize_assert_and_track

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

## ◆ 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.

See also
  Z3_optimize_assert
  Z3_optimize_assert_soft

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

## ◆ 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.

Parameters

  c | - context
  o | - optimization context
  a | - formula
  weight | - a positive weight, penalty for violating soft constraint
  id | - optional identifier to group soft constraints

See also
  Z3_optimize_assert
  Z3_optimize_assert_and_track

Referenced by optimize::add_soft(), and Optimize::add_soft().

## ◆ 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.

Parameters

  c | - context
  o | - optimization context
  num_assumptions | - number of additional assumptions
  assumptions | - the additional assumptions

See also
  Z3_optimize_get_reason_unknown
  Z3_optimize_get_model
  Z3_optimize_get_statistics
  Z3_optimize_get_unsat_core

Referenced by optimize::check(), and Optimize::check().

## ◆ 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.

Referenced by Optimize::__del__(), optimize::operator=(), and optimize::~optimize().

## ◆ 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. Add the parsed constraints and objectives to the optimization context.

Parameters

  c | - context.
  o | - optimize context.
  s | - path to file containing SMT2 specification.

See also
  Z3_optimize_from_string
  Z3_optimize_to_string

Referenced by optimize::from_file(), and Optimize::from_file().

## ◆ 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. Add the parsed constraints and objectives to the optimization context.

Parameters

  c | - context.
  o | - optimize context.
  s | - string containing SMT2 specification.

See also
  Z3_optimize_from_file
  Z3_optimize_to_string

Referenced by optimize::from_string(), and Optimize::from_string().

## ◆ 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.

Referenced by optimize::assertions(), and Optimize::assertions().

## ◆ 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.

See also
  Z3_optimize_get_param_descrs
  Z3_optimize_set_params

Referenced by optimize::help(), and Optimize::help().

## ◆ 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.

Parameters

  c | - context
  o | - optimization context
  idx | - index of optimization objective

See also
  Z3_optimize_get_upper
  Z3_optimize_get_lower_as_vector
  Z3_optimize_get_upper_as_vector

Referenced by optimize::lower(), and OptimizeObjective::lower().

## ◆ Z3_optimize_get_lower_as_vector()

Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector | ( | Z3_context | c,
|  | Z3_optimize | o,
|  | unsigned | idx
| ) |  |

Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients `a`, `b`, `c` and encode the result of Z3_optimize_get_lower `a * infinity + b + c * epsilon`.

Parameters

  c | - context
  o | - optimization context
  idx | - index of optimization objective

See also
  Z3_optimize_get_lower
  Z3_optimize_get_upper
  Z3_optimize_get_upper_as_vector

Referenced by OptimizeObjective::lower_values().

## ◆ 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.

The error handler is invoked if a model is not available because the commands above were not invoked for the given optimization solver, or if the result was `Z3_L_FALSE`.

Referenced by optimize::get_model(), and Optimize::model().

## ◆ 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 returned as a Pseudo-Boolean (minimization) sum of the form `(+ (if f1 w1 0) (if f2 w2 0) ...)` If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.

Referenced by optimize::objectives(), and Optimize::objectives().

## ◆ Z3_optimize_get_param_descrs()

Z3_param_descrs Z3_API Z3_optimize_get_param_descrs | ( | Z3_context | c,
|  | Z3_optimize | o
| ) |  |

Return the parameter description set for the given optimize object.

Parameters

  c | - context
  o | - optimization context

See also
  Z3_optimize_get_help
  Z3_optimize_set_params

Referenced by Optimize::param_descrs().

## ◆ Z3_optimize_get_reason_unknown()

Z3_string Z3_API Z3_optimize_get_reason_unknown | ( | Z3_context | c,
|  | Z3_optimize | d
| ) |  |

Retrieve a string that describes the last status returned by Z3_optimize_check.

Use this method when Z3_optimize_check returns `Z3_L_UNDEF`.

Referenced by Optimize::reason_unknown().

## ◆ 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.

Referenced by optimize::statistics(), and Optimize::statistics().

## ◆ 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 `a`.

Referenced by optimize::unsat_core(), and Optimize::unsat_core().

## ◆ 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.

Parameters

  c | - context
  o | - optimization context
  idx | - index of optimization objective

See also
  Z3_optimize_get_lower
  Z3_optimize_get_lower_as_vector
  Z3_optimize_get_upper_as_vector

Referenced by optimize::upper(), and OptimizeObjective::upper().

## ◆ Z3_optimize_get_upper_as_vector()

Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector | ( | Z3_context | c,
|  | Z3_optimize | o,
|  | unsigned | idx
| ) |  |

Retrieve upper bound value or approximation for the i'th optimization objective.

Parameters

  c | - context
  o | - optimization context
  idx | - index of optimization objective

See also
  Z3_optimize_get_lower
  Z3_optimize_get_upper
  Z3_optimize_get_lower_as_vector

Referenced by OptimizeObjective::upper_values().

## ◆ 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.

Referenced by optimize::operator=(), and optimize::optimize().

## ◆ Z3_optimize_maximize()

unsigned Z3_API Z3_optimize_maximize | ( | Z3_context | c,
|  | Z3_optimize | o,
|  | Z3_ast | t
| ) |  |

Add a maximization constraint.

Parameters

  c | - context
  o | - optimization context
  t | - arithmetical term

See also
  Z3_optimize_minimize

Referenced by optimize::maximize(), and Optimize::maximize().

## ◆ Z3_optimize_minimize()

unsigned Z3_API Z3_optimize_minimize | ( | Z3_context | c,
|  | Z3_optimize | o,
|  | Z3_ast | t
| ) |  |

Add a minimization constraint.

Parameters

  c | - context
  o | - optimization context
  t | - arithmetical term

See also
  Z3_optimize_maximize

Referenced by optimize::minimize(), and Optimize::minimize().

## ◆ Z3_optimize_pop()

void Z3_API Z3_optimize_pop | ( | Z3_context | c,
|  | Z3_optimize | d
| ) |  |

Backtrack one level.

See also
  Z3_optimize_push

Precondition
  The number of calls to pop cannot exceed calls to push.

Referenced by optimize::pop(), and Optimize::pop().

## ◆ Z3_optimize_push()

void Z3_API Z3_optimize_push | ( | Z3_context | c,
|  | Z3_optimize | d
| ) |  |

Create a backtracking point.

The optimize solver contains a set of rules, added facts and assertions. The set of rules, facts and assertions are restored upon calling Z3_optimize_pop.

See also
  Z3_optimize_pop

Referenced by optimize::push(), and Optimize::push().

## ◆ Z3_optimize_register_model_eh()

void Z3_API Z3_optimize_register_model_eh | ( | Z3_context | c,
|  | Z3_optimize | o,
|  | Z3_model | m,
|  | void * | ctx,
|  | Z3_model_eh | model_eh
| ) |  |

register a model event handler for new models.

Referenced by Optimize::set_on_model().

## ◆ 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.

Parameters

  c | - context
  o | - optimization context
  p | - parameters

See also
  Z3_optimize_get_help
  Z3_optimize_get_param_descrs

Referenced by optimize::set(), and Optimize::set().

## ◆ 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.

Parameters

  c | - context.
  o | - optimization context.

See also
  Z3_optimize_from_file
  Z3_optimize_from_string

Referenced by Optimize::sexpr().