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

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 6189 of file z3py.py.

6189  def __init__(self, entry, ctx):
6190  self.entry = entry
6191  self.ctx = ctx
6192  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
6193 
def __init__(self, entry, ctx)
Definition: z3py.py:6189
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:6191
entry
Definition: z3py.py:6190
def __del__ (   self)

Definition at line 6197 of file z3py.py.

6197  def __del__(self):
6198  if self.ctx.ref() is not None and Z3_func_entry_dec_ref is not None:
6199  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
6200 
def __del__(self)
Definition: z3py.py:6197
entry
Definition: z3py.py:6190
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 6194 of file z3py.py.

6194  def __deepcopy__(self, memo={}):
6195  return FuncEntry(self.entry, self.ctx)
6196 
def __deepcopy__
Definition: z3py.py:6194
Definition: z3py.py:6186
ctx
Definition: z3py.py:6191
entry
Definition: z3py.py:6190
def __repr__ (   self)

Definition at line 6291 of file z3py.py.

6291  def __repr__(self):
6292  return repr(self.as_list())
6293 
6294 
def __repr__(self)
Definition: z3py.py:6291
def as_list(self)
Definition: z3py.py:6272
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 6219 of file z3py.py.

6219  def arg_value(self, idx):
6220  """Return the value of argument `idx`.
6221 
6222  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6223  >>> s = Solver()
6224  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6225  >>> s.check()
6226  sat
6227  >>> m = s.model()
6228  >>> f_i = m[f]
6229  >>> f_i.num_entries()
6230  1
6231  >>> e = f_i.entry(0)
6232  >>> e
6233  [1, 2, 20]
6234  >>> e.num_args()
6235  2
6236  >>> e.arg_value(0)
6237  1
6238  >>> e.arg_value(1)
6239  2
6240  >>> try:
6241  ... e.arg_value(2)
6242  ... except IndexError:
6243  ... print("index error")
6244  index error
6245  """
6246  if idx >= self.num_args():
6247  raise IndexError
6248  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
6249 
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:6201
ctx
Definition: z3py.py:6191
entry
Definition: z3py.py:6190
def arg_value(self, idx)
Definition: z3py.py:6219
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 6272 of file z3py.py.

Referenced by FuncEntry.__repr__().

6272  def as_list(self):
6273  """Return entry `self` as a Python list.
6274  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6275  >>> s = Solver()
6276  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6277  >>> s.check()
6278  sat
6279  >>> m = s.model()
6280  >>> f_i = m[f]
6281  >>> f_i.num_entries()
6282  1
6283  >>> e = f_i.entry(0)
6284  >>> e.as_list()
6285  [1, 2, 20]
6286  """
6287  args = [self.arg_value(i) for i in range(self.num_args())]
6288  args.append(self.value())
6289  return args
6290 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def num_args(self)
Definition: z3py.py:6201
def value(self)
Definition: z3py.py:6250
def as_list(self)
Definition: z3py.py:6272
def arg_value(self, idx)
Definition: z3py.py:6219
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 6201 of file z3py.py.

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

6201  def num_args(self):
6202  """Return the number of arguments in the given entry.
6203 
6204  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6205  >>> s = Solver()
6206  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6207  >>> s.check()
6208  sat
6209  >>> m = s.model()
6210  >>> f_i = m[f]
6211  >>> f_i.num_entries()
6212  1
6213  >>> e = f_i.entry(0)
6214  >>> e.num_args()
6215  2
6216  """
6217  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
6218 
def num_args(self)
Definition: z3py.py:6201
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:6190
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 6250 of file z3py.py.

Referenced by FuncEntry.as_list().

6250  def value(self):
6251  """Return the value of the function at point `self`.
6252 
6253  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6254  >>> s = Solver()
6255  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6256  >>> s.check()
6257  sat
6258  >>> m = s.model()
6259  >>> f_i = m[f]
6260  >>> f_i.num_entries()
6261  1
6262  >>> e = f_i.entry(0)
6263  >>> e
6264  [1, 2, 20]
6265  >>> e.num_args()
6266  2
6267  >>> e.value()
6268  20
6269  """
6270  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
6271 
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:6250
ctx
Definition: z3py.py:6191
entry
Definition: z3py.py:6190

Field Documentation

ctx
entry