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 translate (self, other_ctx)
 
def __copy__ (self)
 
def __deepcopy__
 
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 6295 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 6298 of file z3py.py.

6298  def __init__(self, f, ctx):
6299  self.f = f
6300  self.ctx = ctx
6301  if self.f is not None:
6302  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
6303 
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:6298
def __del__ (   self)

Definition at line 6304 of file z3py.py.

6304  def __del__(self):
6305  if self.f is not None and self.ctx.ref() is not None and Z3_func_interp_dec_ref is not None:
6306  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
6307 
def __del__(self)
Definition: z3py.py:6304
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 __copy__ (   self)

Definition at line 6386 of file z3py.py.

6386  def __copy__(self):
6387  return self.translate(self.ctx)
6388 
def translate(self, other_ctx)
Definition: z3py.py:6381
def __copy__(self)
Definition: z3py.py:6386
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6389 of file z3py.py.

6389  def __deepcopy__(self, memo={}):
6390  return self.translate(self.ctx)
6391 
def __deepcopy__
Definition: z3py.py:6389
def translate(self, other_ctx)
Definition: z3py.py:6381
def __repr__ (   self)

Definition at line 6409 of file z3py.py.

6409  def __repr__(self):
6410  return obj_to_string(self)
6411 
6412 
def __repr__(self)
Definition: z3py.py:6409
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 6347 of file z3py.py.

6347  def arity(self):
6348  """Return the number of arguments for each entry in the function interpretation `self`.
6349 
6350  >>> f = Function('f', IntSort(), IntSort())
6351  >>> s = Solver()
6352  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6353  >>> s.check()
6354  sat
6355  >>> m = s.model()
6356  >>> m[f].arity()
6357  1
6358  """
6359  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
6360 
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:6347
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]
[2 -> 0, else -> 1]
>>> m[f].as_list()
[[2, 0], 1]

Definition at line 6392 of file z3py.py.

6392  def as_list(self):
6393  """Return the function interpretation as a Python list.
6394  >>> f = Function('f', IntSort(), IntSort())
6395  >>> s = Solver()
6396  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6397  >>> s.check()
6398  sat
6399  >>> m = s.model()
6400  >>> m[f]
6401  [2 -> 0, else -> 1]
6402  >>> m[f].as_list()
6403  [[2, 0], 1]
6404  """
6405  r = [self.entry(i).as_list() for i in range(self.num_entries())]
6406  r.append(self.else_value())
6407  return r
6408 
def entry(self, idx)
Definition: z3py.py:6361
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def else_value(self)
Definition: z3py.py:6308
def as_list(self)
Definition: z3py.py:6392
def num_entries(self)
Definition: z3py.py:6331
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]
[2 -> 0, else -> 1]
>>> m[f].else_value()
1

Definition at line 6308 of file z3py.py.

Referenced by FuncInterp.as_list().

6308  def else_value(self):
6309  """
6310  Return the `else` value for a function interpretation.
6311  Return None if Z3 did not specify the `else` value for
6312  this object.
6313 
6314  >>> f = Function('f', IntSort(), IntSort())
6315  >>> s = Solver()
6316  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6317  >>> s.check()
6318  sat
6319  >>> m = s.model()
6320  >>> m[f]
6321  [2 -> 0, else -> 1]
6322  >>> m[f].else_value()
6323  1
6324  """
6325  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
6326  if r:
6327  return _to_expr_ref(r, self.ctx)
6328  else:
6329  return None
6330 
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:6308
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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1
>>> m[f].entry(0)
[2, 0]

Definition at line 6361 of file z3py.py.

Referenced by FuncInterp.as_list().

6361  def entry(self, idx):
6362  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
6363 
6364  >>> f = Function('f', IntSort(), IntSort())
6365  >>> s = Solver()
6366  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6367  >>> s.check()
6368  sat
6369  >>> m = s.model()
6370  >>> m[f]
6371  [2 -> 0, else -> 1]
6372  >>> m[f].num_entries()
6373  1
6374  >>> m[f].entry(0)
6375  [2, 0]
6376  """
6377  if idx >= self.num_entries():
6378  raise IndexError
6379  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
6380 
def entry(self, idx)
Definition: z3py.py:6361
Definition: z3py.py:6186
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 interpretation. It represents the value of f in a particular p...
def num_entries(self)
Definition: z3py.py:6331
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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1

Definition at line 6331 of file z3py.py.

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

6331  def num_entries(self):
6332  """Return the number of entries/points in the function interpretation `self`.
6333 
6334  >>> f = Function('f', IntSort(), IntSort())
6335  >>> s = Solver()
6336  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6337  >>> s.check()
6338  sat
6339  >>> m = s.model()
6340  >>> m[f]
6341  [2 -> 0, else -> 1]
6342  >>> m[f].num_entries()
6343  1
6344  """
6345  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
6346 
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:6331
def translate (   self,
  other_ctx 
)
Copy model 'self' to context 'other_ctx'.

Definition at line 6381 of file z3py.py.

Referenced by FuncInterp.__copy__(), and FuncInterp.__deepcopy__().

6381  def translate(self, other_ctx):
6382  """Copy model 'self' to context 'other_ctx'.
6383  """
6384  return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx)
6385 
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
def translate(self, other_ctx)
Definition: z3py.py:6381

Field Documentation

ctx
f