Z3 |

Public Member Functions
OptimizeObjective Class Reference

Optimize. More...

## Public Member Functions
def | __init__ (self, opt, value, is_max)
def | lower (self)
def | upper (self)
def | lower_values (self)
def | upper_values (self)
def | value (self)
def | __str__ (self)

## Detailed Description

Optimize.

Definition at line 7697 of file z3py.py.

## Constructor & Destructor Documentation

## ◆ __init__()

def __init__ | ( |  | self,
|  |  | opt,
|  |  | value,
|  |  | is_max
| ) |  |

Definition at line 7698 of file z3py.py.

7698 def __init__(self, opt, value, is_max):
7699 self._opt = opt
7700 self._value = value
7701 self._is_max = is_max
7702

## Member Function Documentation

## ◆ __str__()

def __str__ | ( |  | self | ) |

Definition at line 7725 of file z3py.py.

7725 def __str__(self):
7726 return "%s:%s" % (self._value, self._is_max)
7727
7728

## ◆ lower()

def lower | ( |  | self | ) |

Definition at line 7703 of file z3py.py.

7703 def lower(self):
7704 opt = self._opt
7705 return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7706
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.

Referenced by OptimizeObjective.value().

## ◆ lower_values()

def lower_values | ( |  | self | ) |

Definition at line 7711 of file z3py.py.

7711 def lower_values(self):
7712 opt = self._opt
7713 return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7714
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 ...

## ◆ upper()

def upper | ( |  | self | ) |

Definition at line 7707 of file z3py.py.

7707 def upper(self):
7708 opt = self._opt
7709 return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7710
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.

Referenced by OptimizeObjective.value().

## ◆ upper_values()

def upper_values | ( |  | self | ) |

Definition at line 7715 of file z3py.py.

7715 def upper_values(self):
7716 opt = self._opt
7717 return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7718
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.

## ◆ value()

def value | ( |  | self | ) |

Definition at line 7719 of file z3py.py.

7719 def value(self):
7720 if self._is_max:
7721 return self.upper()
7722 else:
7723 return self.lower()
7724

Referenced by FuncEntry.as_list().