Z3
Public Member Functions | Data Fields
Statistics Class Reference

Statistics. More...

Public Member Functions

def __init__ (self, stats, ctx)
 
def __deepcopy__ (self, memo={})
 
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 6296 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 6299 of file z3py.py.

6299  def __init__(self, stats, ctx):
6300  self.stats = stats
6301  self.ctx = ctx
6302  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
6303 

◆ __del__()

def __del__ (   self)

Definition at line 6307 of file z3py.py.

6307  def __del__(self):
6308  if self.ctx.ref() is not None:
6309  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
6310 

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6304 of file z3py.py.

6304  def __deepcopy__(self, memo={}):
6305  return Statistics(self.stats, self.ctx)
6306 

◆ __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 6399 of file z3py.py.

6399  def __getattr__(self, name):
6400  """Access the value of statistical using attributes.
6401 
6402  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
6403  we should use '_' (e.g., 'nlsat_propagations').
6404 
6405  >>> x = Int('x')
6406  >>> s = Then('simplify', 'nlsat').solver()
6407  >>> s.add(x > 0)
6408  >>> s.check()
6409  sat
6410  >>> st = s.statistics()
6411  >>> st.nlsat_propagations
6412  2
6413  >>> st.nlsat_stages
6414  2
6415  """
6416  key = name.replace('_', ' ')
6417  try:
6418  return self.get_key_value(key)
6419  except Z3Exception:
6420  raise AttributeError
6421 

◆ __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 6343 of file z3py.py.

6343  def __getitem__(self, idx):
6344  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
6345 
6346  >>> x = Int('x')
6347  >>> s = Then('simplify', 'nlsat').solver()
6348  >>> s.add(x > 0)
6349  >>> s.check()
6350  sat
6351  >>> st = s.statistics()
6352  >>> len(st)
6353  6
6354  >>> st[0]
6355  ('nlsat propagations', 2)
6356  >>> st[1]
6357  ('nlsat stages', 2)
6358  """
6359  if idx >= len(self):
6360  raise IndexError
6361  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6362  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6363  else:
6364  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6365  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
6366 

◆ __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 6329 of file z3py.py.

6329  def __len__(self):
6330  """Return the number of statistical counters.
6331 
6332  >>> x = Int('x')
6333  >>> s = Then('simplify', 'nlsat').solver()
6334  >>> s.add(x > 0)
6335  >>> s.check()
6336  sat
6337  >>> st = s.statistics()
6338  >>> len(st)
6339  6
6340  """
6341  return int(Z3_stats_size(self.ctx.ref(), self.stats))
6342 

◆ __repr__()

def __repr__ (   self)

Definition at line 6311 of file z3py.py.

6311  def __repr__(self):
6312  if in_html_mode():
6313  out = io.StringIO()
6314  even = True
6315  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
6316  for k, v in self:
6317  if even:
6318  out.write(u('<tr style="background-color:#CFCFCF">'))
6319  even = False
6320  else:
6321  out.write(u('<tr>'))
6322  even = True
6323  out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
6324  out.write(u('</table>'))
6325  return out.getvalue()
6326  else:
6327  return Z3_stats_to_string(self.ctx.ref(), self.stats)
6328 

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

6379  def get_key_value(self, key):
6380  """Return the value of a particular statistical counter.
6381 
6382  >>> x = Int('x')
6383  >>> s = Then('simplify', 'nlsat').solver()
6384  >>> s.add(x > 0)
6385  >>> s.check()
6386  sat
6387  >>> st = s.statistics()
6388  >>> st.get_key_value('nlsat propagations')
6389  2
6390  """
6391  for idx in range(len(self)):
6392  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
6393  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6394  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6395  else:
6396  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6397  raise Z3Exception("unknown key")
6398 

Referenced by Statistics.__getattr__().

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

6367  def keys(self):
6368  """Return the list of statistical counters.
6369 
6370  >>> x = Int('x')
6371  >>> s = Then('simplify', 'nlsat').solver()
6372  >>> s.add(x > 0)
6373  >>> s.check()
6374  sat
6375  >>> st = s.statistics()
6376  """
6377  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
6378 

Field Documentation

◆ ctx

ctx

Definition at line 6301 of file z3py.py.

Referenced by Probe.__call__(), Solver.__copy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Statistics.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Statistics.__len__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Statistics.__repr__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), UserPropagateBase.ctx_ref(), Solver.dimacs(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Statistics.get_key_value(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Statistics.keys(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), Solver.num_scopes(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.pop(), Optimize.pop(), Solver.proof(), Solver.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Solver.reset(), Solver.set(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().

◆ stats

stats
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10582
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.
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
Z3_stats_is_uint
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
z3py.UserPropagateBase.__del__
def __del__(self)
Definition: z3py.py:10607
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_size
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_stats_to_string
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
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.
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.
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.