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.

     def __init__(self, f, ctx):
         self.f   = f
         self.ctx = ctx
         if self.f is not None:
             Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
 

◆ del()

def __del__ ( self )

Definition at line 5354 of file z3py.py.

     def __del__(self):
         if self.f is not None and self.ctx.ref() is not None:
             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
 

Member Function Documentation

◆ repr()

def __repr__ ( self )

Definition at line 5452 of file z3py.py.

     def __repr__(self):
         return obj_to_string(self)
 

◆ 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.

     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
         """
         return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
 

◆ 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.

     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]
         """
         r = [ self.entry(i).as_list() for i in range(self.num_entries())]
         r.append(self.else_value())
         return r
 

◆ 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.

     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
         """
         r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
         if r:
             return _to_expr_ref(r, self.ctx)
         else:
             return None
 

Referenced by FuncInterp.as_list().

◆ 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.

     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]
         """
         if idx >= self.num_entries():
             raise IndexError
         return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
 

Referenced by FuncInterp.as_list().

◆ 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.

     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
         """
         return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
 