Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
FuncEntry Class Reference

Public Member Functions

def __init__
 
def __del__
 
def num_args
 
def arg_value
 
def value
 
def as_list
 
def __repr__
 

Data Fields

 entry
 
 ctx
 

Detailed Description

Store the value of the interpretation of a function in a particular point.

Definition at line 4973 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 4976 of file z3py.py.

4977  def __init__(self, entry, ctx):
4978  self.entry = entry
4979  self.ctx = ctx
4980  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
def __del__ (   self)

Definition at line 4981 of file z3py.py.

4982  def __del__(self):
4983  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)

Member Function Documentation

def __repr__ (   self)

Definition at line 5074 of file z3py.py.

5075  def __repr__(self):
return repr(self.as_list())
def arg_value (   self,
  idx 
)
Return the value of argument `idx`.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
3
>>> e = f_i.entry(0)
>>> e
[0, 1, 10]
>>> e.num_args()
2
>>> e.arg_value(0)
0
>>> e.arg_value(1)
1
>>> try:
...   e.arg_value(2)
... except IndexError:
...   print "index error"
index error

Definition at line 5002 of file z3py.py.

5003  def arg_value(self, idx):
5004  """Return the value of argument `idx`.
5005 
5006  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5007  >>> s = Solver()
5008  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5009  >>> s.check()
5010  sat
5011  >>> m = s.model()
5012  >>> f_i = m[f]
5013  >>> f_i.num_entries()
5014  3
5015  >>> e = f_i.entry(0)
5016  >>> e
5017  [0, 1, 10]
5018  >>> e.num_args()
5019  2
5020  >>> e.arg_value(0)
5021  0
5022  >>> e.arg_value(1)
5023  1
5024  >>> try:
5025  ... e.arg_value(2)
5026  ... except IndexError:
5027  ... print "index error"
5028  index error
5029  """
5030  if idx >= self.num_args():
5031  raise IndexError
5032  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
def as_list (   self)
Return entry `self` as a Python list.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
3
>>> e = f_i.entry(0)
>>> e.as_list()
[0, 1, 10]

Definition at line 5055 of file z3py.py.

Referenced by FuncEntry.__repr__().

5056  def as_list(self):
5057  """Return entry `self` as a Python list.
5058  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5059  >>> s = Solver()
5060  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5061  >>> s.check()
5062  sat
5063  >>> m = s.model()
5064  >>> f_i = m[f]
5065  >>> f_i.num_entries()
5066  3
5067  >>> e = f_i.entry(0)
5068  >>> e.as_list()
5069  [0, 1, 10]
5070  """
5071  args = [ self.arg_value(i) for i in range(self.num_args())]
5072  args.append(self.value())
5073  return args
def num_args (   self)
Return the number of arguments in the given entry.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
3
>>> e = f_i.entry(0)
>>> e.num_args()
2

Definition at line 4984 of file z3py.py.

Referenced by FuncEntry.arg_value(), and FuncEntry.as_list().

4985  def num_args(self):
4986  """Return the number of arguments in the given entry.
4987 
4988  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4989  >>> s = Solver()
4990  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
4991  >>> s.check()
4992  sat
4993  >>> m = s.model()
4994  >>> f_i = m[f]
4995  >>> f_i.num_entries()
4996  3
4997  >>> e = f_i.entry(0)
4998  >>> e.num_args()
4999  2
5000  """
5001  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
def value (   self)
Return the value of the function at point `self`.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
3
>>> e = f_i.entry(0)
>>> e
[0, 1, 10]
>>> e.num_args()
2
>>> e.value()
10

Definition at line 5033 of file z3py.py.

Referenced by FuncEntry.as_list().

5034  def value(self):
5035  """Return the value of the function at point `self`.
5036 
5037  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5038  >>> s = Solver()
5039  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5040  >>> s.check()
5041  sat
5042  >>> m = s.model()
5043  >>> f_i = m[f]
5044  >>> f_i.num_entries()
5045  3
5046  >>> e = f_i.entry(0)
5047  >>> e
5048  [0, 1, 10]
5049  >>> e.num_args()
5050  2
5051  >>> e.value()
5052  10
5053  """
5054  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)

Field Documentation

ctx

Definition at line 4978 of file z3py.py.

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

entry

Definition at line 4977 of file z3py.py.

Referenced by FuncEntry.__del__(), FuncEntry.arg_value(), FuncEntry.num_args(), and FuncEntry.value().