Z3: 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 5453 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(	self,
		stats,
		ctx
	)

Definition at line 5456 of file z3py.py.

 
     def __init__(self, stats, ctx):
         self.stats = stats
         self.ctx   = ctx
         Z3_stats_inc_ref(self.ctx.ref(), self.stats)

def __del__ ( self )

Definition at line 5461 of file z3py.py.

 
     def __del__(self):
         Z3_stats_dec_ref(self.ctx.ref(), self.stats)

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']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2

Definition at line 5554 of file z3py.py.

 
     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']
         >>> st.nlsat_propagations
         2
         >>> st.nlsat_stages
         2
         """
         key = name.replace('_', ' ')
         try:
             return self.get_key_value(key)
         except Z3Exception:
             raise AttributeError

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)
2
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)

Definition at line 5496 of file z3py.py.

 
     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)
         2
         >>> st[0]
         ('nlsat propagations', 2)
         >>> st[1]
         ('nlsat stages', 2)
         """
         if idx >= len(self):
             raise IndexError
         if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
             val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
         else:
             val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
         return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)

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)
2

Definition at line 5482 of file z3py.py.

 
     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)
         2
         """
         return int(Z3_stats_size(self.ctx.ref(), self.stats))

def __repr__ ( self )

Definition at line 5464 of file z3py.py.

 
     def __repr__(self):
         if in_html_mode():
             out = io.StringIO()
             even = True
             out.write(u'<table border="1" cellpadding="2" cellspacing="0">')
             for k, v in self:
                 if even:
                     out.write(u'<tr style="background-color:#CFCFCF">')
                     even = False
                 else:
                     out.write(u'<tr>')
                     even = True
                 out.write(u'<td>%s</td><td>%s</td></tr>' % (k, v))
             out.write(u'</table>')
             return out.getvalue()
         else:
             return Z3_stats_to_string(self.ctx.ref(), self.stats)

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

Referenced by Statistics.__getattr__().

 
     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
         """
         for idx in range(len(self)):
             if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
                 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
                     return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
                 else:
                     return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
         raise Z3Exception("unknown key")

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']

Definition at line 5520 of file z3py.py.

 
     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']
         """
         return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation