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

Optimize. More...

Public Member Functions

def __init__
 
def lower
 
def upper
 
def lower_values
 
def upper_values
 
def value
 
def __str__
 

Detailed Description

Optimize.

Definition at line 7292 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 7293 of file z3py.py.

7294  def __init__(self, opt, value, is_max):
7295  self._opt = opt
7296  self._value = value
7297  self._is_max = is_max

Member Function Documentation

def __str__ (   self)

Definition at line 7320 of file z3py.py.

7321  def __str__(self):
7322  return "%s:%s" % (self._value, self._is_max)
7323 
def lower (   self)

Definition at line 7298 of file z3py.py.

Referenced by OptimizeObjective.value().

7299  def lower(self):
7300  opt = self._opt
7301  return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
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_values (   self)

Definition at line 7306 of file z3py.py.

7307  def lower_values(self):
7308  opt = self._opt
7309  return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
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 ...
def upper (   self)

Definition at line 7302 of file z3py.py.

Referenced by OptimizeObjective.value().

7303  def upper(self):
7304  opt = self._opt
7305  return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
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 upper_values (   self)

Definition at line 7310 of file z3py.py.

7311  def upper_values(self):
7312  opt = self._opt
7313  return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
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.
def value (   self)

Definition at line 7314 of file z3py.py.

7315  def value(self):
7316  if self._is_max:
7317  return self.upper()
7318  else:
7319  return self.lower()