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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
stats,
ctx )

Definition at line 6795 of file z3py.py.

6795 def __init__(self, stats, ctx):
6796 self.stats = stats
6797 self.ctx = ctx
6798 Z3_stats_inc_ref(self.ctx.ref(), self.stats)
6799
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 6803 of file z3py.py.

6803 def __del__(self):
6804 if self.ctx.ref() is not None and Z3_stats_dec_ref is not None:
6805 Z3_stats_dec_ref(self.ctx.ref(), self.stats)
6806
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 6800 of file z3py.py.

6800 def __deepcopy__(self, memo={}):
6801 return Statistics(self.stats, self.ctx)
6802

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

6895 def __getattr__(self, name):
6896 """Access the value of statistical using attributes.
6897
6898 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
6899 we should use '_' (e.g., 'nlsat_propagations').
6900
6901 >>> x = Int('x')
6902 >>> s = Then('simplify', 'nlsat').solver()
6903 >>> s.add(x > 0)
6904 >>> s.check()
6905 sat
6906 >>> st = s.statistics()
6907 >>> st.nlsat_propagations
6908 2
6909 >>> st.nlsat_stages
6910 2
6911 """
6912 key = name.replace("_", " ")
6913 try:
6914 return self.get_key_value(key)
6915 except Z3Exception:
6916 raise AttributeError
6917

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

6839 def __getitem__(self, idx):
6840 """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
6841
6842 >>> x = Int('x')
6843 >>> s = Then('simplify', 'nlsat').solver()
6844 >>> s.add(x > 0)
6845 >>> s.check()
6846 sat
6847 >>> st = s.statistics()
6848 >>> len(st)
6849 7
6850 >>> st[0]
6851 ('nlsat propagations', 2)
6852 >>> st[1]
6853 ('nlsat restarts', 1)
6854 """
6855 if idx >= len(self):
6856 raise IndexError
6857 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6858 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6859 else:
6860 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6861 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
6862
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 6825 of file z3py.py.

6825 def __len__(self):
6826 """Return the number of statistical counters.
6827
6828 >>> x = Int('x')
6829 >>> s = Then('simplify', 'nlsat').solver()
6830 >>> s.add(x > 0)
6831 >>> s.check()
6832 sat
6833 >>> st = s.statistics()
6834 >>> len(st)
6835 7
6836 """
6837 return int(Z3_stats_size(self.ctx.ref(), self.stats))
6838
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.

Referenced by AstVector.__getitem__(), and AstVector.__setitem__().

◆ __repr__()

__repr__ ( self)

Definition at line 6807 of file z3py.py.

6807 def __repr__(self):
6808 if in_html_mode():
6809 out = io.StringIO()
6810 even = True
6811 out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
6812 for k, v in self:
6813 if even:
6814 out.write(u('<tr style="background-color:#CFCFCF">'))
6815 even = False
6816 else:
6817 out.write(u("<tr>"))
6818 even = True
6819 out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
6820 out.write(u("</table>"))
6821 return out.getvalue()
6822 else:
6823 return Z3_stats_to_string(self.ctx.ref(), self.stats)
6824
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 6875 of file z3py.py.

6875 def get_key_value(self, key):
6876 """Return the value of a particular statistical counter.
6877
6878 >>> x = Int('x')
6879 >>> s = Then('simplify', 'nlsat').solver()
6880 >>> s.add(x > 0)
6881 >>> s.check()
6882 sat
6883 >>> st = s.statistics()
6884 >>> st.get_key_value('nlsat propagations')
6885 2
6886 """
6887 for idx in range(len(self)):
6888 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
6889 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6890 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6891 else:
6892 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6893 raise Z3Exception("unknown key")
6894

Referenced by Statistics.__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 6863 of file z3py.py.

6863 def keys(self):
6864 """Return the list of statistical counters.
6865
6866 >>> x = Int('x')
6867 >>> s = Then('simplify', 'nlsat').solver()
6868 >>> s.add(x > 0)
6869 >>> s.check()
6870 sat
6871 >>> st = s.statistics()
6872 """
6873 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
6874

Field Documentation

◆ ctx

ctx = ctx

Definition at line 6797 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ stats