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

Constructor & Destructor Documentation

def __init__ (   self,
  f,
  ctx 
)

Definition at line 5224 of file z3py.py.

5224 
5225  def __init__(self, f, ctx):
5226  self.f = f
5227  self.ctx = ctx
5228  if self.f != None:
5229  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
Z3_func_interp_inc_ref
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.
z3py.FuncInterp.__init__
def __init__
Definition: z3py.py:5224
def __del__ (   self)

Definition at line 5230 of file z3py.py.

5230 
5231  def __del__(self):
5232  if self.f != None:
5233  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
Z3_func_interp_dec_ref
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 __repr__ (   self)

Definition at line 5328 of file z3py.py.

5328 
5329  def __repr__(self):
5330  return obj_to_string(self)
z3py.FuncInterp.__repr__
def __repr__
Definition: z3py.py:5328
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 5273 of file z3py.py.

5273 
5274  def arity(self):
5275  """Return the number of arguments for each entry in the function interpretation `self`.
5276 
5277  >>> f = Function('f', IntSort(), IntSort())
5278  >>> s = Solver()
5279  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5280  >>> s.check()
5281  sat
5282  >>> m = s.model()
5283  >>> m[f].arity()
5284  1
5285  """
5286  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
Z3_func_interp_get_arity
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 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 5311 of file z3py.py.

5311 
5312  def as_list(self):
5313  """Return the function interpretation as a Python list.
5314  >>> f = Function('f', IntSort(), IntSort())
5315  >>> s = Solver()
5316  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5317  >>> s.check()
5318  sat
5319  >>> m = s.model()
5320  >>> m[f]
5321  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5322  >>> m[f].as_list()
5323  [[0, 1], [1, 1], [2, 0], 1]
5324  """
5325  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5326  r.append(self.else_value())
5327  return r
z3py.FuncInterp.else_value
def else_value
Definition: z3py.py:5234
z3py.FuncInterp.num_entries
def num_entries
Definition: z3py.py:5257
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 5234 of file z3py.py.

Referenced by FuncInterp.as_list().

5234 
5235  def else_value(self):
5236  """
5237  Return the `else` value for a function interpretation.
5238  Return None if Z3 did not specify the `else` value for
5239  this object.
5240 
5241  >>> f = Function('f', IntSort(), IntSort())
5242  >>> s = Solver()
5243  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5244  >>> s.check()
5245  sat
5246  >>> m = s.model()
5247  >>> m[f]
5248  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5249  >>> m[f].else_value()
5250  1
5251  """
5252  r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5253  if r:
5254  return _to_expr_ref(r, self.ctx)
5255  else:
5256  return None
Z3_func_interp_get_else
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.
z3py.FuncInterp.else_value
def else_value
Definition: z3py.py:5234
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 5287 of file z3py.py.

Referenced by FuncInterp.as_list().

5287 
5288  def entry(self, idx):
5289  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5290 
5291  >>> f = Function('f', IntSort(), IntSort())
5292  >>> s = Solver()
5293  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5294  >>> s.check()
5295  sat
5296  >>> m = s.model()
5297  >>> m[f]
5298  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5299  >>> m[f].num_entries()
5300  3
5301  >>> m[f].entry(0)
5302  [0, 1]
5303  >>> m[f].entry(1)
5304  [1, 1]
5305  >>> m[f].entry(2)
5306  [2, 0]
5307  """
5308  if idx >= self.num_entries():
5309  raise IndexError
5310  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
z3py.FuncEntry
Definition: z3py.py:5117
Z3_func_interp_get_entry
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a &quot;point&quot; of the given function intepretation. It represents the value of f in a particular po...
z3py.FuncInterp.num_entries
def num_entries
Definition: z3py.py:5257
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 5257 of file z3py.py.

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

5257 
5258  def num_entries(self):
5259  """Return the number of entries/points in the function interpretation `self`.
5260 
5261  >>> f = Function('f', IntSort(), IntSort())
5262  >>> s = Solver()
5263  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5264  >>> s.check()
5265  sat
5266  >>> m = s.model()
5267  >>> m[f]
5268  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5269  >>> m[f].num_entries()
5270  3
5271  """
5272  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
Z3_func_interp_get_num_entries
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.
z3py.FuncInterp.num_entries
def num_entries
Definition: z3py.py:5257

Field Documentation

ctx

Definition at line 5226 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), 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(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().

f

Definition at line 5225 of file z3py.py.

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

Generated on Fri Apr 12 2019 11:38:54 for Z3 by   doxygen 1.8.5