Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions
OptimizeObjective Class Reference

Optimize. More...

Public Member Functions

def __init__
 
def lower
 
def upper
 
def value
 

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 
6402  def __init__(self, opt, value, is_max):
6403  self._opt = opt
6404  self._value = value
6405  self._is_max = is_max

Member Function Documentation

def lower (   self)

Definition at line 6406 of file z3py.py.

Referenced by OptimizeObjective.value().

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

Definition at line 6410 of file z3py.py.

Referenced by OptimizeObjective.value().

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

Definition at line 6414 of file z3py.py.

6414 
6415  def value(self):
6416  if self._is_max:
6417  return self.upper()
6418  else:
6419  return self.lower()
Generated on Fri Apr 12 2019 11:38:55 for Z3 by   doxygen 1.8.5