Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 5544 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5547 of file z3py.py.

5548  def __init__(self, stats, ctx):
5549  self.stats = stats
5550  self.ctx = ctx
5551  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
void Z3_API Z3_stats_inc_ref(__in Z3_context c, __in Z3_stats s)
Increment the reference counter of the given statistics object.
def __init__
Definition: z3py.py:5547
def __del__ (   self)

Definition at line 5552 of file z3py.py.

5553  def __del__(self):
5554  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
void Z3_API Z3_stats_dec_ref(__in Z3_context c, __in Z3_stats s)
Decrement the reference counter of the given statistics object.

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

5646  def __getattr__(self, name):
5647  """Access the value of statistical using attributes.
5648 
5649  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5650  we should use '_' (e.g., 'nlsat_propagations').
5651 
5652  >>> x = Int('x')
5653  >>> s = Then('simplify', 'nlsat').solver()
5654  >>> s.add(x > 0)
5655  >>> s.check()
5656  sat
5657  >>> st = s.statistics()
5658  >>> st.keys()
5659  ['nlsat propagations', 'nlsat stages']
5660  >>> st.nlsat_propagations
5661  2
5662  >>> st.nlsat_stages
5663  2
5664  """
5665  key = name.replace('_', ' ')
5666  try:
5667  return self.get_key_value(key)
5668  except Z3Exception:
5669  raise AttributeError
def __getattr__
Definition: z3py.py:5645
def get_key_value
Definition: z3py.py:5625
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 5587 of file z3py.py.

5588  def __getitem__(self, idx):
5589  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5590 
5591  >>> x = Int('x')
5592  >>> s = Then('simplify', 'nlsat').solver()
5593  >>> s.add(x > 0)
5594  >>> s.check()
5595  sat
5596  >>> st = s.statistics()
5597  >>> len(st)
5598  2
5599  >>> st[0]
5600  ('nlsat propagations', 2)
5601  >>> st[1]
5602  ('nlsat stages', 2)
5603  """
5604  if idx >= len(self):
5605  raise IndexError
5606  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5607  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5608  else:
5609  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5610  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
def __getitem__
Definition: z3py.py:5587
double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the double value of the given statistical data.
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the unsigned value of the given statistical data.
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 5573 of file z3py.py.

5574  def __len__(self):
5575  """Return the number of statistical counters.
5576 
5577  >>> x = Int('x')
5578  >>> s = Then('simplify', 'nlsat').solver()
5579  >>> s.add(x > 0)
5580  >>> s.check()
5581  sat
5582  >>> st = s.statistics()
5583  >>> len(st)
5584  2
5585  """
5586  return int(Z3_stats_size(self.ctx.ref(), self.stats))
unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s)
Return the number of statistical data in s.
def __repr__ (   self)

Definition at line 5555 of file z3py.py.

5556  def __repr__(self):
5557  if in_html_mode():
5558  out = io.StringIO()
5559  even = True
5560  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5561  for k, v in self:
5562  if even:
5563  out.write(u('<tr style="background-color:#CFCFCF">'))
5564  even = False
5565  else:
5566  out.write(u('<tr>'))
5567  even = True
5568  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5569  out.write(u('</table>'))
5570  return out.getvalue()
5571  else:
5572  return Z3_stats_to_string(self.ctx.ref(), self.stats)
def __repr__
Definition: z3py.py:5555
Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s)
Convert a statistics into a string.
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 5625 of file z3py.py.

Referenced by Statistics.__getattr__().

5626  def get_key_value(self, key):
5627  """Return the value of a particular statistical counter.
5628 
5629  >>> x = Int('x')
5630  >>> s = Then('simplify', 'nlsat').solver()
5631  >>> s.add(x > 0)
5632  >>> s.check()
5633  sat
5634  >>> st = s.statistics()
5635  >>> st.get_key_value('nlsat propagations')
5636  2
5637  """
5638  for idx in range(len(self)):
5639  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5640  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5641  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5642  else:
5643  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5644  raise Z3Exception("unknown key")
double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the double value of the given statistical data.
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
def get_key_value
Definition: z3py.py:5625
unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the unsigned value of the given statistical data.
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 5611 of file z3py.py.

5612  def keys(self):
5613  """Return the list of statistical counters.
5614 
5615  >>> x = Int('x')
5616  >>> s = Then('simplify', 'nlsat').solver()
5617  >>> s.add(x > 0)
5618  >>> s.check()
5619  sat
5620  >>> st = s.statistics()
5621  >>> st.keys()
5622  ['nlsat propagations', 'nlsat stages']
5623  """
5624  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.

Field Documentation

ctx

Definition at line 5549 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(), ApplyResult.as_expr(), Solver.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Solver.assertions(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Solver.model(), Solver.param_descrs(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Solver.set(), Fixedpoint.set(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Solver.to_smt2(), Solver.unsat_core(), and Fixedpoint.update_rule().

stats

Definition at line 5548 of file z3py.py.

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