Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 5161 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5164 of file z3py.py.

5165  def __init__(self, f, ctx):
5166  self.f = f
5167  self.ctx = ctx
5168  if self.f != None:
5169  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
def __init__
Definition: z3py.py:5164
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 __del__ (   self)

Definition at line 5170 of file z3py.py.

5171  def __del__(self):
5172  if self.f != None:
5173  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
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 5268 of file z3py.py.

5269  def __repr__(self):
5270  return obj_to_string(self)
def __repr__
Definition: z3py.py:5268
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 5213 of file z3py.py.

5214  def arity(self):
5215  """Return the number of arguments for each entry in the function interpretation `self`.
5216 
5217  >>> f = Function('f', IntSort(), IntSort())
5218  >>> s = Solver()
5219  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5220  >>> s.check()
5221  sat
5222  >>> m = s.model()
5223  >>> m[f].arity()
5224  1
5225  """
5226  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
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 5251 of file z3py.py.

5252  def as_list(self):
5253  """Return the function interpretation as a Python list.
5254  >>> f = Function('f', IntSort(), IntSort())
5255  >>> s = Solver()
5256  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5257  >>> s.check()
5258  sat
5259  >>> m = s.model()
5260  >>> m[f]
5261  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5262  >>> m[f].as_list()
5263  [[0, 1], [1, 1], [2, 0], 1]
5264  """
5265  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5266  r.append(self.else_value())
5267  return r
def else_value
Definition: z3py.py:5174
def num_entries
Definition: z3py.py:5197
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 5174 of file z3py.py.

Referenced by FuncInterp.as_list().

5175  def else_value(self):
5176  """
5177  Return the `else` value for a function interpretation.
5178  Return None if Z3 did not specify the `else` value for
5179  this object.
5180 
5181  >>> f = Function('f', IntSort(), IntSort())
5182  >>> s = Solver()
5183  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5184  >>> s.check()
5185  sat
5186  >>> m = s.model()
5187  >>> m[f]
5188  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5189  >>> m[f].else_value()
5190  1
5191  """
5192  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5193  if r:
5194  return _to_expr_ref(r, self.ctx)
5195  else:
5196  return None
def else_value
Definition: z3py.py:5174
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 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 5227 of file z3py.py.

Referenced by FuncInterp.as_list().

5228  def entry(self, idx):
5229  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5230 
5231  >>> f = Function('f', IntSort(), IntSort())
5232  >>> s = Solver()
5233  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5234  >>> s.check()
5235  sat
5236  >>> m = s.model()
5237  >>> m[f]
5238  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5239  >>> m[f].num_entries()
5240  3
5241  >>> m[f].entry(0)
5242  [0, 1]
5243  >>> m[f].entry(1)
5244  [1, 1]
5245  >>> m[f].entry(2)
5246  [2, 0]
5247  """
5248  if idx >= self.num_entries():
5249  raise IndexError
5250  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
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:5057
def num_entries
Definition: z3py.py:5197
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 5197 of file z3py.py.

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

5198  def num_entries(self):
5199  """Return the number of entries/points in the function interpretation `self`.
5200 
5201  >>> f = Function('f', IntSort(), IntSort())
5202  >>> s = Solver()
5203  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5204  >>> s.check()
5205  sat
5206  >>> m = s.model()
5207  >>> m[f]
5208  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5209  >>> m[f].num_entries()
5210  3
5211  """
5212  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
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
Definition: z3py.py:5197

Field Documentation

ctx

Definition at line 5166 of file z3py.py.

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

f

Definition at line 5165 of file z3py.py.

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