Z3
Public Member Functions | Data Fields
Statistics Class Reference

Statistics. More...

Public Member Functions

def __init__ (self, stats, ctx)
 
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 5567 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5570 of file z3py.py.

5570  def __init__(self, stats, ctx):
5571  self.stats = stats
5572  self.ctx = ctx
5573  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5574 
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__(self, stats, ctx)
Definition: z3py.py:5570
def __del__ (   self)

Definition at line 5575 of file z3py.py.

5575  def __del__(self):
5576  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5577 
def __del__(self)
Definition: z3py.py:5575
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 5668 of file z3py.py.

5668  def __getattr__(self, name):
5669  """Access the value of statistical using attributes.
5670 
5671  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5672  we should use '_' (e.g., 'nlsat_propagations').
5673 
5674  >>> x = Int('x')
5675  >>> s = Then('simplify', 'nlsat').solver()
5676  >>> s.add(x > 0)
5677  >>> s.check()
5678  sat
5679  >>> st = s.statistics()
5680  >>> st.keys()
5681  ['nlsat propagations', 'nlsat stages']
5682  >>> st.nlsat_propagations
5683  2
5684  >>> st.nlsat_stages
5685  2
5686  """
5687  key = name.replace('_', ' ')
5688  try:
5689  return self.get_key_value(key)
5690  except Z3Exception:
5691  raise AttributeError
5692 
def __getattr__(self, name)
Definition: z3py.py:5668
def get_key_value(self, key)
Definition: z3py.py:5648
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 5610 of file z3py.py.

5610  def __getitem__(self, idx):
5611  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5612 
5613  >>> x = Int('x')
5614  >>> s = Then('simplify', 'nlsat').solver()
5615  >>> s.add(x > 0)
5616  >>> s.check()
5617  sat
5618  >>> st = s.statistics()
5619  >>> len(st)
5620  2
5621  >>> st[0]
5622  ('nlsat propagations', 2)
5623  >>> st[1]
5624  ('nlsat stages', 2)
5625  """
5626  if idx >= len(self):
5627  raise IndexError
5628  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5629  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5630  else:
5631  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5632  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5633 
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 __getitem__(self, idx)
Definition: z3py.py:5610
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 5596 of file z3py.py.

5596  def __len__(self):
5597  """Return the number of statistical counters.
5598 
5599  >>> x = Int('x')
5600  >>> s = Then('simplify', 'nlsat').solver()
5601  >>> s.add(x > 0)
5602  >>> s.check()
5603  sat
5604  >>> st = s.statistics()
5605  >>> len(st)
5606  2
5607  """
5608  return int(Z3_stats_size(self.ctx.ref(), self.stats))
5609 
unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s)
Return the number of statistical data in s.
def __len__(self)
Definition: z3py.py:5596
def __repr__ (   self)

Definition at line 5578 of file z3py.py.

5578  def __repr__(self):
5579  if in_html_mode():
5580  out = io.StringIO()
5581  even = True
5582  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5583  for k, v in self:
5584  if even:
5585  out.write(u('<tr style="background-color:#CFCFCF">'))
5586  even = False
5587  else:
5588  out.write(u('<tr>'))
5589  even = True
5590  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5591  out.write(u('</table>'))
5592  return out.getvalue()
5593  else:
5594  return Z3_stats_to_string(self.ctx.ref(), self.stats)
5595 
Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s)
Convert a statistics into a string.
def __repr__(self)
Definition: z3py.py:5578
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 5648 of file z3py.py.

Referenced by Statistics.__getattr__().

5648  def get_key_value(self, key):
5649  """Return the value of a particular statistical counter.
5650 
5651  >>> x = Int('x')
5652  >>> s = Then('simplify', 'nlsat').solver()
5653  >>> s.add(x > 0)
5654  >>> s.check()
5655  sat
5656  >>> st = s.statistics()
5657  >>> st.get_key_value('nlsat propagations')
5658  2
5659  """
5660  for idx in range(len(self)):
5661  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5662  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5663  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5664  else:
5665  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5666  raise Z3Exception("unknown key")
5667 
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.
def get_key_value(self, key)
Definition: z3py.py:5648
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 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 5634 of file z3py.py.

5634  def keys(self):
5635  """Return the list of statistical counters.
5636 
5637  >>> x = Int('x')
5638  >>> s = Then('simplify', 'nlsat').solver()
5639  >>> s.add(x > 0)
5640  >>> s.check()
5641  sat
5642  >>> st = s.statistics()
5643  >>> st.keys()
5644  ['nlsat propagations', 'nlsat stages']
5645  """
5646  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5647 
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.
def keys(self)
Definition: z3py.py:5634

Field Documentation

ctx
stats