Statistics Class Reference

Statistics. More...

Public Member Functions
def	__init__ (self, stats, ctx)
def	__deepcopy__ (self, memo={})
def	__del__ (self)
def	__repr__ (self)
def	__len__ (self)
def	__getitem__ (self, idx)
def	keys (self)
def	get_key_value (self, key)
def	__getattr__ (self, name)

Data Fields
	stats
	ctx

Detailed Description

Statistics.

Statistics for `Solver.check()`.

Definition at line 6602 of file z3py.py.

Constructor & Destructor Documentation

__init__()

def __init__	(		self,
			stats,
			ctx
	)

Definition at line 6605 of file z3py.py.

    def __init__(self, stats, ctx):
        self.stats = stats
        self.ctx = ctx
        Z3_stats_inc_ref(self.ctx.ref(), self.stats)
 

__del__()

def __del__

(

self

)

Definition at line 6613 of file z3py.py.

    def __del__(self):
        if self.ctx.ref() is not None:
            Z3_stats_dec_ref(self.ctx.ref(), self.stats)
 

Member Function Documentation

__deepcopy__()

def __deepcopy__	(		self,
			memo = {}
	)

Definition at line 6610 of file z3py.py.

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

__getattr__()

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.nlsat_propagations
2
>>> st.nlsat_stages
2

Definition at line 6705 of file z3py.py.

    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.nlsat_propagations
        2
        >>> st.nlsat_stages
        2
        """
        key = name.replace("_", " ")
        try:
            return self.get_key_value(key)
        except Z3Exception:
            raise AttributeError
 

__getitem__()

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

    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)
        """
        if idx >= len(self):
            raise IndexError
        if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
            val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
        else:
            val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
        return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
 

__len__()

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

    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
        """
        return int(Z3_stats_size(self.ctx.ref(), self.stats))
 

__repr__()

def __repr__

(

self

)

Definition at line 6617 of file z3py.py.

    def __repr__(self):
        if in_html_mode():
            out = io.StringIO()
            even = True
            out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
            for k, v in self:
                if even:
                    out.write(u('<tr style="background-color:#CFCFCF">'))
                    even = False
                else:
                    out.write(u("<tr>"))
                    even = True
                out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
            out.write(u("</table>"))
            return out.getvalue()
        else:
            return Z3_stats_to_string(self.ctx.ref(), self.stats)
 

get_key_value()

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

    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
        """
        for idx in range(len(self)):
            if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
                if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
                    return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
                else:
                    return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
        raise Z3Exception("unknown key")
 

Referenced by Statistics.__getattr__().

keys()

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

Definition at line 6673 of file z3py.py.

    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()
        """
        return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
 

Field Documentation

ctx

ctx

Definition at line 6607 of file z3py.py.

Referenced by Probe.__call__(), Solver.__copy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Statistics.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Statistics.__len__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Statistics.__repr__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), UserPropagateBase.ctx_ref(), Solver.dimacs(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Statistics.get_key_value(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Statistics.keys(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), Solver.num_scopes(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Optimize.pop(), Solver.pop(), Solver.proof(), Solver.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Solver.reset(), Solver.set(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().

stats

stats

Definition at line 6606 of file z3py.py.

Referenced by Statistics.__deepcopy__(), Statistics.__del__(), Statistics.__getitem__(), Statistics.__len__(), Statistics.__repr__(), Statistics.get_key_value(), and Statistics.keys().