A max-heap of ids into caller-owned storage. More...

#include <SATSolver.h>

Collaboration diagram for circt::IndexedMaxHeap< T, ScoreFn >:

[legend]

Public Member Functions
	IndexedMaxHeap (llvm::SmallVectorImpl< T > &storage)

void	resize (unsigned size)

bool	empty () const

bool	contains (unsigned id) const

void	clear ()
	Remove all heap entries while keeping the underlying storage untouched.

void	insert (unsigned id)
	Insert `id` if it is not already present.

void	increase (unsigned id)
	Restore heap order after the score for an existing `id` increased.

unsigned	pop ()
	Remove and return the highest-scoring id.

Private Member Functions
double	score (unsigned id) const
	Compute the ordering score for one heap entry.

void	swapHeapEntries (unsigned lhs, unsigned rhs)
	Swap two heap slots and keep the reverse index in sync.

void	siftUp (unsigned index)
	Bubble one entry toward the root until the heap property is restored.

void	siftDown (unsigned index)
	Push one entry toward the leaves until the heap property is restored.

Private Attributes
llvm::SmallVectorImpl< T > &	storage
	The caller-owned objects indexed by heap ids.

llvm::SmallVector< unsigned, 0 >	heap
	Binary heap of ids ordered by descending score.

llvm::SmallVector< unsigned, 0 >	positions
	Reverse map from id to heap slot, or `InvalidIndex` if absent.

Static Private Attributes
static constexpr unsigned	kInvalidIndex = ~0u

Detailed Description

template<typename T, typename ScoreFn = HeapScore<T>>
class circt::IndexedMaxHeap< T, ScoreFn >

A max-heap of ids into caller-owned storage.

The heap stores only integer ids and keeps a reverse map from each id to its heap slot. That lets callers update an existing entry without creating duplicates. Scores come from a stateless policy type. If a caller changes an element in storage in a way that raises its score, it must call increase(id) to restore heap order.

This data structure design is inspired by MiniSat's minisat/mtl/Heap.h.

Definition at line 33 of file SATSolver.h.

Constructor & Destructor Documentation

◆ IndexedMaxHeap()

template<typename T , typename ScoreFn = HeapScore<T>>

circt::IndexedMaxHeap< T, ScoreFn >::IndexedMaxHeap ( llvm::SmallVectorImpl< T > & storage )

inlineexplicit

Definition at line 37 of file SATSolver.h.

Member Function Documentation

◆ clear()

template<typename T , typename ScoreFn = HeapScore<T>>

void circt::IndexedMaxHeap< T, ScoreFn >::clear ( )

inline

Remove all heap entries while keeping the underlying storage untouched.

Definition at line 52 of file SATSolver.h.

References circt::IndexedMaxHeap< T, ScoreFn >::heap, circt::IndexedMaxHeap< T, ScoreFn >::kInvalidIndex, and circt::IndexedMaxHeap< T, ScoreFn >::positions.

◆ contains()

template<typename T , typename ScoreFn = HeapScore<T>>

bool circt::IndexedMaxHeap< T, ScoreFn >::contains ( unsigned id ) const

inline

Definition at line 47 of file SATSolver.h.

References circt::IndexedMaxHeap< T, ScoreFn >::kInvalidIndex, and circt::IndexedMaxHeap< T, ScoreFn >::positions.

Referenced by circt::IndexedMaxHeap< T, ScoreFn >::increase(), and circt::IndexedMaxHeap< T, ScoreFn >::insert().

◆ empty()

template<typename T , typename ScoreFn = HeapScore<T>>

bool circt::IndexedMaxHeap< T, ScoreFn >::empty ( ) const

inline

Definition at line 45 of file SATSolver.h.

References circt::IndexedMaxHeap< T, ScoreFn >::heap.

Referenced by circt::IndexedMaxHeap< T, ScoreFn >::pop().

◆ increase()

template<typename T , typename ScoreFn = HeapScore<T>>

void circt::IndexedMaxHeap< T, ScoreFn >::increase ( unsigned id )

inline

Restore heap order after the score for an existing id increased.

This only moves the entry upward. Callers should use this when the score policy is monotonic in the "better" direction, such as SAT variable activity bumps. Mutating a stored element without calling increase(id) leaves the heap order stale.

Definition at line 76 of file SATSolver.h.

References circt::IndexedMaxHeap< T, ScoreFn >::contains(), circt::IndexedMaxHeap< T, ScoreFn >::positions, and circt::IndexedMaxHeap< T, ScoreFn >::siftUp().