Z3
Public Member Functions | Data Fields
Statistics Class Reference

Statistics. More...

Public Member Functions

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

Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 6761 of file z3py.py.

6761  def __init__(self, stats, ctx):
6762  self.stats = stats
6763  self.ctx = ctx
6764  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
6765 
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:6761
def __del__ (   self)

Definition at line 6769 of file z3py.py.

6769  def __del__(self):
6770  if self.ctx.ref() is not None and Z3_stats_dec_ref is not None:
6771  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
6772 
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:6769

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6766 of file z3py.py.

6766  def __deepcopy__(self, memo={}):
6767  return Statistics(self.stats, self.ctx)
6768 
def __deepcopy__
Definition: z3py.py:6766
Statistics.
Definition: z3py.py:6758
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 6861 of file z3py.py.

6861  def __getattr__(self, name):
6862  """Access the value of statistical using attributes.
6863 
6864  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
6865  we should use '_' (e.g., 'nlsat_propagations').
6866 
6867  >>> x = Int('x')
6868  >>> s = Then('simplify', 'nlsat').solver()
6869  >>> s.add(x > 0)
6870  >>> s.check()
6871  sat
6872  >>> st = s.statistics()
6873  >>> st.nlsat_propagations
6874  2
6875  >>> st.nlsat_stages
6876  2
6877  """
6878  key = name.replace("_", " ")
6879  try:
6880  return self.get_key_value(key)
6881  except Z3Exception:
6882  raise AttributeError
6883 
def __getattr__(self, name)
Definition: z3py.py:6861
def get_key_value(self, key)
Definition: z3py.py:6841
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 6805 of file z3py.py.

6805  def __getitem__(self, idx):
6806  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
6807 
6808  >>> x = Int('x')
6809  >>> s = Then('simplify', 'nlsat').solver()
6810  >>> s.add(x > 0)
6811  >>> s.check()
6812  sat
6813  >>> st = s.statistics()
6814  >>> len(st)
6815  6
6816  >>> st[0]
6817  ('nlsat propagations', 2)
6818  >>> st[1]
6819  ('nlsat stages', 2)
6820  """
6821  if idx >= len(self):
6822  raise IndexError
6823  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6824  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6825  else:
6826  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6827  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
6828 
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.
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.
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:6805
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 6791 of file z3py.py.

6791  def __len__(self):
6792  """Return the number of statistical counters.
6793 
6794  >>> x = Int('x')
6795  >>> s = Then('simplify', 'nlsat').solver()
6796  >>> s.add(x > 0)
6797  >>> s.check()
6798  sat
6799  >>> st = s.statistics()
6800  >>> len(st)
6801  6
6802  """
6803  return int(Z3_stats_size(self.ctx.ref(), self.stats))
6804 
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:6791
def __repr__ (   self)

Definition at line 6773 of file z3py.py.

6773  def __repr__(self):
6774  if in_html_mode():
6775  out = io.StringIO()
6776  even = True
6777  out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
6778  for k, v in self:
6779  if even:
6780  out.write(u('<tr style="background-color:#CFCFCF">'))
6781  even = False
6782  else:
6783  out.write(u("<tr>"))
6784  even = True
6785  out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
6786  out.write(u("</table>"))
6787  return out.getvalue()
6788  else:
6789  return Z3_stats_to_string(self.ctx.ref(), self.stats)
6790 
def __repr__(self)
Definition: z3py.py:6773
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 6841 of file z3py.py.

Referenced by Statistics.__getattr__().

6841  def get_key_value(self, key):
6842  """Return the value of a particular statistical counter.
6843 
6844  >>> x = Int('x')
6845  >>> s = Then('simplify', 'nlsat').solver()
6846  >>> s.add(x > 0)
6847  >>> s.check()
6848  sat
6849  >>> st = s.statistics()
6850  >>> st.get_key_value('nlsat propagations')
6851  2
6852  """
6853  for idx in range(len(self)):
6854  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
6855  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6856  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6857  else:
6858  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6859  raise Z3Exception("unknown key")
6860 
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.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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:6841
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()

Definition at line 6829 of file z3py.py.

6829  def keys(self):
6830  """Return the list of statistical counters.
6831 
6832  >>> x = Int('x')
6833  >>> s = Then('simplify', 'nlsat').solver()
6834  >>> s.add(x > 0)
6835  >>> s.check()
6836  sat
6837  >>> st = s.statistics()
6838  """
6839  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
6840 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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:6829

Field Documentation

ctx

Definition at line 6763 of file z3py.py.

Referenced by Solver.__copy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), 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(), Solver.consequences(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.model(), Optimize.model(), Solver.next(), Solver.non_units(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Fixedpoint.query(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.trail(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().

stats