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

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5187 of file z3py.py.

5187  def __init__(self, f, ctx):
5188  self.f = f
5189  self.ctx = ctx
5190  if self.f != None:
5191  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
5192 
void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
def __init__(self, f, ctx)
Definition: z3py.py:5187
def __del__ (   self)

Definition at line 5193 of file z3py.py.

5193  def __del__(self):
5194  if self.f != None:
5195  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
5196 
def __del__(self)
Definition: z3py.py:5193
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.

Member Function Documentation

def __repr__ (   self)

Definition at line 5291 of file z3py.py.

5291  def __repr__(self):
5292  return obj_to_string(self)
5293 
def __repr__(self)
Definition: z3py.py:5291
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 5236 of file z3py.py.

5236  def arity(self):
5237  """Return the number of arguments for each entry in the function interpretation `self`.
5238 
5239  >>> f = Function('f', IntSort(), IntSort())
5240  >>> s = Solver()
5241  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5242  >>> s.check()
5243  sat
5244  >>> m = s.model()
5245  >>> m[f].arity()
5246  1
5247  """
5248  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
5249 
def arity(self)
Definition: z3py.py:5236
unsigned Z3_API Z3_func_interp_get_arity(__in Z3_context c, __in Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
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 5274 of file z3py.py.

5274  def as_list(self):
5275  """Return the function interpretation as a Python list.
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]
5283  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5284  >>> m[f].as_list()
5285  [[0, 1], [1, 1], [2, 0], 1]
5286  """
5287  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5288  r.append(self.else_value())
5289  return r
5290 
def entry(self, idx)
Definition: z3py.py:5250
def else_value(self)
Definition: z3py.py:5197
def as_list(self)
Definition: z3py.py:5274
def num_entries(self)
Definition: z3py.py:5220
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 5197 of file z3py.py.

Referenced by FuncInterp.as_list().

5197  def else_value(self):
5198  """
5199  Return the `else` value for a function interpretation.
5200  Return None if Z3 did not specify the `else` value for
5201  this object.
5202 
5203  >>> f = Function('f', IntSort(), IntSort())
5204  >>> s = Solver()
5205  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5206  >>> s.check()
5207  sat
5208  >>> m = s.model()
5209  >>> m[f]
5210  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5211  >>> m[f].else_value()
5212  1
5213  """
5214  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5215  if r:
5216  return _to_expr_ref(r, self.ctx)
5217  else:
5218  return None
5219 
Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f)
Return the 'else' value of the given function interpretation.
def else_value(self)
Definition: z3py.py:5197
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 5250 of file z3py.py.

Referenced by FuncInterp.as_list().

5250  def entry(self, idx):
5251  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5252 
5253  >>> f = Function('f', IntSort(), IntSort())
5254  >>> s = Solver()
5255  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5256  >>> s.check()
5257  sat
5258  >>> m = s.model()
5259  >>> m[f]
5260  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5261  >>> m[f].num_entries()
5262  3
5263  >>> m[f].entry(0)
5264  [0, 1]
5265  >>> m[f].entry(1)
5266  [1, 1]
5267  >>> m[f].entry(2)
5268  [2, 0]
5269  """
5270  if idx >= self.num_entries():
5271  raise IndexError
5272  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
5273 
def entry(self, idx)
Definition: z3py.py:5250
Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
Definition: z3py.py:5080
def num_entries(self)
Definition: z3py.py:5220
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 5220 of file z3py.py.

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

5220  def num_entries(self):
5221  """Return the number of entries/points in the function interpretation `self`.
5222 
5223  >>> f = Function('f', IntSort(), IntSort())
5224  >>> s = Solver()
5225  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5226  >>> s.check()
5227  sat
5228  >>> m = s.model()
5229  >>> m[f]
5230  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5231  >>> m[f].num_entries()
5232  3
5233  """
5234  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
5235 
unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f)
Return the number of entries in the given function interpretation.
def num_entries(self)
Definition: z3py.py:5220

Field Documentation

ctx
f