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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 7383 of file z3py.py.

7383  def __init__(self, opt, value, is_max):
7384  self._opt = opt
7385  self._value = value
7386  self._is_max = is_max
7387 

Member Function Documentation

◆ __str__()

def __str__ (   self)

Definition at line 7410 of file z3py.py.

7410  def __str__(self):
7411  return "%s:%s" % (self._value, self._is_max)
7412 
7413 

◆ lower()

def lower (   self)

Definition at line 7388 of file z3py.py.

7388  def lower(self):
7389  opt = self._opt
7390  return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7391 

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self)

Definition at line 7396 of file z3py.py.

7396  def lower_values(self):
7397  opt = self._opt
7398  return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7399 

◆ upper()

def upper (   self)

Definition at line 7392 of file z3py.py.

7392  def upper(self):
7393  opt = self._opt
7394  return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7395 

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self)

Definition at line 7400 of file z3py.py.

7400  def upper_values(self):
7401  opt = self._opt
7402  return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7403 

◆ value()

def value (   self)

Definition at line 7404 of file z3py.py.

7404  def value(self):
7405  if self._is_max:
7406  return self.upper()
7407  else:
7408  return self.lower()
7409 
Z3_optimize_get_lower_as_vector
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 ...
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10597
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.
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.
Z3_optimize_get_upper_as_vector
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.