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

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5607 of file z3py.py.

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

Definition at line 5612 of file z3py.py.

5612 
5613  def __del__(self):
5614  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
Z3_stats_dec_ref
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

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 
5706  def __getattr__(self, name):
5707  """Access the value of statistical using attributes.
5708 
5709  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5710  we should use '_' (e.g., 'nlsat_propagations').
5711 
5712  >>> x = Int('x')
5713  >>> s = Then('simplify', 'nlsat').solver()
5714  >>> s.add(x > 0)
5715  >>> s.check()
5716  sat
5717  >>> st = s.statistics()
5718  >>> st.keys()
5719  ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
5720  >>> st.nlsat_propagations
5721  2
5722  >>> st.nlsat_stages
5723  2
5724  """
5725  key = name.replace('_', ' ')
5726  try:
5727  return self.get_key_value(key)
5728  except Z3Exception:
5729  raise AttributeError
z3py.Statistics.__getattr__
def __getattr__
Definition: z3py.py:5705
z3py.Statistics.get_key_value
def get_key_value
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 
5648  def __getitem__(self, idx):
5649  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
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  >>> len(st)
5658  6
5659  >>> st[0]
5660  ('nlsat propagations', 2)
5661  >>> st[1]
5662  ('nlsat stages', 2)
5663  """
5664  if idx >= len(self):
5665  raise IndexError
5666  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5667  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5668  else:
5669  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5670  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
Z3_stats_get_key
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.
z3py.Statistics.__getitem__
def __getitem__
Definition: z3py.py:5647
Z3_stats_is_uint
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_stats_get_uint_value
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_stats_get_double_value
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 __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 
5634  def __len__(self):
5635  """Return the number 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  >>> len(st)
5644  6
5645  """
5646  return int(Z3_stats_size(self.ctx.ref(), self.stats))
Z3_stats_size
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
def __repr__ (   self)

Definition at line 5615 of file z3py.py.

5615 
5616  def __repr__(self):
5617  if in_html_mode():
5618  out = io.StringIO()
5619  even = True
5620  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5621  for k, v in self:
5622  if even:
5623  out.write(u('<tr style="background-color:#CFCFCF">'))
5624  even = False
5625  else:
5626  out.write(u('<tr>'))
5627  even = True
5628  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5629  out.write(u('</table>'))
5630  return out.getvalue()
5631  else:
5632  return Z3_stats_to_string(self.ctx.ref(), self.stats)
z3py.Statistics.__repr__
def __repr__
Definition: z3py.py:5615
Z3_stats_to_string
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 
5686  def get_key_value(self, key):
5687  """Return the value of a particular statistical counter.
5688 
5689  >>> x = Int('x')
5690  >>> s = Then('simplify', 'nlsat').solver()
5691  >>> s.add(x > 0)
5692  >>> s.check()
5693  sat
5694  >>> st = s.statistics()
5695  >>> st.get_key_value('nlsat propagations')
5696  2
5697  """
5698  for idx in range(len(self)):
5699  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5700  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5701  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5702  else:
5703  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5704  raise Z3Exception("unknown key")
Z3_stats_get_key
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_stats_is_uint
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_stats_get_uint_value
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.
z3py.Statistics.get_key_value
def get_key_value
Definition: z3py.py:5685
Z3_stats_get_double_value
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 
5672  def keys(self):
5673  """Return the list of statistical counters.
5674 
5675  >>> x = Int('x')
5676  >>> s = Then('simplify', 'nlsat').solver()
5677  >>> s.add(x > 0)
5678  >>> s.check()
5679  sat
5680  >>> st = s.statistics()
5681  >>> st.keys()
5682  ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
5683  """
5684  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
Z3_stats_get_key
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

Definition at line 5609 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().

stats

Definition at line 5608 of file z3py.py.

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

Generated on Fri Apr 12 2019 11:38:54 for Z3 by   doxygen 1.8.5