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 | |
__init__ | ( | self, | |
stats, | |||
ctx ) |
Definition at line 6832 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 6840 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__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 6932 of file z3py.py.
__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 6876 of file z3py.py.
__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 6862 of file z3py.py.
__repr__ | ( | self | ) |
Definition at line 6844 of file z3py.py.
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 6912 of file z3py.py.
Referenced by __getattr__().
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 6900 of file z3py.py.
ctx = ctx |
Definition at line 6834 of file z3py.py.
Referenced by __deepcopy__(), Solver.__del__(), __del__(), __getitem__(), __len__(), __repr__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), get_key_value(), keys(), Solver.model(), Solver.num_scopes(), Solver.pop(), Solver.push(), Solver.reset(), and Solver.set().
stats = stats |
Definition at line 6833 of file z3py.py.
Referenced by __deepcopy__(), __del__(), __getitem__(), __len__(), __repr__(), get_key_value(), and keys().