Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
Statistics Class Reference

Statistics. More...

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

Detailed Description

Statistics.

Statistics for `Solver.check()`.

Definition at line 5544 of file z3py.py.


Constructor & Destructor Documentation

def __init__ (   self,
  stats,
  ctx 
)

Definition at line 5547 of file z3py.py.

05547 
05548     def __init__(self, stats, ctx):
05549         self.stats = stats
05550         self.ctx   = ctx
05551         Z3_stats_inc_ref(self.ctx.ref(), self.stats)

def __del__ (   self)

Definition at line 5552 of file z3py.py.

05552 
05553     def __del__(self):
05554         Z3_stats_dec_ref(self.ctx.ref(), self.stats)


Member Function Documentation

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


Field Documentation

ctx

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().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines