Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Data Fields
FuncEntry Class Reference

Public Member Functions

def __init__
 
def __del__
 
def num_args
 
def arg_value
 
def value
 
def as_list
 
def __repr__
 

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.

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

Definition at line 5065 of file z3py.py.

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

Member Function Documentation

def __repr__ (   self)

Definition at line 5158 of file z3py.py.

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

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

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

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

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

Field Documentation

ctx

Definition at line 5062 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), FuncEntry.arg_value(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.set(), Tactic.solver(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), and FuncEntry.value().

entry

Definition at line 5061 of file z3py.py.

Referenced by FuncEntry.__del__(), FuncEntry.arg_value(), FuncEntry.num_args(), and FuncEntry.value().