Module priority_queue 

Priority Queue for Propagations.

Manages propagation priorities across multiple theories, ensuring efficient propagation order for conflict-driven theory combination.

Priority Levels

• Boolean (0): Highest priority - unit propagation
• Equality (1): Shared term equalities
• Theory (2-10): Per-theory propagations
• Heuristic (11+): Low-priority optional propagations

References

• Z3’s smt/smt_context.cpp propagation queue

Structs

PriorityQueueConfig

Configuration for priority queue.

PriorityQueueStats

Statistics for priority queue.

Propagation

A propagation entry in the queue.

PropagationQueue

Priority queue for propagations.

Enums

PropagationType

Type of propagation.

Type Aliases

Priority

Priority level (lower = higher priority).

PropagationId

Propagation ID.