Z3
 
Loading...
Searching...
No Matches
Statistics Class Reference

Statistics. More...

Public Member Functions

 __init__ (self, stats, ctx)
 
 __deepcopy__ (self, memo={})
 
 __del__ (self)
 
 __repr__ (self)
 
 __len__ (self)
 
 __getitem__ (self, idx)
 
 keys (self)
 
 get_key_value (self, key)
 
 __getattr__ (self, name)
 

Data Fields

 stats = stats
 
 ctx = ctx
 

Detailed Description

Statistics.

Statistics for `Solver.check()`.

Definition at line 6820 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
stats,
ctx )

Definition at line 6823 of file z3py.py.

6823 def __init__(self, stats, ctx):
6824 self.stats = stats
6825 self.ctx = ctx
6826 Z3_stats_inc_ref(self.ctx.ref(), self.stats)
6827
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.

◆ __del__()

__del__ ( self)

Definition at line 6831 of file z3py.py.

6831 def __del__(self):
6832 if self.ctx.ref() is not None and Z3_stats_dec_ref is not None:
6833 Z3_stats_dec_ref(self.ctx.ref(), self.stats)
6834
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

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6828 of file z3py.py.

6828 def __deepcopy__(self, memo={}):
6829 return Statistics(self.stats, self.ctx)
6830

◆ __getattr__()

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

6923 def __getattr__(self, name):
6924 """Access the value of statistical using attributes.
6925
6926 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
6927 we should use '_' (e.g., 'nlsat_propagations').
6928
6929 >>> x = Int('x')
6930 >>> s = Then('simplify', 'nlsat').solver()
6931 >>> s.add(x > 0)
6932 >>> s.check()
6933 sat
6934 >>> st = s.statistics()
6935 >>> st.nlsat_propagations
6936 2
6937 >>> st.nlsat_stages
6938 2
6939 """
6940 key = name.replace("_", " ")
6941 try:
6942 return self.get_key_value(key)
6943 except Z3Exception:
6944 raise AttributeError
6945

◆ __getitem__()

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

Definition at line 6867 of file z3py.py.

6867 def __getitem__(self, idx):
6868 """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
6869
6870 >>> x = Int('x')
6871 >>> s = Then('simplify', 'nlsat').solver()
6872 >>> s.add(x > 0)
6873 >>> s.check()
6874 sat
6875 >>> st = s.statistics()
6876 >>> len(st)
6877 7
6878 >>> st[0]
6879 ('nlsat propagations', 2)
6880 >>> st[1]
6881 ('nlsat restarts', 1)
6882 """
6883 if idx >= len(self):
6884 raise IndexError
6885 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6886 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6887 else:
6888 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6889 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
6890
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.
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.
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.

◆ __len__()

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

Definition at line 6853 of file z3py.py.

6853 def __len__(self):
6854 """Return the number of statistical counters.
6855
6856 >>> x = Int('x')
6857 >>> s = Then('simplify', 'nlsat').solver()
6858 >>> s.add(x > 0)
6859 >>> s.check()
6860 sat
6861 >>> st = s.statistics()
6862 >>> len(st)
6863 7
6864 """
6865 return int(Z3_stats_size(self.ctx.ref(), self.stats))
6866
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.

◆ __repr__()

__repr__ ( self)

Definition at line 6835 of file z3py.py.

6835 def __repr__(self):
6836 if in_html_mode():
6837 out = io.StringIO()
6838 even = True
6839 out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
6840 for k, v in self:
6841 if even:
6842 out.write(u('<tr style="background-color:#CFCFCF">'))
6843 even = False
6844 else:
6845 out.write(u("<tr>"))
6846 even = True
6847 out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
6848 out.write(u("</table>"))
6849 return out.getvalue()
6850 else:
6851 return Z3_stats_to_string(self.ctx.ref(), self.stats)
6852
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.

◆ get_key_value()

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

6903 def get_key_value(self, key):
6904 """Return the value of a particular statistical counter.
6905
6906 >>> x = Int('x')
6907 >>> s = Then('simplify', 'nlsat').solver()
6908 >>> s.add(x > 0)
6909 >>> s.check()
6910 sat
6911 >>> st = s.statistics()
6912 >>> st.get_key_value('nlsat propagations')
6913 2
6914 """
6915 for idx in range(len(self)):
6916 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
6917 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6918 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6919 else:
6920 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6921 raise Z3Exception("unknown key")
6922

Referenced by __getattr__().

◆ keys()

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

6891 def keys(self):
6892 """Return the list of statistical counters.
6893
6894 >>> x = Int('x')
6895 >>> s = Then('simplify', 'nlsat').solver()
6896 >>> s.add(x > 0)
6897 >>> s.check()
6898 sat
6899 >>> st = s.statistics()
6900 """
6901 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
6902

Field Documentation

◆ ctx

◆ stats

stats = stats

Definition at line 6824 of file z3py.py.

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