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

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5224 of file z3py.py.

5224  def __init__(self, f, ctx):
5225  self.f = f
5226  self.ctx = ctx
5227  if self.f != None:
5228  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
5229 
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.
def __init__(self, f, ctx)
Definition: z3py.py:5224
def __del__ (   self)

Definition at line 5230 of file z3py.py.

5230  def __del__(self):
5231  if self.f != None:
5232  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
5233 
def __del__(self)
Definition: z3py.py:5230
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

def __repr__ (   self)

Definition at line 5328 of file z3py.py.

5328  def __repr__(self):
5329  return obj_to_string(self)
5330 
def __repr__(self)
Definition: z3py.py:5328
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 5273 of file z3py.py.

5273  def arity(self):
5274  """Return the number of arguments for each entry in the function interpretation `self`.
5275 
5276  >>> f = Function('f', IntSort(), IntSort())
5277  >>> s = Solver()
5278  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5279  >>> s.check()
5280  sat
5281  >>> m = s.model()
5282  >>> m[f].arity()
5283  1
5284  """
5285  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
5286 
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.
def arity(self)
Definition: z3py.py:5273
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 5311 of file z3py.py.

5311  def as_list(self):
5312  """Return the function interpretation as a Python list.
5313  >>> f = Function('f', IntSort(), IntSort())
5314  >>> s = Solver()
5315  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5316  >>> s.check()
5317  sat
5318  >>> m = s.model()
5319  >>> m[f]
5320  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5321  >>> m[f].as_list()
5322  [[0, 1], [1, 1], [2, 0], 1]
5323  """
5324  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5325  r.append(self.else_value())
5326  return r
5327 
def entry(self, idx)
Definition: z3py.py:5287
def else_value(self)
Definition: z3py.py:5234
def as_list(self)
Definition: z3py.py:5311
def num_entries(self)
Definition: z3py.py:5257
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 5234 of file z3py.py.

Referenced by FuncInterp.as_list().

5234  def else_value(self):
5235  """
5236  Return the `else` value for a function interpretation.
5237  Return None if Z3 did not specify the `else` value for
5238  this object.
5239 
5240  >>> f = Function('f', IntSort(), IntSort())
5241  >>> s = Solver()
5242  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5243  >>> s.check()
5244  sat
5245  >>> m = s.model()
5246  >>> m[f]
5247  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5248  >>> m[f].else_value()
5249  1
5250  """
5251  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5252  if r:
5253  return _to_expr_ref(r, self.ctx)
5254  else:
5255  return None
5256 
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.
def else_value(self)
Definition: z3py.py:5234
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 5287 of file z3py.py.

Referenced by FuncInterp.as_list().

5287  def entry(self, idx):
5288  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5289 
5290  >>> f = Function('f', IntSort(), IntSort())
5291  >>> s = Solver()
5292  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5293  >>> s.check()
5294  sat
5295  >>> m = s.model()
5296  >>> m[f]
5297  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5298  >>> m[f].num_entries()
5299  3
5300  >>> m[f].entry(0)
5301  [0, 1]
5302  >>> m[f].entry(1)
5303  [1, 1]
5304  >>> m[f].entry(2)
5305  [2, 0]
5306  """
5307  if idx >= self.num_entries():
5308  raise IndexError
5309  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
5310 
def entry(self, idx)
Definition: z3py.py:5287
Definition: z3py.py:5117
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...
def num_entries(self)
Definition: z3py.py:5257
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 5257 of file z3py.py.

Referenced by FuncInterp.as_list(), and FuncInterp.entry().

5257  def num_entries(self):
5258  """Return the number of entries/points in the function interpretation `self`.
5259 
5260  >>> f = Function('f', IntSort(), IntSort())
5261  >>> s = Solver()
5262  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5263  >>> s.check()
5264  sat
5265  >>> m = s.model()
5266  >>> m[f]
5267  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5268  >>> m[f].num_entries()
5269  3
5270  """
5271  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
5272 
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.
def num_entries(self)
Definition: z3py.py:5257

Field Documentation

ctx
f