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

Statistics. More...

Public Member Functions

def __init__
 
def __del__
 
def __repr__
 
def __len__
 
def __getitem__
 
def keys
 
def get_key_value
 
def __getattr__
 

Data Fields

 stats
 
 ctx
 

Detailed Description

Statistics.

Statistics for `Solver.check()`.

Definition at line 5453 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5456 of file z3py.py.

5457  def __init__(self, stats, ctx):
5458  self.stats = stats
5459  self.ctx = ctx
5460  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
def __del__ (   self)

Definition at line 5461 of file z3py.py.

5462  def __del__(self):
5463  Z3_stats_dec_ref(self.ctx.ref(), self.stats)

Member Function Documentation

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.keys()
['nlsat propagations', 'nlsat stages']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2

Definition at line 5554 of file z3py.py.

5555  def __getattr__(self, name):
5556  """Access the value of statistical using attributes.
5557 
5558  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5559  we should use '_' (e.g., 'nlsat_propagations').
5560 
5561  >>> x = Int('x')
5562  >>> s = Then('simplify', 'nlsat').solver()
5563  >>> s.add(x > 0)
5564  >>> s.check()
5565  sat
5566  >>> st = s.statistics()
5567  >>> st.keys()
5568  ['nlsat propagations', 'nlsat stages']
5569  >>> st.nlsat_propagations
5570  2
5571  >>> st.nlsat_stages
5572  2
5573  """
5574  key = name.replace('_', ' ')
5575  try:
5576  return self.get_key_value(key)
5577  except Z3Exception:
5578  raise AttributeError
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)
2
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)

Definition at line 5496 of file z3py.py.

5497  def __getitem__(self, idx):
5498  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5499 
5500  >>> x = Int('x')
5501  >>> s = Then('simplify', 'nlsat').solver()
5502  >>> s.add(x > 0)
5503  >>> s.check()
5504  sat
5505  >>> st = s.statistics()
5506  >>> len(st)
5507  2
5508  >>> st[0]
5509  ('nlsat propagations', 2)
5510  >>> st[1]
5511  ('nlsat stages', 2)
5512  """
5513  if idx >= len(self):
5514  raise IndexError
5515  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5516  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5517  else:
5518  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5519  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
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)
2

Definition at line 5482 of file z3py.py.

5483  def __len__(self):
5484  """Return the number of statistical counters.
5485 
5486  >>> x = Int('x')
5487  >>> s = Then('simplify', 'nlsat').solver()
5488  >>> s.add(x > 0)
5489  >>> s.check()
5490  sat
5491  >>> st = s.statistics()
5492  >>> len(st)
5493  2
5494  """
5495  return int(Z3_stats_size(self.ctx.ref(), self.stats))
def __repr__ (   self)

Definition at line 5464 of file z3py.py.

5465  def __repr__(self):
5466  if in_html_mode():
5467  out = io.StringIO()
5468  even = True
5469  out.write(u'<table border="1" cellpadding="2" cellspacing="0">')
5470  for k, v in self:
5471  if even:
5472  out.write(u'<tr style="background-color:#CFCFCF">')
5473  even = False
5474  else:
5475  out.write(u'<tr>')
5476  even = True
5477  out.write(u'<td>%s</td><td>%s</td></tr>' % (k, v))
5478  out.write(u'</table>')
5479  return out.getvalue()
5480  else:
5481  return Z3_stats_to_string(self.ctx.ref(), self.stats)
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 5534 of file z3py.py.

Referenced by Statistics.__getattr__().

5535  def get_key_value(self, key):
5536  """Return the value of a particular statistical counter.
5537 
5538  >>> x = Int('x')
5539  >>> s = Then('simplify', 'nlsat').solver()
5540  >>> s.add(x > 0)
5541  >>> s.check()
5542  sat
5543  >>> st = s.statistics()
5544  >>> st.get_key_value('nlsat propagations')
5545  2
5546  """
5547  for idx in range(len(self)):
5548  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5549  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5550  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5551  else:
5552  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5553  raise Z3Exception("unknown key")
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()
>>> st.keys()
['nlsat propagations', 'nlsat stages']

Definition at line 5520 of file z3py.py.

5521  def keys(self):
5522  """Return the list of statistical counters.
5523 
5524  >>> x = Int('x')
5525  >>> s = Then('simplify', 'nlsat').solver()
5526  >>> s.add(x > 0)
5527  >>> s.check()
5528  sat
5529  >>> st = s.statistics()
5530  >>> st.keys()
5531  ['nlsat propagations', 'nlsat stages']
5532  """
5533  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]

Field Documentation

ctx

Definition at line 5458 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Tactic.solver(), and Fixedpoint.statistics().

stats

Definition at line 5457 of file z3py.py.

Referenced by Statistics.__del__(), Statistics.__getitem__(), Statistics.__len__(), Statistics.__repr__(), Statistics.get_key_value(), and Statistics.keys().