Z3
Public Member Functions | Data Fields
Statistics Class Reference

Statistics. More...

Public Member Functions

def __init__ (self, stats, ctx)
 
def __deepcopy__ (self, memo={})
 
def __del__ (self)
 
def __repr__ (self)
 
def __len__ (self)
 
def __getitem__ (self, idx)
 
def keys (self)
 
def get_key_value (self, key)
 
def __getattr__ (self, name)
 

Data Fields

 stats
 
 ctx
 

Detailed Description

Statistics.

Statistics for `Solver.check()`.

Definition at line 5853 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5856 of file z3py.py.

5856  def __init__(self, stats, ctx):
5857  self.stats = stats
5858  self.ctx = ctx
5859  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5860 
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.

◆ __del__()

def __del__ (   self)

Definition at line 5864 of file z3py.py.

5864  def __del__(self):
5865  if self.ctx.ref() is not None:
5866  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5867 
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 5861 of file z3py.py.

5861  def __deepcopy__(self, memo={}):
5862  return Statistics(self.stats, self.ctx)
5863 

◆ __getattr__()

def __getattr__ (   self,
  name 
)
Access the value of statistical using attributes.

Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
we should use '_' (e.g., 'nlsat_propagations').

>>> x = Int('x')
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2

Definition at line 5956 of file z3py.py.

5956  def __getattr__(self, name):
5957  """Access the value of statistical using attributes.
5958 
5959  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5960  we should use '_' (e.g., 'nlsat_propagations').
5961 
5962  >>> x = Int('x')
5963  >>> s = Then('simplify', 'nlsat').solver()
5964  >>> s.add(x > 0)
5965  >>> s.check()
5966  sat
5967  >>> st = s.statistics()
5968  >>> st.nlsat_propagations
5969  2
5970  >>> st.nlsat_stages
5971  2
5972  """
5973  key = name.replace('_', ' ')
5974  try:
5975  return self.get_key_value(key)
5976  except Z3Exception:
5977  raise AttributeError
5978 

◆ __getitem__()

def __getitem__ (   self,
  idx 
)
Return the value of statistical counter at position `idx`. The result is a pair (key, value).

>>> x = Int('x')
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> len(st)
6
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)

Definition at line 5900 of file z3py.py.

5900  def __getitem__(self, idx):
5901  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5902 
5903  >>> x = Int('x')
5904  >>> s = Then('simplify', 'nlsat').solver()
5905  >>> s.add(x > 0)
5906  >>> s.check()
5907  sat
5908  >>> st = s.statistics()
5909  >>> len(st)
5910  6
5911  >>> st[0]
5912  ('nlsat propagations', 2)
5913  >>> st[1]
5914  ('nlsat stages', 2)
5915  """
5916  if idx >= len(self):
5917  raise IndexError
5918  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5919  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5920  else:
5921  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5922  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5923 
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.

◆ __len__()

def __len__ (   self)
Return the number of statistical counters.

>>> x = Int('x')
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> len(st)
6

Definition at line 5886 of file z3py.py.

5886  def __len__(self):
5887  """Return the number of statistical counters.
5888 
5889  >>> x = Int('x')
5890  >>> s = Then('simplify', 'nlsat').solver()
5891  >>> s.add(x > 0)
5892  >>> s.check()
5893  sat
5894  >>> st = s.statistics()
5895  >>> len(st)
5896  6
5897  """
5898  return int(Z3_stats_size(self.ctx.ref(), self.stats))
5899 
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.

◆ __repr__()

def __repr__ (   self)

Definition at line 5868 of file z3py.py.

5868  def __repr__(self):
5869  if in_html_mode():
5870  out = io.StringIO()
5871  even = True
5872  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5873  for k, v in self:
5874  if even:
5875  out.write(u('<tr style="background-color:#CFCFCF">'))
5876  even = False
5877  else:
5878  out.write(u('<tr>'))
5879  even = True
5880  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5881  out.write(u('</table>'))
5882  return out.getvalue()
5883  else:
5884  return Z3_stats_to_string(self.ctx.ref(), self.stats)
5885 
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.

◆ get_key_value()

def get_key_value (   self,
  key 
)
Return the value of a particular statistical counter.

>>> x = Int('x')
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('nlsat propagations')
2

Definition at line 5936 of file z3py.py.

5936  def get_key_value(self, key):
5937  """Return the value of a particular statistical counter.
5938 
5939  >>> x = Int('x')
5940  >>> s = Then('simplify', 'nlsat').solver()
5941  >>> s.add(x > 0)
5942  >>> s.check()
5943  sat
5944  >>> st = s.statistics()
5945  >>> st.get_key_value('nlsat propagations')
5946  2
5947  """
5948  for idx in range(len(self)):
5949  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5950  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5951  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5952  else:
5953  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5954  raise Z3Exception("unknown key")
5955 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.

◆ keys()

def keys (   self)
Return the list of statistical counters.

>>> x = Int('x')
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()

Definition at line 5924 of file z3py.py.

5924  def keys(self):
5925  """Return the list of statistical counters.
5926 
5927  >>> x = Int('x')
5928  >>> s = Then('simplify', 'nlsat').solver()
5929  >>> s.add(x > 0)
5930  >>> s.check()
5931  sat
5932  >>> st = s.statistics()
5933  """
5934  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5935 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.

Field Documentation

◆ ctx

ctx

Definition at line 5858 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

◆ stats

stats

Definition at line 5857 of file z3py.py.