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

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5607 of file z3py.py.

5607  def __init__(self, stats, ctx):
5608  self.stats = stats
5609  self.ctx = ctx
5610  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5611 
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
def __init__(self, stats, ctx)
Definition: z3py.py:5607
def __del__ (   self)

Definition at line 5612 of file z3py.py.

5612  def __del__(self):
5613  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5614 
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
def __del__(self)
Definition: z3py.py:5612

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', 'rlimit count', 'max memory', 'memory', 'num allocs']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2

Definition at line 5705 of file z3py.py.

5705  def __getattr__(self, name):
5706  """Access the value of statistical using attributes.
5707 
5708  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5709  we should use '_' (e.g., 'nlsat_propagations').
5710 
5711  >>> x = Int('x')
5712  >>> s = Then('simplify', 'nlsat').solver()
5713  >>> s.add(x > 0)
5714  >>> s.check()
5715  sat
5716  >>> st = s.statistics()
5717  >>> st.keys()
5718  ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
5719  >>> st.nlsat_propagations
5720  2
5721  >>> st.nlsat_stages
5722  2
5723  """
5724  key = name.replace('_', ' ')
5725  try:
5726  return self.get_key_value(key)
5727  except Z3Exception:
5728  raise AttributeError
5729 
def __getattr__(self, name)
Definition: z3py.py:5705
def get_key_value(self, key)
Definition: z3py.py:5685
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 5647 of file z3py.py.

5647  def __getitem__(self, idx):
5648  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5649 
5650  >>> x = Int('x')
5651  >>> s = Then('simplify', 'nlsat').solver()
5652  >>> s.add(x > 0)
5653  >>> s.check()
5654  sat
5655  >>> st = s.statistics()
5656  >>> len(st)
5657  6
5658  >>> st[0]
5659  ('nlsat propagations', 2)
5660  >>> st[1]
5661  ('nlsat stages', 2)
5662  """
5663  if idx >= len(self):
5664  raise IndexError
5665  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5666  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5667  else:
5668  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5669  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5670 
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.
def __getitem__(self, idx)
Definition: z3py.py:5647
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 5633 of file z3py.py.

5633  def __len__(self):
5634  """Return the number of statistical counters.
5635 
5636  >>> x = Int('x')
5637  >>> s = Then('simplify', 'nlsat').solver()
5638  >>> s.add(x > 0)
5639  >>> s.check()
5640  sat
5641  >>> st = s.statistics()
5642  >>> len(st)
5643  6
5644  """
5645  return int(Z3_stats_size(self.ctx.ref(), self.stats))
5646 
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
def __len__(self)
Definition: z3py.py:5633
def __repr__ (   self)

Definition at line 5615 of file z3py.py.

5615  def __repr__(self):
5616  if in_html_mode():
5617  out = io.StringIO()
5618  even = True
5619  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5620  for k, v in self:
5621  if even:
5622  out.write(u('<tr style="background-color:#CFCFCF">'))
5623  even = False
5624  else:
5625  out.write(u('<tr>'))
5626  even = True
5627  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5628  out.write(u('</table>'))
5629  return out.getvalue()
5630  else:
5631  return Z3_stats_to_string(self.ctx.ref(), self.stats)
5632 
def __repr__(self)
Definition: z3py.py:5615
Z3_string Z3_API Z3_stats_to_string(Z3_context c, 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 5685 of file z3py.py.

Referenced by Statistics.__getattr__().

5685  def get_key_value(self, key):
5686  """Return the value of a particular statistical counter.
5687 
5688  >>> x = Int('x')
5689  >>> s = Then('simplify', 'nlsat').solver()
5690  >>> s.add(x > 0)
5691  >>> s.check()
5692  sat
5693  >>> st = s.statistics()
5694  >>> st.get_key_value('nlsat propagations')
5695  2
5696  """
5697  for idx in range(len(self)):
5698  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5699  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5700  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5701  else:
5702  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5703  raise Z3Exception("unknown key")
5704 
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.
def get_key_value(self, key)
Definition: z3py.py:5685
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.
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', 'rlimit count', 'max memory', 'memory', 'num allocs']

Definition at line 5671 of file z3py.py.

5671  def keys(self):
5672  """Return the list of statistical counters.
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', 'rlimit count', 'max memory', 'memory', 'num allocs']
5682  """
5683  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5684 
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.
def keys(self)
Definition: z3py.py:5671

Field Documentation

ctx
stats