collections.Counter Class Reference

Public Member Functions
None	__init__ (self)
int	__getitem__ (self, tuple[int, int] key)
None	__setitem__ (self, tuple[int, int] key, int value)
list[int]	values (self)
bool	__bool__ (self)
list[tuple[int, int]]	most_common (self, int n=1)

Public Attributes
dict[tuple[int, int], int]	data
int	count = 0

Detailed Description

Simplified Counter model: maps (int, int) keys to integer counts.

Constructor & Destructor Documentation

__init__()

None collections.Counter.__init__

(

self

)

Initialize an empty counter with no recorded keys.

Member Function Documentation

__bool__()

bool collections.Counter.__bool__

(

self

)

Return True iff at least one key has been recorded.

__getitem__()

int collections.Counter.__getitem__	(		self,
		tuple[int, int]	key )

Return the count for *key*, or 0 if *key* has not been recorded.

__setitem__()

None collections.Counter.__setitem__	(		self,
		tuple[int, int]	key,
		int	value )

Set the count for *key*, tracking unique-key arrivals via ``count``.

most_common()

list[tuple[int, int]] collections.Counter.most_common	(		self,
		int	n = 1 )

Counter.most_common is not modelled — reject with a clear assertion.

CPython returns up to ``n`` ``(elem, count)`` pairs sorted by
count descending. ESBMC's Counter model does not track which key
maps to which count, so the CPython contract cannot be honoured.
Rather than silently returning a lossy approximation (which
caused issue #4665 by misleading callers that wrote
``c.most_common(n)[i][j]``), this method fires a verification
assertion as soon as it is reached. Programs that need counts
without keys should iterate ``Counter.data`` directly.

The return type ``list[tuple[int, int]]`` is kept matching
CPython's API surface so the frontend can type-check
subscript-of-subscript expressions cleanly before the assertion
fires — otherwise callers see the cryptic "Unsupported
comparison with unresolved operand type" frontend error
instead of the assertion message.

values()

list[int] collections.Counter.values

(

self

)

Return all recorded counts.

Member Data Documentation

count

int collections.Counter.count = 0

data

dict[tuple[int, int], int] collections.Counter.data

---

The documentation for this class was generated from the following file:

• src/python-frontend/models/collections.py