Z3
Public Member Functions | Data Fields
FuncEntry Class Reference

Public Member Functions

def __init__ (self, entry, ctx)
 
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 5240 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 5243 of file z3py.py.

5243  def __init__(self, entry, ctx):
5244  self.entry = entry
5245  self.ctx = ctx
5246  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
5247 
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.

§ __del__()

def __del__ (   self)

Definition at line 5248 of file z3py.py.

5248  def __del__(self):
5249  if self.ctx.ref() is not None:
5250  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
5251 
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

§ __repr__()

def __repr__ (   self)

Definition at line 5342 of file z3py.py.

5342  def __repr__(self):
5343  return repr(self.as_list())
5344 

§ arg_value()

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

5270  def arg_value(self, idx):
5271  """Return the value of argument `idx`.
5272 
5273  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5274  >>> s = Solver()
5275  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5276  >>> s.check()
5277  sat
5278  >>> m = s.model()
5279  >>> f_i = m[f]
5280  >>> f_i.num_entries()
5281  3
5282  >>> e = f_i.entry(0)
5283  >>> e
5284  [0, 1, 10]
5285  >>> e.num_args()
5286  2
5287  >>> e.arg_value(0)
5288  0
5289  >>> e.arg_value(1)
5290  1
5291  >>> try:
5292  ... e.arg_value(2)
5293  ... except IndexError:
5294  ... print("index error")
5295  index error
5296  """
5297  if idx >= self.num_args():
5298  raise IndexError
5299  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5300 
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.

§ as_list()

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

5323  def as_list(self):
5324  """Return entry `self` as a Python list.
5325  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5326  >>> s = Solver()
5327  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5328  >>> s.check()
5329  sat
5330  >>> m = s.model()
5331  >>> f_i = m[f]
5332  >>> f_i.num_entries()
5333  3
5334  >>> e = f_i.entry(0)
5335  >>> e.as_list()
5336  [0, 1, 10]
5337  """
5338  args = [ self.arg_value(i) for i in range(self.num_args())]
5339  args.append(self.value())
5340  return args
5341 

§ num_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 5252 of file z3py.py.

Referenced by AstRef.__bool__().

5252  def num_args(self):
5253  """Return the number of arguments in the given entry.
5254 
5255  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5256  >>> s = Solver()
5257  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5258  >>> s.check()
5259  sat
5260  >>> m = s.model()
5261  >>> f_i = m[f]
5262  >>> f_i.num_entries()
5263  3
5264  >>> e = f_i.entry(0)
5265  >>> e.num_args()
5266  2
5267  """
5268  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5269 
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.

§ value()

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

5301  def value(self):
5302  """Return the value of the function at point `self`.
5303 
5304  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5305  >>> s = Solver()
5306  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5307  >>> s.check()
5308  sat
5309  >>> m = s.model()
5310  >>> f_i = m[f]
5311  >>> f_i.num_entries()
5312  3
5313  >>> e = f_i.entry(0)
5314  >>> e
5315  [0, 1, 10]
5316  >>> e.num_args()
5317  2
5318  >>> e.value()
5319  10
5320  """
5321  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5322 
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.

Field Documentation

§ ctx

ctx

§ entry

entry

Definition at line 5244 of file z3py.py.