Z3
Public Member Functions | Data Fields
FuncInterp Class Reference
+ Inheritance diagram for FuncInterp:

Public Member Functions

def __init__ (self, f, ctx)
 
def __del__ (self)
 
def else_value (self)
 
def num_entries (self)
 
def arity (self)
 
def entry (self, idx)
 
def as_list (self)
 
def __repr__ (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 f
 
 ctx
 

Detailed Description

Stores the interpretation of a function in a Z3 model.

Definition at line 5345 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5348 of file z3py.py.

5348  def __init__(self, f, ctx):
5349  self.f = f
5350  self.ctx = ctx
5351  if self.f is not None:
5352  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
5353 
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.

§ __del__()

def __del__ (   self)

Definition at line 5354 of file z3py.py.

5354  def __del__(self):
5355  if self.f is not None and self.ctx.ref() is not None:
5356  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
5357 
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.

Member Function Documentation

§ __repr__()

def __repr__ (   self)

Definition at line 5452 of file z3py.py.

5452  def __repr__(self):
5453  return obj_to_string(self)
5454 

§ arity()

def arity (   self)
Return the number of arguments for each entry in the function interpretation `self`.

>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f].arity()
1

Definition at line 5397 of file z3py.py.

5397  def arity(self):
5398  """Return the number of arguments for each entry in the function interpretation `self`.
5399 
5400  >>> f = Function('f', IntSort(), IntSort())
5401  >>> s = Solver()
5402  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5403  >>> s.check()
5404  sat
5405  >>> m = s.model()
5406  >>> m[f].arity()
5407  1
5408  """
5409  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
5410 
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.

§ as_list()

def as_list (   self)
Return the function interpretation as a Python list.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].as_list()
[[0, 1], [1, 1], [2, 0], 1]

Definition at line 5435 of file z3py.py.

5435  def as_list(self):
5436  """Return the function interpretation as a Python list.
5437  >>> f = Function('f', IntSort(), IntSort())
5438  >>> s = Solver()
5439  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5440  >>> s.check()
5441  sat
5442  >>> m = s.model()
5443  >>> m[f]
5444  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5445  >>> m[f].as_list()
5446  [[0, 1], [1, 1], [2, 0], 1]
5447  """
5448  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5449  r.append(self.else_value())
5450  return r
5451 

§ else_value()

def else_value (   self)
Return the `else` value for a function interpretation.
Return None if Z3 did not specify the `else` value for
this object.

>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].else_value()
1

Definition at line 5358 of file z3py.py.

5358  def else_value(self):
5359  """
5360  Return the `else` value for a function interpretation.
5361  Return None if Z3 did not specify the `else` value for
5362  this object.
5363 
5364  >>> f = Function('f', IntSort(), IntSort())
5365  >>> s = Solver()
5366  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5367  >>> s.check()
5368  sat
5369  >>> m = s.model()
5370  >>> m[f]
5371  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5372  >>> m[f].else_value()
5373  1
5374  """
5375  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5376  if r:
5377  return _to_expr_ref(r, self.ctx)
5378  else:
5379  return None
5380 
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.

§ entry()

def entry (   self,
  idx 
)
Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.

>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].num_entries()
3
>>> m[f].entry(0)
[0, 1]
>>> m[f].entry(1)
[1, 1]
>>> m[f].entry(2)
[2, 0]

Definition at line 5411 of file z3py.py.

5411  def entry(self, idx):
5412  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5413 
5414  >>> f = Function('f', IntSort(), IntSort())
5415  >>> s = Solver()
5416  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5417  >>> s.check()
5418  sat
5419  >>> m = s.model()
5420  >>> m[f]
5421  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5422  >>> m[f].num_entries()
5423  3
5424  >>> m[f].entry(0)
5425  [0, 1]
5426  >>> m[f].entry(1)
5427  [1, 1]
5428  >>> m[f].entry(2)
5429  [2, 0]
5430  """
5431  if idx >= self.num_entries():
5432  raise IndexError
5433  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
5434 
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...

§ num_entries()

def num_entries (   self)
Return the number of entries/points in the function interpretation `self`.

>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].num_entries()
3

Definition at line 5381 of file z3py.py.

Referenced by FuncInterp.entry().

5381  def num_entries(self):
5382  """Return the number of entries/points in the function interpretation `self`.
5383 
5384  >>> f = Function('f', IntSort(), IntSort())
5385  >>> s = Solver()
5386  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5387  >>> s.check()
5388  sat
5389  >>> m = s.model()
5390  >>> m[f]
5391  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5392  >>> m[f].num_entries()
5393  3
5394  """
5395  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
5396 
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.

Field Documentation

§ ctx

ctx

§ f

f