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'] >>> st.nlsat_propagations 2 >>> st.nlsat_stages 2
Definition at line 5645 of file z3py.py.
05645 05646 def __getattr__(self, name): 05647 """Access the value of statistical using attributes. 05648 05649 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'), 05650 we should use '_' (e.g., 'nlsat_propagations'). 05651 05652 >>> x = Int('x') 05653 >>> s = Then('simplify', 'nlsat').solver() 05654 >>> s.add(x > 0) 05655 >>> s.check() 05656 sat 05657 >>> st = s.statistics() 05658 >>> st.keys() 05659 ['nlsat propagations', 'nlsat stages'] 05660 >>> st.nlsat_propagations 05661 2 05662 >>> st.nlsat_stages 05663 2 05664 """ 05665 key = name.replace('_', ' ') 05666 try: 05667 return self.get_key_value(key) 05668 except Z3Exception: 05669 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) 2 >>> st[0] ('nlsat propagations', 2) >>> st[1] ('nlsat stages', 2)
Definition at line 5587 of file z3py.py.
05587 05588 def __getitem__(self, idx): 05589 """Return the value of statistical counter at position `idx`. The result is a pair (key, value). 05590 05591 >>> x = Int('x') 05592 >>> s = Then('simplify', 'nlsat').solver() 05593 >>> s.add(x > 0) 05594 >>> s.check() 05595 sat 05596 >>> st = s.statistics() 05597 >>> len(st) 05598 2 05599 >>> st[0] 05600 ('nlsat propagations', 2) 05601 >>> st[1] 05602 ('nlsat stages', 2) 05603 """ 05604 if idx >= len(self): 05605 raise IndexError 05606 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 05607 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 05608 else: 05609 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 05610 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) 2
Definition at line 5573 of file z3py.py.
05573 05574 def __len__(self): 05575 """Return the number of statistical counters. 05576 05577 >>> x = Int('x') 05578 >>> s = Then('simplify', 'nlsat').solver() 05579 >>> s.add(x > 0) 05580 >>> s.check() 05581 sat 05582 >>> st = s.statistics() 05583 >>> len(st) 05584 2 05585 """ 05586 return int(Z3_stats_size(self.ctx.ref(), self.stats))
def __repr__ | ( | self | ) |
Definition at line 5555 of file z3py.py.
05555 05556 def __repr__(self): 05557 if in_html_mode(): 05558 out = io.StringIO() 05559 even = True 05560 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 05561 for k, v in self: 05562 if even: 05563 out.write(u('<tr style="background-color:#CFCFCF">')) 05564 even = False 05565 else: 05566 out.write(u('<tr>')) 05567 even = True 05568 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 05569 out.write(u('</table>')) 05570 return out.getvalue() 05571 else: 05572 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 5625 of file z3py.py.
Referenced by Statistics.__getattr__().
05625 05626 def get_key_value(self, key): 05627 """Return the value of a particular statistical counter. 05628 05629 >>> x = Int('x') 05630 >>> s = Then('simplify', 'nlsat').solver() 05631 >>> s.add(x > 0) 05632 >>> s.check() 05633 sat 05634 >>> st = s.statistics() 05635 >>> st.get_key_value('nlsat propagations') 05636 2 05637 """ 05638 for idx in range(len(self)): 05639 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 05640 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 05641 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 05642 else: 05643 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 05644 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']
Definition at line 5611 of file z3py.py.
05611 05612 def keys(self): 05613 """Return the list of statistical counters. 05614 05615 >>> x = Int('x') 05616 >>> s = Then('simplify', 'nlsat').solver() 05617 >>> s.add(x > 0) 05618 >>> s.check() 05619 sat 05620 >>> st = s.statistics() 05621 >>> st.keys() 05622 ['nlsat propagations', 'nlsat stages'] 05623 """ 05624 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
Definition at line 5547 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(), 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(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 5547 of file z3py.py.
Referenced by Statistics::__del__(), Statistics::__getitem__(), Statistics::__len__(), Statistics::__repr__(), Statistics::get_key_value(), and Statistics::keys().