oxiz_solver/propagation/
priority_queue.rs

1//! Priority Queue for Propagations.
2//!
3//! Manages propagation priorities across multiple theories, ensuring
4//! efficient propagation order for conflict-driven theory combination.
5//!
6//! ## Priority Levels
7//!
8//! - **Boolean (0)**: Highest priority - unit propagation
9//! - **Equality (1)**: Shared term equalities
10//! - **Theory (2-10)**: Per-theory propagations
11//! - **Heuristic (11+)**: Low-priority optional propagations
12//!
13//! ## References
14//!
15//! - Z3's `smt/smt_context.cpp` propagation queue
16
17use oxiz_sat::Lit;
18use rustc_hash::FxHashMap;
19use std::cmp::Ordering;
20use std::collections::BinaryHeap;
21
22/// Priority level (lower = higher priority).
23pub type Priority = u8;
24
25/// Propagation ID.
26pub type PropagationId = usize;
27
28/// Type of propagation.
29#[derive(Debug, Clone, Copy, PartialEq, Eq)]
30pub enum PropagationType {
31    /// Boolean unit propagation.
32    Boolean,
33    /// Equality propagation between theories.
34    Equality,
35    /// Theory-specific propagation.
36    Theory(u8),
37    /// Heuristic propagation (optional).
38    Heuristic,
39}
40
41impl PropagationType {
42    /// Get the priority level for this propagation type.
43    pub fn priority(&self) -> Priority {
44        match self {
45            PropagationType::Boolean => 0,
46            PropagationType::Equality => 1,
47            PropagationType::Theory(theory_id) => 2 + theory_id,
48            PropagationType::Heuristic => 255,
49        }
50    }
51}
52
53/// A propagation entry in the queue.
54#[derive(Debug, Clone)]
55pub struct Propagation {
56    /// Unique ID for this propagation.
57    pub id: PropagationId,
58    /// Type of propagation.
59    pub prop_type: PropagationType,
60    /// Priority (computed from type).
61    pub priority: Priority,
62    /// Literal being propagated (if Boolean).
63    pub literal: Option<Lit>,
64    /// Timestamp (for FIFO within same priority).
65    pub timestamp: u64,
66}
67
68impl PartialEq for Propagation {
69    fn eq(&self, other: &Self) -> bool {
70        self.id == other.id
71    }
72}
73
74impl Eq for Propagation {}
75
76impl PartialOrd for Propagation {
77    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
78        Some(self.cmp(other))
79    }
80}
81
82impl Ord for Propagation {
83    fn cmp(&self, other: &Self) -> Ordering {
84        // Reverse order for min-heap (lower priority value = higher priority)
85        // For timestamps, also reverse to get FIFO order (lower timestamp = earlier = higher priority)
86        other
87            .priority
88            .cmp(&self.priority)
89            .then_with(|| other.timestamp.cmp(&self.timestamp))
90    }
91}
92
93/// Configuration for priority queue.
94#[derive(Debug, Clone)]
95pub struct PriorityQueueConfig {
96    /// Enable timestamp ordering within same priority.
97    pub use_timestamps: bool,
98    /// Maximum queue size (0 = unlimited).
99    pub max_size: usize,
100}
101
102impl Default for PriorityQueueConfig {
103    fn default() -> Self {
104        Self {
105            use_timestamps: true,
106            max_size: 100_000,
107        }
108    }
109}
110
111/// Statistics for priority queue.
112#[derive(Debug, Clone, Default)]
113pub struct PriorityQueueStats {
114    /// Total propagations enqueued.
115    pub enqueued: u64,
116    /// Total propagations dequeued.
117    pub dequeued: u64,
118    /// Peak queue size.
119    pub peak_size: usize,
120    /// Propagations by type.
121    pub by_type: FxHashMap<u8, u64>,
122}
123
124/// Priority queue for propagations.
125#[derive(Debug)]
126pub struct PropagationQueue {
127    /// Binary heap (min-heap by priority).
128    heap: BinaryHeap<Propagation>,
129    /// Next propagation ID.
130    next_id: PropagationId,
131    /// Current timestamp (for FIFO within priority).
132    timestamp: u64,
133    /// Configuration.
134    config: PriorityQueueConfig,
135    /// Statistics.
136    stats: PriorityQueueStats,
137}
138
139impl PropagationQueue {
140    /// Create a new priority queue.
141    pub fn new(config: PriorityQueueConfig) -> Self {
142        Self {
143            heap: BinaryHeap::new(),
144            next_id: 0,
145            timestamp: 0,
146            config,
147            stats: PriorityQueueStats::default(),
148        }
149    }
150
151    /// Create with default configuration.
152    pub fn default_config() -> Self {
153        Self::new(PriorityQueueConfig::default())
154    }
155
156    /// Enqueue a propagation.
157    pub fn enqueue(&mut self, prop_type: PropagationType, literal: Option<Lit>) -> PropagationId {
158        let id = self.next_id;
159        self.next_id += 1;
160
161        let priority = prop_type.priority();
162        let timestamp = if self.config.use_timestamps {
163            let ts = self.timestamp;
164            self.timestamp += 1;
165            ts
166        } else {
167            0
168        };
169
170        let prop = Propagation {
171            id,
172            prop_type,
173            priority,
174            literal,
175            timestamp,
176        };
177
178        self.heap.push(prop);
179        self.stats.enqueued += 1;
180
181        // Update peak size
182        if self.heap.len() > self.stats.peak_size {
183            self.stats.peak_size = self.heap.len();
184        }
185
186        // Update by-type stats
187        *self.stats.by_type.entry(priority).or_insert(0) += 1;
188
189        id
190    }
191
192    /// Dequeue the highest-priority propagation.
193    pub fn dequeue(&mut self) -> Option<Propagation> {
194        let prop = self.heap.pop()?;
195        self.stats.dequeued += 1;
196        Some(prop)
197    }
198
199    /// Peek at the highest-priority propagation without removing it.
200    pub fn peek(&self) -> Option<&Propagation> {
201        self.heap.peek()
202    }
203
204    /// Check if queue is empty.
205    pub fn is_empty(&self) -> bool {
206        self.heap.is_empty()
207    }
208
209    /// Get current queue size.
210    pub fn len(&self) -> usize {
211        self.heap.len()
212    }
213
214    /// Clear all propagations.
215    pub fn clear(&mut self) {
216        self.heap.clear();
217        self.timestamp = 0;
218    }
219
220    /// Get statistics.
221    pub fn stats(&self) -> &PriorityQueueStats {
222        &self.stats
223    }
224
225    /// Reset statistics.
226    pub fn reset_stats(&mut self) {
227        self.stats = PriorityQueueStats::default();
228    }
229}
230
231impl Default for PropagationQueue {
232    fn default() -> Self {
233        Self::default_config()
234    }
235}
236
237#[cfg(test)]
238mod tests {
239    use super::*;
240
241    #[test]
242    fn test_queue_creation() {
243        let queue = PropagationQueue::default_config();
244        assert!(queue.is_empty());
245        assert_eq!(queue.len(), 0);
246    }
247
248    #[test]
249    fn test_priority_ordering() {
250        use oxiz_sat::Var;
251        let mut queue = PropagationQueue::default_config();
252
253        // Enqueue in reverse priority order
254        let _heuristic = queue.enqueue(PropagationType::Heuristic, None);
255        let _theory = queue.enqueue(PropagationType::Theory(2), None);
256        let _equality = queue.enqueue(PropagationType::Equality, None);
257        let boolean = queue.enqueue(PropagationType::Boolean, Some(Lit::pos(Var::new(0))));
258
259        // Boolean should be dequeued first (highest priority)
260        let first = queue.dequeue().unwrap();
261        assert_eq!(first.id, boolean);
262        assert_eq!(first.priority, 0);
263    }
264
265    #[test]
266    fn test_timestamp_fifo() {
267        let mut queue = PropagationQueue::default_config();
268
269        // Enqueue multiple with same priority
270        let id1 = queue.enqueue(PropagationType::Theory(0), None);
271        let id2 = queue.enqueue(PropagationType::Theory(0), None);
272        let id3 = queue.enqueue(PropagationType::Theory(0), None);
273
274        // Should dequeue in FIFO order
275        assert_eq!(queue.dequeue().unwrap().id, id1);
276        assert_eq!(queue.dequeue().unwrap().id, id2);
277        assert_eq!(queue.dequeue().unwrap().id, id3);
278    }
279
280    #[test]
281    fn test_peek() {
282        use oxiz_sat::Var;
283        let mut queue = PropagationQueue::default_config();
284        let id = queue.enqueue(PropagationType::Boolean, Some(Lit::pos(Var::new(0))));
285
286        let peeked = queue.peek().unwrap();
287        assert_eq!(peeked.id, id);
288        assert_eq!(queue.len(), 1); // Still in queue
289
290        let dequeued = queue.dequeue().unwrap();
291        assert_eq!(dequeued.id, id);
292        assert_eq!(queue.len(), 0);
293    }
294
295    #[test]
296    fn test_clear() {
297        use oxiz_sat::Var;
298        let mut queue = PropagationQueue::default_config();
299        queue.enqueue(PropagationType::Boolean, Some(Lit::pos(Var::new(0))));
300        queue.enqueue(PropagationType::Equality, None);
301
302        assert_eq!(queue.len(), 2);
303
304        queue.clear();
305        assert!(queue.is_empty());
306    }
307
308    #[test]
309    fn test_stats() {
310        use oxiz_sat::Var;
311        let mut queue = PropagationQueue::default_config();
312        queue.enqueue(PropagationType::Boolean, Some(Lit::pos(Var::new(0))));
313        queue.enqueue(PropagationType::Boolean, Some(Lit::pos(Var::new(1))));
314        queue.dequeue();
315
316        let stats = queue.stats();
317        assert_eq!(stats.enqueued, 2);
318        assert_eq!(stats.dequeued, 1);
319        assert_eq!(stats.peak_size, 2);
320    }
321}
oxiz_solver/propagation/priority_queue.rs

oxiz_solver/propagation/
priority_queue.rs
