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

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 5060 of file z3py.py.

5060  def __init__(self, entry, ctx):
5061  self.entry = entry
5062  self.ctx = ctx
5063  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
5064 
def __init__(self, entry, ctx)
Definition: z3py.py:5060
ctx
Definition: z3py.py:5062
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:5061
def __del__ (   self)

Definition at line 5065 of file z3py.py.

5065  def __del__(self):
5066  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
5067 
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:5065
entry
Definition: z3py.py:5061

Member Function Documentation

def __repr__ (   self)

Definition at line 5158 of file z3py.py.

5158  def __repr__(self):
5159  return repr(self.as_list())
def __repr__(self)
Definition: z3py.py:5158
def as_list(self)
Definition: z3py.py:5139
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 5086 of file z3py.py.

5086  def arg_value(self, idx):
5087  """Return the value of argument `idx`.
5088 
5089  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5090  >>> s = Solver()
5091  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5092  >>> s.check()
5093  sat
5094  >>> m = s.model()
5095  >>> f_i = m[f]
5096  >>> f_i.num_entries()
5097  3
5098  >>> e = f_i.entry(0)
5099  >>> e
5100  [0, 1, 10]
5101  >>> e.num_args()
5102  2
5103  >>> e.arg_value(0)
5104  0
5105  >>> e.arg_value(1)
5106  1
5107  >>> try:
5108  ... e.arg_value(2)
5109  ... except IndexError:
5110  ... print("index error")
5111  index error
5112  """
5113  if idx >= self.num_args():
5114  raise IndexError
5115  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5116 
def num_args(self)
Definition: z3py.py:5068
ctx
Definition: z3py.py:5062
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:5061
def arg_value(self, idx)
Definition: z3py.py:5086
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 5139 of file z3py.py.

Referenced by FuncEntry.__repr__().

5139  def as_list(self):
5140  """Return entry `self` as a Python list.
5141  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5142  >>> s = Solver()
5143  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5144  >>> s.check()
5145  sat
5146  >>> m = s.model()
5147  >>> f_i = m[f]
5148  >>> f_i.num_entries()
5149  3
5150  >>> e = f_i.entry(0)
5151  >>> e.as_list()
5152  [0, 1, 10]
5153  """
5154  args = [ self.arg_value(i) for i in range(self.num_args())]
5155  args.append(self.value())
5156  return args
5157 
def num_args(self)
Definition: z3py.py:5068
def value(self)
Definition: z3py.py:5117
def as_list(self)
Definition: z3py.py:5139
def arg_value(self, idx)
Definition: z3py.py:5086
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 5068 of file z3py.py.

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

5068  def num_args(self):
5069  """Return the number of arguments in the given entry.
5070 
5071  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5072  >>> s = Solver()
5073  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5074  >>> s.check()
5075  sat
5076  >>> m = s.model()
5077  >>> f_i = m[f]
5078  >>> f_i.num_entries()
5079  3
5080  >>> e = f_i.entry(0)
5081  >>> e.num_args()
5082  2
5083  """
5084  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5085 
def num_args(self)
Definition: z3py.py:5068
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:5061
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 5117 of file z3py.py.

Referenced by FuncEntry.as_list().

5117  def value(self):
5118  """Return the value of the function at point `self`.
5119 
5120  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5121  >>> s = Solver()
5122  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5123  >>> s.check()
5124  sat
5125  >>> m = s.model()
5126  >>> f_i = m[f]
5127  >>> f_i.num_entries()
5128  3
5129  >>> e = f_i.entry(0)
5130  >>> e
5131  [0, 1, 10]
5132  >>> e.num_args()
5133  2
5134  >>> e.value()
5135  10
5136  """
5137  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5138 
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:5117
ctx
Definition: z3py.py:5062
entry
Definition: z3py.py:5061

Field Documentation

ctx
entry