|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
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 | |
| def __init__ | ( | self, | |
| stats, | |||
| ctx | |||
| ) |
| def __del__ | ( | self | ) |
| 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.
05705 05706 def __getattr__(self, name): 05707 """Access the value of statistical using attributes. 05708 05709 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'), 05710 we should use '_' (e.g., 'nlsat_propagations'). 05711 05712 >>> x = Int('x') 05713 >>> s = Then('simplify', 'nlsat').solver() 05714 >>> s.add(x > 0) 05715 >>> s.check() 05716 sat 05717 >>> st = s.statistics() 05718 >>> st.keys() 05719 ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] 05720 >>> st.nlsat_propagations 05721 2 05722 >>> st.nlsat_stages 05723 2 05724 """ 05725 key = name.replace('_', ' ') 05726 try: 05727 return self.get_key_value(key) 05728 except Z3Exception: 05729 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)
6
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)
Definition at line 5647 of file z3py.py.
05647 05648 def __getitem__(self, idx): 05649 """Return the value of statistical counter at position `idx`. The result is a pair (key, value). 05650 05651 >>> x = Int('x') 05652 >>> s = Then('simplify', 'nlsat').solver() 05653 >>> s.add(x > 0) 05654 >>> s.check() 05655 sat 05656 >>> st = s.statistics() 05657 >>> len(st) 05658 6 05659 >>> st[0] 05660 ('nlsat propagations', 2) 05661 >>> st[1] 05662 ('nlsat stages', 2) 05663 """ 05664 if idx >= len(self): 05665 raise IndexError 05666 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 05667 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 05668 else: 05669 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 05670 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)
6
Definition at line 5633 of file z3py.py.
05633 05634 def __len__(self): 05635 """Return the number of statistical counters. 05636 05637 >>> x = Int('x') 05638 >>> s = Then('simplify', 'nlsat').solver() 05639 >>> s.add(x > 0) 05640 >>> s.check() 05641 sat 05642 >>> st = s.statistics() 05643 >>> len(st) 05644 6 05645 """ 05646 return int(Z3_stats_size(self.ctx.ref(), self.stats))
| def __repr__ | ( | self | ) |
Definition at line 5615 of file z3py.py.
05615 05616 def __repr__(self): 05617 if in_html_mode(): 05618 out = io.StringIO() 05619 even = True 05620 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 05621 for k, v in self: 05622 if even: 05623 out.write(u('<tr style="background-color:#CFCFCF">')) 05624 even = False 05625 else: 05626 out.write(u('<tr>')) 05627 even = True 05628 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 05629 out.write(u('</table>')) 05630 return out.getvalue() 05631 else: 05632 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 5685 of file z3py.py.
Referenced by Statistics.__getattr__().
05685 05686 def get_key_value(self, key): 05687 """Return the value of a particular statistical counter. 05688 05689 >>> x = Int('x') 05690 >>> s = Then('simplify', 'nlsat').solver() 05691 >>> s.add(x > 0) 05692 >>> s.check() 05693 sat 05694 >>> st = s.statistics() 05695 >>> st.get_key_value('nlsat propagations') 05696 2 05697 """ 05698 for idx in range(len(self)): 05699 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 05700 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 05701 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 05702 else: 05703 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 05704 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', 'rlimit count', 'max memory', 'memory', 'num allocs']
Definition at line 5671 of file z3py.py.
05671 05672 def keys(self): 05673 """Return the list of statistical counters. 05674 05675 >>> x = Int('x') 05676 >>> s = Then('simplify', 'nlsat').solver() 05677 >>> s.add(x > 0) 05678 >>> s.check() 05679 sat 05680 >>> st = s.statistics() 05681 >>> st.keys() 05682 ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] 05683 """ 05684 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
Definition at line 5607 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), ArrayRef.mk_default(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 5607 of file z3py.py.
Referenced by Statistics::__del__(), Statistics::__getitem__(), Statistics::__len__(), Statistics::__repr__(), Statistics::get_key_value(), and Statistics::keys().
1.7.6.1