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

Public Member Functions

def __init__
 
def __deepcopy__
 
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 5712 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  entry,
  ctx 
)

Definition at line 5715 of file z3py.py.

5716  def __init__(self, entry, ctx):
5717  self.entry = entry
5718  self.ctx = ctx
5719  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
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:5717
entry
Definition: z3py.py:5716
def __init__
Definition: z3py.py:5715
def __del__ (   self)

Definition at line 5723 of file z3py.py.

5724  def __del__(self):
5725  if self.ctx.ref() is not None:
5726  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
def __del__
Definition: z3py.py:5723
entry
Definition: z3py.py:5716
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 __deepcopy__ (   self,
  memo = {} 
)

Definition at line 5720 of file z3py.py.

5721  def __deepcopy__(self, memo={}):
5722  return FuncEntry(self.entry, self.ctx)
def __deepcopy__
Definition: z3py.py:5720
Definition: z3py.py:5712
ctx
Definition: z3py.py:5717
entry
Definition: z3py.py:5716
def __repr__ (   self)

Definition at line 5817 of file z3py.py.

5818  def __repr__(self):
5819  return repr(self.as_list())
def as_list
Definition: z3py.py:5798
def __repr__
Definition: z3py.py:5817
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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.arg_value(0)
1
>>> e.arg_value(1)
2
>>> try:
...   e.arg_value(2)
... except IndexError:
...   print("index error")
index error

Definition at line 5745 of file z3py.py.

5746  def arg_value(self, idx):
5747  """Return the value of argument `idx`.
5748 
5749  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5750  >>> s = Solver()
5751  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5752  >>> s.check()
5753  sat
5754  >>> m = s.model()
5755  >>> f_i = m[f]
5756  >>> f_i.num_entries()
5757  1
5758  >>> e = f_i.entry(0)
5759  >>> e
5760  [1, 2, 20]
5761  >>> e.num_args()
5762  2
5763  >>> e.arg_value(0)
5764  1
5765  >>> e.arg_value(1)
5766  2
5767  >>> try:
5768  ... e.arg_value(2)
5769  ... except IndexError:
5770  ... print("index error")
5771  index error
5772  """
5773  if idx >= self.num_args():
5774  raise IndexError
5775  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
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 arg_value
Definition: z3py.py:5745
ctx
Definition: z3py.py:5717
entry
Definition: z3py.py:5716
def num_args
Definition: z3py.py:5727
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()
1
>>> e = f_i.entry(0)
>>> e.as_list()
[1, 2, 20]

Definition at line 5798 of file z3py.py.

Referenced by FuncEntry.__repr__().

5799  def as_list(self):
5800  """Return entry `self` as a Python list.
5801  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5802  >>> s = Solver()
5803  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5804  >>> s.check()
5805  sat
5806  >>> m = s.model()
5807  >>> f_i = m[f]
5808  >>> f_i.num_entries()
5809  1
5810  >>> e = f_i.entry(0)
5811  >>> e.as_list()
5812  [1, 2, 20]
5813  """
5814  args = [ self.arg_value(i) for i in range(self.num_args())]
5815  args.append(self.value())
5816  return args
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def as_list
Definition: z3py.py:5798
def value
Definition: z3py.py:5776
def arg_value
Definition: z3py.py:5745
def num_args
Definition: z3py.py:5727
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()
1
>>> e = f_i.entry(0)
>>> e.num_args()
2

Definition at line 5727 of file z3py.py.

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

5728  def num_args(self):
5729  """Return the number of arguments in the given entry.
5730 
5731  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5732  >>> s = Solver()
5733  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5734  >>> s.check()
5735  sat
5736  >>> m = s.model()
5737  >>> f_i = m[f]
5738  >>> f_i.num_entries()
5739  1
5740  >>> e = f_i.entry(0)
5741  >>> e.num_args()
5742  2
5743  """
5744  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
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:5716
def num_args
Definition: z3py.py:5727
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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.value()
20

Definition at line 5776 of file z3py.py.

Referenced by FuncEntry.as_list().

5777  def value(self):
5778  """Return the value of the function at point `self`.
5779 
5780  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5781  >>> s = Solver()
5782  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5783  >>> s.check()
5784  sat
5785  >>> m = s.model()
5786  >>> f_i = m[f]
5787  >>> f_i.num_entries()
5788  1
5789  >>> e = f_i.entry(0)
5790  >>> e
5791  [1, 2, 20]
5792  >>> e.num_args()
5793  2
5794  >>> e.value()
5795  20
5796  """
5797  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
def value
Definition: z3py.py:5776
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
ctx
Definition: z3py.py:5717
entry
Definition: z3py.py:5716

Field Documentation

ctx

Definition at line 5717 of file z3py.py.

Referenced by FuncEntry.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), FuncEntry.arg_value(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), Fixedpoint.update_rule(), and FuncEntry.value().

entry

Definition at line 5716 of file z3py.py.

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