Z3
Public Member Functions | Data Fields
FuncEntry Class Reference

Public Member Functions

def __init__ (self, entry, ctx)
 
def __deepcopy__
 
def __del__ (self)
 
def num_args (self)
 
def arg_value (self, idx)
 
def value (self)
 
def as_list (self)
 
def __repr__ (self)
 

Data Fields

 entry
 
 ctx
 

Detailed Description

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

Definition at line 6132 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 6135 of file z3py.py.

6135  def __init__(self, entry, ctx):
6136  self.entry = entry
6137  self.ctx = ctx
6138  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
6139 
def __init__(self, entry, ctx)
Definition: z3py.py:6135
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
ctx
Definition: z3py.py:6137
entry
Definition: z3py.py:6136
def __del__ (   self)

Definition at line 6143 of file z3py.py.

6143  def __del__(self):
6144  if self.ctx.ref() is not None and Z3_func_entry_dec_ref is not None:
6145  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
6146 
def __del__(self)
Definition: z3py.py:6143
entry
Definition: z3py.py:6136
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6140 of file z3py.py.

6140  def __deepcopy__(self, memo={}):
6141  return FuncEntry(self.entry, self.ctx)
6142 
def __deepcopy__
Definition: z3py.py:6140
Definition: z3py.py:6132
ctx
Definition: z3py.py:6137
entry
Definition: z3py.py:6136
def __repr__ (   self)

Definition at line 6237 of file z3py.py.

6237  def __repr__(self):
6238  return repr(self.as_list())
6239 
6240 
def __repr__(self)
Definition: z3py.py:6237
def as_list(self)
Definition: z3py.py:6218
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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.arg_value(0)
1
>>> e.arg_value(1)
2
>>> try:
...   e.arg_value(2)
... except IndexError:
...   print("index error")
index error

Definition at line 6165 of file z3py.py.

6165  def arg_value(self, idx):
6166  """Return the value of argument `idx`.
6167 
6168  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6169  >>> s = Solver()
6170  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6171  >>> s.check()
6172  sat
6173  >>> m = s.model()
6174  >>> f_i = m[f]
6175  >>> f_i.num_entries()
6176  1
6177  >>> e = f_i.entry(0)
6178  >>> e
6179  [1, 2, 20]
6180  >>> e.num_args()
6181  2
6182  >>> e.arg_value(0)
6183  1
6184  >>> e.arg_value(1)
6185  2
6186  >>> try:
6187  ... e.arg_value(2)
6188  ... except IndexError:
6189  ... print("index error")
6190  index error
6191  """
6192  if idx >= self.num_args():
6193  raise IndexError
6194  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
6195 
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
def num_args(self)
Definition: z3py.py:6147
ctx
Definition: z3py.py:6137
entry
Definition: z3py.py:6136
def arg_value(self, idx)
Definition: z3py.py:6165
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()
1
>>> e = f_i.entry(0)
>>> e.as_list()
[1, 2, 20]

Definition at line 6218 of file z3py.py.

Referenced by FuncEntry.__repr__().

6218  def as_list(self):
6219  """Return entry `self` as a Python list.
6220  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6221  >>> s = Solver()
6222  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6223  >>> s.check()
6224  sat
6225  >>> m = s.model()
6226  >>> f_i = m[f]
6227  >>> f_i.num_entries()
6228  1
6229  >>> e = f_i.entry(0)
6230  >>> e.as_list()
6231  [1, 2, 20]
6232  """
6233  args = [self.arg_value(i) for i in range(self.num_args())]
6234  args.append(self.value())
6235  return args
6236 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def num_args(self)
Definition: z3py.py:6147
def value(self)
Definition: z3py.py:6196
def as_list(self)
Definition: z3py.py:6218
def arg_value(self, idx)
Definition: z3py.py:6165
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()
1
>>> e = f_i.entry(0)
>>> e.num_args()
2

Definition at line 6147 of file z3py.py.

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

6147  def num_args(self):
6148  """Return the number of arguments in the given entry.
6149 
6150  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6151  >>> s = Solver()
6152  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6153  >>> s.check()
6154  sat
6155  >>> m = s.model()
6156  >>> f_i = m[f]
6157  >>> f_i.num_entries()
6158  1
6159  >>> e = f_i.entry(0)
6160  >>> e.num_args()
6161  2
6162  """
6163  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
6164 
def num_args(self)
Definition: z3py.py:6147
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
entry
Definition: z3py.py:6136
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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.value()
20

Definition at line 6196 of file z3py.py.

Referenced by FuncEntry.as_list().

6196  def value(self):
6197  """Return the value of the function at point `self`.
6198 
6199  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6200  >>> s = Solver()
6201  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6202  >>> s.check()
6203  sat
6204  >>> m = s.model()
6205  >>> f_i = m[f]
6206  >>> f_i.num_entries()
6207  1
6208  >>> e = f_i.entry(0)
6209  >>> e
6210  [1, 2, 20]
6211  >>> e.num_args()
6212  2
6213  >>> e.value()
6214  20
6215  """
6216  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
6217 
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
def value(self)
Definition: z3py.py:6196
ctx
Definition: z3py.py:6137
entry
Definition: z3py.py:6136

Field Documentation

ctx
entry