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

Constructor & Destructor Documentation

def __init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 7816 of file z3py.py.

7816  def __init__(self, opt, value, is_max):
7817  self._opt = opt
7818  self._value = value
7819  self._is_max = is_max
7820 
def __init__(self, opt, value, is_max)
Definition: z3py.py:7816

Member Function Documentation

def __str__ (   self)

Definition at line 7843 of file z3py.py.

7843  def __str__(self):
7844  return "%s:%s" % (self._value, self._is_max)
7845 
7846 
def __str__(self)
Definition: z3py.py:7843
def lower (   self)

Definition at line 7821 of file z3py.py.

Referenced by OptimizeObjective.value().

7821  def lower(self):
7822  opt = self._opt
7823  return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7824 
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:7821
def lower_values (   self)

Definition at line 7829 of file z3py.py.

7829  def lower_values(self):
7830  opt = self._opt
7831  return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7832 
def lower_values(self)
Definition: z3py.py:7829
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 7825 of file z3py.py.

Referenced by OptimizeObjective.value().

7825  def upper(self):
7826  opt = self._opt
7827  return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7828 
def upper(self)
Definition: z3py.py:7825
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 7833 of file z3py.py.

7833  def upper_values(self):
7834  opt = self._opt
7835  return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7836 
def upper_values(self)
Definition: z3py.py:7833
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 7837 of file z3py.py.

7837  def value(self):
7838  if self._is_max:
7839  return self.upper()
7840  else:
7841  return self.lower()
7842 
def value(self)
Definition: z3py.py:7837
def upper(self)
Definition: z3py.py:7825
def lower(self)
Definition: z3py.py:7821