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

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5735 of file z3py.py.

5735  def __init__(self, stats, ctx):
5736  self.stats = stats
5737  self.ctx = ctx
5738  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5739 
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 5740 of file z3py.py.

5740  def __del__(self):
5741  if self.ctx.ref() is not None:
5742  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5743 
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

§ __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 5832 of file z3py.py.

5832  def __getattr__(self, name):
5833  """Access the value of statistical using attributes.
5834 
5835  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5836  we should use '_' (e.g., 'nlsat_propagations').
5837 
5838  >>> x = Int('x')
5839  >>> s = Then('simplify', 'nlsat').solver()
5840  >>> s.add(x > 0)
5841  >>> s.check()
5842  sat
5843  >>> st = s.statistics()
5844  >>> st.nlsat_propagations
5845  2
5846  >>> st.nlsat_stages
5847  2
5848  """
5849  key = name.replace('_', ' ')
5850  try:
5851  return self.get_key_value(key)
5852  except Z3Exception:
5853  raise AttributeError
5854 

§ __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 5776 of file z3py.py.

5776  def __getitem__(self, idx):
5777  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5778 
5779  >>> x = Int('x')
5780  >>> s = Then('simplify', 'nlsat').solver()
5781  >>> s.add(x > 0)
5782  >>> s.check()
5783  sat
5784  >>> st = s.statistics()
5785  >>> len(st)
5786  6
5787  >>> st[0]
5788  ('nlsat propagations', 2)
5789  >>> st[1]
5790  ('nlsat stages', 2)
5791  """
5792  if idx >= len(self):
5793  raise IndexError
5794  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5795  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5796  else:
5797  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5798  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5799 
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.
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.
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.
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.

§ __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 5762 of file z3py.py.

5762  def __len__(self):
5763  """Return the number of statistical counters.
5764 
5765  >>> x = Int('x')
5766  >>> s = Then('simplify', 'nlsat').solver()
5767  >>> s.add(x > 0)
5768  >>> s.check()
5769  sat
5770  >>> st = s.statistics()
5771  >>> len(st)
5772  6
5773  """
5774  return int(Z3_stats_size(self.ctx.ref(), self.stats))
5775 
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 5744 of file z3py.py.

5744  def __repr__(self):
5745  if in_html_mode():
5746  out = io.StringIO()
5747  even = True
5748  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5749  for k, v in self:
5750  if even:
5751  out.write(u('<tr style="background-color:#CFCFCF">'))
5752  even = False
5753  else:
5754  out.write(u('<tr>'))
5755  even = True
5756  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5757  out.write(u('</table>'))
5758  return out.getvalue()
5759  else:
5760  return Z3_stats_to_string(self.ctx.ref(), self.stats)
5761 
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 5812 of file z3py.py.

5812  def get_key_value(self, key):
5813  """Return the value of a particular statistical counter.
5814 
5815  >>> x = Int('x')
5816  >>> s = Then('simplify', 'nlsat').solver()
5817  >>> s.add(x > 0)
5818  >>> s.check()
5819  sat
5820  >>> st = s.statistics()
5821  >>> st.get_key_value('nlsat propagations')
5822  2
5823  """
5824  for idx in range(len(self)):
5825  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5826  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5827  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5828  else:
5829  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5830  raise Z3Exception("unknown key")
5831 
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.
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.
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.
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.

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

5800  def keys(self):
5801  """Return the list of statistical counters.
5802 
5803  >>> x = Int('x')
5804  >>> s = Then('simplify', 'nlsat').solver()
5805  >>> s.add(x > 0)
5806  >>> s.check()
5807  sat
5808  >>> st = s.statistics()
5809  """
5810  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5811 
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

§ stats

stats

Definition at line 5736 of file z3py.py.