Statistics.
Statistics for `Solver.check()`.
Definition at line 5604 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', 'rlimit count', 'max memory', 'memory', 'num allocs']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2
Definition at line 5705 of file z3py.py.
5706 """Access the value of statistical using attributes. 5708 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'), 5709 we should use '_' (e.g., 'nlsat_propagations'). 5712 >>> s = Then('simplify', 'nlsat').solver() 5716 >>> st = s.statistics() 5718 ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] 5719 >>> st.nlsat_propagations 5724 key = name.replace(
'_',
' ')
5728 raise AttributeError
def __getattr__(self, name)
def get_key_value(self, key)
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.
5672 """Return the list of statistical counters. 5675 >>> s = Then('simplify', 'nlsat').solver() 5679 >>> st = s.statistics() 5681 ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] 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.