|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| None | _siftdown (list[_Elem] heap, int startpos, int pos) |
| None | _siftup (list[_Elem] heap, int pos) |
| None | heapify (list[_Elem] heap) |
| None | heappush (list[_Elem] heap, _Elem item) |
| _Elem | heappop (list[_Elem] heap) |
| _Elem | heapreplace (list[_Elem] heap, _Elem item) |
| _Elem | heappushpop (list[_Elem] heap, _Elem item) |
Variables | |
| _Elem = int | |
Move heap[pos] toward startpos until its parent is no larger.
Bubble the smaller child up to heap[pos], then sift the oddball down.
| None heapq.heapify | ( | list[_Elem] | heap | ) |
Transform the list into a heap, in-place.
Pop and return the smallest item, maintaining the heap invariant.
Push item onto the heap, maintaining the heap invariant.
Push item on the heap, then pop and return the smallest item.
Pop and return the smallest item, then push item; heap size is unchanged.
|
protected |