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 6667 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 6668 of file z3py.py.

6668  def __init__(self, opt, value, is_max):
6669  self._opt = opt
6670  self._value = value
6671  self._is_max = is_max
6672 

Member Function Documentation

§ lower()

def lower (   self)

Definition at line 6673 of file z3py.py.

Referenced by OptimizeObjective.value().

6673  def lower(self):
6674  opt = self._opt
6675  return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
6676 

§ upper()

def upper (   self)

Definition at line 6677 of file z3py.py.

Referenced by OptimizeObjective.value().

6677  def upper(self):
6678  opt = self._opt
6679  return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
6680 

§ value()

def value (   self)

Definition at line 6681 of file z3py.py.

6681  def value(self):
6682  if self._is_max:
6683  return self.upper()
6684  else:
6685  return self.lower()
6686