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 value (self)
 

Detailed Description

Optimize.

Definition at line 6400 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 6401 of file z3py.py.

6401  def __init__(self, opt, value, is_max):
6402  self._opt = opt
6403  self._value = value
6404  self._is_max = is_max
6405 
def __init__(self, opt, value, is_max)
Definition: z3py.py:6401

Member Function Documentation

def lower (   self)

Definition at line 6406 of file z3py.py.

Referenced by OptimizeObjective.value().

6406  def lower(self):
6407  opt = self._opt
6408  return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
6409 
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.
def lower(self)
Definition: z3py.py:6406
def upper (   self)

Definition at line 6410 of file z3py.py.

Referenced by OptimizeObjective.value().

6410  def upper(self):
6411  opt = self._opt
6412  return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
6413 
def upper(self)
Definition: z3py.py:6410
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.
def value (   self)

Definition at line 6414 of file z3py.py.

6414  def value(self):
6415  if self._is_max:
6416  return self.upper()
6417  else:
6418  return self.lower()
6419 
def value(self)
Definition: z3py.py:6414
def upper(self)
Definition: z3py.py:6410
def lower(self)
Definition: z3py.py:6406