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

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 5083 of file z3py.py.

5083  def __init__(self, entry, ctx):
5084  self.entry = entry
5085  self.ctx = ctx
5086  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
5087 
def __init__(self, entry, ctx)
Definition: z3py.py:5083
ctx
Definition: z3py.py:5085
void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
entry
Definition: z3py.py:5084
def __del__ (   self)

Definition at line 5088 of file z3py.py.

5088  def __del__(self):
5089  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
5090 
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
def __del__(self)
Definition: z3py.py:5088
entry
Definition: z3py.py:5084

Member Function Documentation

def __repr__ (   self)

Definition at line 5181 of file z3py.py.

5181  def __repr__(self):
5182  return repr(self.as_list())
def __repr__(self)
Definition: z3py.py:5181
def as_list(self)
Definition: z3py.py:5162
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 5109 of file z3py.py.

5109  def arg_value(self, idx):
5110  """Return the value of argument `idx`.
5111 
5112  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5113  >>> s = Solver()
5114  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5115  >>> s.check()
5116  sat
5117  >>> m = s.model()
5118  >>> f_i = m[f]
5119  >>> f_i.num_entries()
5120  3
5121  >>> e = f_i.entry(0)
5122  >>> e
5123  [0, 1, 10]
5124  >>> e.num_args()
5125  2
5126  >>> e.arg_value(0)
5127  0
5128  >>> e.arg_value(1)
5129  1
5130  >>> try:
5131  ... e.arg_value(2)
5132  ... except IndexError:
5133  ... print("index error")
5134  index error
5135  """
5136  if idx >= self.num_args():
5137  raise IndexError
5138  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5139 
def num_args(self)
Definition: z3py.py:5091
ctx
Definition: z3py.py:5085
Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i)
Return an argument of a Z3_func_entry object.
entry
Definition: z3py.py:5084
def arg_value(self, idx)
Definition: z3py.py:5109
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 5162 of file z3py.py.

Referenced by FuncEntry.__repr__().

5162  def as_list(self):
5163  """Return entry `self` as a Python list.
5164  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5165  >>> s = Solver()
5166  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5167  >>> s.check()
5168  sat
5169  >>> m = s.model()
5170  >>> f_i = m[f]
5171  >>> f_i.num_entries()
5172  3
5173  >>> e = f_i.entry(0)
5174  >>> e.as_list()
5175  [0, 1, 10]
5176  """
5177  args = [ self.arg_value(i) for i in range(self.num_args())]
5178  args.append(self.value())
5179  return args
5180 
def num_args(self)
Definition: z3py.py:5091
def value(self)
Definition: z3py.py:5140
def as_list(self)
Definition: z3py.py:5162
def arg_value(self, idx)
Definition: z3py.py:5109
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 5091 of file z3py.py.

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

5091  def num_args(self):
5092  """Return the number of arguments in the given entry.
5093 
5094  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5095  >>> s = Solver()
5096  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5097  >>> s.check()
5098  sat
5099  >>> m = s.model()
5100  >>> f_i = m[f]
5101  >>> f_i.num_entries()
5102  3
5103  >>> e = f_i.entry(0)
5104  >>> e.num_args()
5105  2
5106  """
5107  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5108 
def num_args(self)
Definition: z3py.py:5091
unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
entry
Definition: z3py.py:5084
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 5140 of file z3py.py.

Referenced by FuncEntry.as_list().

5140  def value(self):
5141  """Return the value of the function at point `self`.
5142 
5143  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5144  >>> s = Solver()
5145  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5146  >>> s.check()
5147  sat
5148  >>> m = s.model()
5149  >>> f_i = m[f]
5150  >>> f_i.num_entries()
5151  3
5152  >>> e = f_i.entry(0)
5153  >>> e
5154  [0, 1, 10]
5155  >>> e.num_args()
5156  2
5157  >>> e.value()
5158  10
5159  """
5160  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5161 
Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e)
Return the value of this point.
def value(self)
Definition: z3py.py:5140
ctx
Definition: z3py.py:5085
entry
Definition: z3py.py:5084

Field Documentation

ctx
entry