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

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 5120 of file z3py.py.

5120  def __init__(self, entry, ctx):
5121  self.entry = entry
5122  self.ctx = ctx
5123  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
5124 
def __init__(self, entry, ctx)
Definition: z3py.py:5120
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:5122
entry
Definition: z3py.py:5121
def __del__ (   self)

Definition at line 5125 of file z3py.py.

5125  def __del__(self):
5126  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
5127 
def __del__(self)
Definition: z3py.py:5125
entry
Definition: z3py.py:5121
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 __repr__ (   self)

Definition at line 5218 of file z3py.py.

5218  def __repr__(self):
5219  return repr(self.as_list())
def __repr__(self)
Definition: z3py.py:5218
def as_list(self)
Definition: z3py.py:5199
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 5146 of file z3py.py.

5146  def arg_value(self, idx):
5147  """Return the value of argument `idx`.
5148 
5149  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5150  >>> s = Solver()
5151  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5152  >>> s.check()
5153  sat
5154  >>> m = s.model()
5155  >>> f_i = m[f]
5156  >>> f_i.num_entries()
5157  3
5158  >>> e = f_i.entry(0)
5159  >>> e
5160  [0, 1, 10]
5161  >>> e.num_args()
5162  2
5163  >>> e.arg_value(0)
5164  0
5165  >>> e.arg_value(1)
5166  1
5167  >>> try:
5168  ... e.arg_value(2)
5169  ... except IndexError:
5170  ... print("index error")
5171  index error
5172  """
5173  if idx >= self.num_args():
5174  raise IndexError
5175  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5176 
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:5128
ctx
Definition: z3py.py:5122
entry
Definition: z3py.py:5121
def arg_value(self, idx)
Definition: z3py.py:5146
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 5199 of file z3py.py.

Referenced by FuncEntry.__repr__().

5199  def as_list(self):
5200  """Return entry `self` as a Python list.
5201  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5202  >>> s = Solver()
5203  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5204  >>> s.check()
5205  sat
5206  >>> m = s.model()
5207  >>> f_i = m[f]
5208  >>> f_i.num_entries()
5209  3
5210  >>> e = f_i.entry(0)
5211  >>> e.as_list()
5212  [0, 1, 10]
5213  """
5214  args = [ self.arg_value(i) for i in range(self.num_args())]
5215  args.append(self.value())
5216  return args
5217 
def num_args(self)
Definition: z3py.py:5128
def value(self)
Definition: z3py.py:5177
def as_list(self)
Definition: z3py.py:5199
def arg_value(self, idx)
Definition: z3py.py:5146
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 5128 of file z3py.py.

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

5128  def num_args(self):
5129  """Return the number of arguments in the given entry.
5130 
5131  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5132  >>> s = Solver()
5133  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5134  >>> s.check()
5135  sat
5136  >>> m = s.model()
5137  >>> f_i = m[f]
5138  >>> f_i.num_entries()
5139  3
5140  >>> e = f_i.entry(0)
5141  >>> e.num_args()
5142  2
5143  """
5144  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5145 
def num_args(self)
Definition: z3py.py:5128
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:5121
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 5177 of file z3py.py.

Referenced by FuncEntry.as_list().

5177  def value(self):
5178  """Return the value of the function at point `self`.
5179 
5180  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5181  >>> s = Solver()
5182  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5183  >>> s.check()
5184  sat
5185  >>> m = s.model()
5186  >>> f_i = m[f]
5187  >>> f_i.num_entries()
5188  3
5189  >>> e = f_i.entry(0)
5190  >>> e
5191  [0, 1, 10]
5192  >>> e.num_args()
5193  2
5194  >>> e.value()
5195  10
5196  """
5197  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5198 
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:5177
ctx
Definition: z3py.py:5122
entry
Definition: z3py.py:5121

Field Documentation

ctx
entry