Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
FuncInterp Class Reference
+ Inheritance diagram for FuncInterp:

Public Member Functions

def __init__
 
def __del__
 
def else_value
 
def num_entries
 
def arity
 
def entry
 
def as_list
 
def __repr__
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Data Fields

 f
 
 ctx
 

Detailed Description

Stores the interpretation of a function in a Z3 model.

Definition at line 5077 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5080 of file z3py.py.

5081  def __init__(self, f, ctx):
5082  self.f = f
5083  self.ctx = ctx
5084  if self.f != None:
5085  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
def __del__ (   self)

Definition at line 5086 of file z3py.py.

5087  def __del__(self):
5088  if self.f != None:
5089  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)

Member Function Documentation

def __repr__ (   self)

Definition at line 5177 of file z3py.py.

5178  def __repr__(self):
5179  return obj_to_string(self)
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 5122 of file z3py.py.

5123  def arity(self):
5124  """Return the number of arguments for each entry in the function interpretation `self`.
5125 
5126  >>> f = Function('f', IntSort(), IntSort())
5127  >>> s = Solver()
5128  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5129  >>> s.check()
5130  sat
5131  >>> m = s.model()
5132  >>> m[f].arity()
5133  1
5134  """
5135  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
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 5160 of file z3py.py.

5161  def as_list(self):
5162  """Return the function interpretation as a Python list.
5163  >>> f = Function('f', IntSort(), IntSort())
5164  >>> s = Solver()
5165  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5166  >>> s.check()
5167  sat
5168  >>> m = s.model()
5169  >>> m[f]
5170  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5171  >>> m[f].as_list()
5172  [[0, 1], [1, 1], [2, 0], 1]
5173  """
5174  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5175  r.append(self.else_value())
5176  return r
def else_value (   self)
Return the `else` value for a function interpretation.

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

Referenced by FuncInterp.as_list().

5091  def else_value(self):
5092  """Return the `else` value for a function interpretation.
5093 
5094  >>> f = Function('f', IntSort(), IntSort())
5095  >>> s = Solver()
5096  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5097  >>> s.check()
5098  sat
5099  >>> m = s.model()
5100  >>> m[f]
5101  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5102  >>> m[f].else_value()
5103  1
5104  """
5105  return _to_expr_ref(Z3_func_interp_get_else(self.ctx.ref(), self.f), self.ctx)
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 5136 of file z3py.py.

Referenced by FuncInterp.as_list().

5137  def entry(self, idx):
5138  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5139 
5140  >>> f = Function('f', IntSort(), IntSort())
5141  >>> s = Solver()
5142  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5143  >>> s.check()
5144  sat
5145  >>> m = s.model()
5146  >>> m[f]
5147  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5148  >>> m[f].num_entries()
5149  3
5150  >>> m[f].entry(0)
5151  [0, 1]
5152  >>> m[f].entry(1)
5153  [1, 1]
5154  >>> m[f].entry(2)
5155  [2, 0]
5156  """
5157  if idx >= self.num_entries():
5158  raise IndexError
5159  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
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 5106 of file z3py.py.

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

5107  def num_entries(self):
5108  """Return the number of entries/points in the function interpretation `self`.
5109 
5110  >>> f = Function('f', IntSort(), IntSort())
5111  >>> s = Solver()
5112  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5113  >>> s.check()
5114  sat
5115  >>> m = s.model()
5116  >>> m[f]
5117  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5118  >>> m[f].num_entries()
5119  3
5120  """
5121  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))

Field Documentation

ctx

Definition at line 5082 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), FuncInterp.else_value(), FuncInterp.entry(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Tactic.solver(), and Fixedpoint.statistics().

f

Definition at line 5081 of file z3py.py.

Referenced by FuncInterp.__del__(), FuncInterp.arity(), FuncInterp.as_list(), FuncInterp.else_value(), FuncInterp.entry(), and FuncInterp.num_entries().