1use super::functions::*;
6use crate::Expr;
7use std::collections::{HashMap, HashSet, VecDeque};
8
9#[allow(dead_code)]
11pub struct EquivalenceTable {
12 hash_to_id: std::collections::HashMap<u64, usize>,
13 uf: UnionFind,
14 next_id: usize,
15}
16#[allow(dead_code)]
17impl EquivalenceTable {
18 pub fn new(capacity: usize) -> Self {
20 Self {
21 hash_to_id: std::collections::HashMap::with_capacity(capacity),
22 uf: UnionFind::new(capacity),
23 next_id: 0,
24 }
25 }
26 pub fn register(&mut self, hash: u64) -> usize {
28 if let Some(&id) = self.hash_to_id.get(&hash) {
29 return id;
30 }
31 let id = self.next_id;
32 self.next_id += 1;
33 self.hash_to_id.insert(hash, id);
34 id
35 }
36 pub fn merge(&mut self, h1: u64, h2: u64) {
38 let id1 = self.register(h1);
39 let id2 = self.register(h2);
40 self.uf.union(id1, id2);
41 }
42 pub fn equiv(&mut self, h1: u64, h2: u64) -> bool {
44 let id1 = self.register(h1);
45 let id2 = self.register(h2);
46 self.uf.same(id1, id2)
47 }
48}
49#[allow(dead_code)]
51#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
52pub struct Timestamp(u64);
53#[allow(dead_code)]
54impl Timestamp {
55 pub const fn from_us(us: u64) -> Self {
57 Self(us)
58 }
59 pub fn as_us(self) -> u64 {
61 self.0
62 }
63 pub fn elapsed_since(self, earlier: Timestamp) -> u64 {
65 self.0.saturating_sub(earlier.0)
66 }
67}
68#[allow(dead_code)]
70#[derive(Clone, Copy, Debug, PartialEq, Eq)]
71pub struct Generation(u32);
72#[allow(dead_code)]
73impl Generation {
74 pub const INITIAL: Generation = Generation(0);
76 pub fn advance(self) -> Generation {
78 Generation(self.0 + 1)
79 }
80 pub fn number(self) -> u32 {
82 self.0
83 }
84}
85#[allow(dead_code)]
87pub struct LoopClock {
88 start: std::time::Instant,
89 iters: u64,
90}
91#[allow(dead_code)]
92impl LoopClock {
93 pub fn start() -> Self {
95 Self {
96 start: std::time::Instant::now(),
97 iters: 0,
98 }
99 }
100 pub fn tick(&mut self) {
102 self.iters += 1;
103 }
104 pub fn elapsed_us(&self) -> f64 {
106 self.start.elapsed().as_secs_f64() * 1e6
107 }
108 pub fn avg_us_per_iter(&self) -> f64 {
110 if self.iters == 0 {
111 return 0.0;
112 }
113 self.elapsed_us() / self.iters as f64
114 }
115 pub fn iters(&self) -> u64 {
117 self.iters
118 }
119}
120#[allow(dead_code)]
122pub struct BiMap<A: std::hash::Hash + Eq + Clone, B: std::hash::Hash + Eq + Clone> {
123 forward: std::collections::HashMap<A, B>,
124 backward: std::collections::HashMap<B, A>,
125}
126#[allow(dead_code)]
127impl<A: std::hash::Hash + Eq + Clone, B: std::hash::Hash + Eq + Clone> BiMap<A, B> {
128 pub fn new() -> Self {
130 Self {
131 forward: std::collections::HashMap::new(),
132 backward: std::collections::HashMap::new(),
133 }
134 }
135 pub fn insert(&mut self, a: A, b: B) {
137 self.forward.insert(a.clone(), b.clone());
138 self.backward.insert(b, a);
139 }
140 pub fn get_b(&self, a: &A) -> Option<&B> {
142 self.forward.get(a)
143 }
144 pub fn get_a(&self, b: &B) -> Option<&A> {
146 self.backward.get(b)
147 }
148 pub fn len(&self) -> usize {
150 self.forward.len()
151 }
152 pub fn is_empty(&self) -> bool {
154 self.forward.is_empty()
155 }
156}
157#[allow(dead_code)]
159#[allow(missing_docs)]
160pub struct BeforeAfter<T> {
161 pub before: T,
163 pub after: T,
165}
166#[allow(dead_code)]
167impl<T: PartialEq> BeforeAfter<T> {
168 pub fn new(before: T, after: T) -> Self {
170 Self { before, after }
171 }
172 pub fn unchanged(&self) -> bool {
174 self.before == self.after
175 }
176}
177#[allow(dead_code)]
179pub struct SimpleLruCache<K: std::hash::Hash + Eq + Clone, V: Clone> {
180 capacity: usize,
181 map: std::collections::HashMap<K, usize>,
182 keys: Vec<K>,
183 vals: Vec<V>,
184 order: Vec<usize>,
185}
186#[allow(dead_code)]
187impl<K: std::hash::Hash + Eq + Clone, V: Clone> SimpleLruCache<K, V> {
188 pub fn new(capacity: usize) -> Self {
190 assert!(capacity > 0);
191 Self {
192 capacity,
193 map: std::collections::HashMap::new(),
194 keys: Vec::new(),
195 vals: Vec::new(),
196 order: Vec::new(),
197 }
198 }
199 pub fn put(&mut self, key: K, val: V) {
201 if let Some(&idx) = self.map.get(&key) {
202 self.vals[idx] = val;
203 self.order.retain(|&x| x != idx);
204 self.order.insert(0, idx);
205 return;
206 }
207 if self.keys.len() >= self.capacity {
208 let evict_idx = *self
209 .order
210 .last()
211 .expect("order list must be non-empty before eviction");
212 self.map.remove(&self.keys[evict_idx]);
213 self.order.pop();
214 self.keys[evict_idx] = key.clone();
215 self.vals[evict_idx] = val;
216 self.map.insert(key, evict_idx);
217 self.order.insert(0, evict_idx);
218 } else {
219 let idx = self.keys.len();
220 self.keys.push(key.clone());
221 self.vals.push(val);
222 self.map.insert(key, idx);
223 self.order.insert(0, idx);
224 }
225 }
226 pub fn get(&mut self, key: &K) -> Option<&V> {
228 let idx = *self.map.get(key)?;
229 self.order.retain(|&x| x != idx);
230 self.order.insert(0, idx);
231 Some(&self.vals[idx])
232 }
233 pub fn len(&self) -> usize {
235 self.keys.len()
236 }
237 pub fn is_empty(&self) -> bool {
239 self.keys.is_empty()
240 }
241}
242#[allow(dead_code)]
244pub struct SparseBitSet {
245 words: Vec<u64>,
246}
247#[allow(dead_code)]
248impl SparseBitSet {
249 pub fn new(capacity: usize) -> Self {
251 let words = (capacity + 63) / 64;
252 Self {
253 words: vec![0u64; words],
254 }
255 }
256 pub fn set(&mut self, i: usize) {
258 let word = i / 64;
259 let bit = i % 64;
260 if word < self.words.len() {
261 self.words[word] |= 1u64 << bit;
262 }
263 }
264 pub fn clear(&mut self, i: usize) {
266 let word = i / 64;
267 let bit = i % 64;
268 if word < self.words.len() {
269 self.words[word] &= !(1u64 << bit);
270 }
271 }
272 pub fn get(&self, i: usize) -> bool {
274 let word = i / 64;
275 let bit = i % 64;
276 self.words.get(word).is_some_and(|w| w & (1u64 << bit) != 0)
277 }
278 pub fn count_ones(&self) -> u32 {
280 self.words.iter().map(|w| w.count_ones()).sum()
281 }
282 pub fn union(&self, other: &SparseBitSet) -> SparseBitSet {
284 let len = self.words.len().max(other.words.len());
285 let mut result = SparseBitSet {
286 words: vec![0u64; len],
287 };
288 for i in 0..self.words.len() {
289 result.words[i] |= self.words[i];
290 }
291 for i in 0..other.words.len() {
292 result.words[i] |= other.words[i];
293 }
294 result
295 }
296}
297#[allow(dead_code)]
299pub struct FrequencyTable<T: std::hash::Hash + Eq + Clone> {
300 counts: std::collections::HashMap<T, u64>,
301}
302#[allow(dead_code)]
303impl<T: std::hash::Hash + Eq + Clone> FrequencyTable<T> {
304 pub fn new() -> Self {
306 Self {
307 counts: std::collections::HashMap::new(),
308 }
309 }
310 pub fn record(&mut self, item: T) {
312 *self.counts.entry(item).or_insert(0) += 1;
313 }
314 pub fn freq(&self, item: &T) -> u64 {
316 self.counts.get(item).copied().unwrap_or(0)
317 }
318 pub fn most_frequent(&self) -> Option<(&T, u64)> {
320 self.counts
321 .iter()
322 .max_by_key(|(_, &v)| v)
323 .map(|(k, &v)| (k, v))
324 }
325 pub fn total(&self) -> u64 {
327 self.counts.values().sum()
328 }
329 pub fn distinct(&self) -> usize {
331 self.counts.len()
332 }
333}
334#[allow(dead_code)]
336pub struct WorkStack<T> {
337 items: Vec<T>,
338}
339#[allow(dead_code)]
340impl<T> WorkStack<T> {
341 pub fn new() -> Self {
343 Self { items: Vec::new() }
344 }
345 pub fn push(&mut self, item: T) {
347 self.items.push(item);
348 }
349 pub fn pop(&mut self) -> Option<T> {
351 self.items.pop()
352 }
353 pub fn is_empty(&self) -> bool {
355 self.items.is_empty()
356 }
357 pub fn len(&self) -> usize {
359 self.items.len()
360 }
361}
362#[allow(dead_code)]
364pub struct SymmetricRelation {
365 pairs: std::collections::HashSet<(u64, u64)>,
366}
367#[allow(dead_code)]
368impl SymmetricRelation {
369 pub fn new() -> Self {
371 Self {
372 pairs: std::collections::HashSet::new(),
373 }
374 }
375 fn key(a: u64, b: u64) -> (u64, u64) {
376 if a <= b {
377 (a, b)
378 } else {
379 (b, a)
380 }
381 }
382 pub fn add(&mut self, a: u64, b: u64) {
384 self.pairs.insert(Self::key(a, b));
385 }
386 pub fn contains(&self, a: u64, b: u64) -> bool {
388 self.pairs.contains(&Self::key(a, b))
389 }
390 pub fn len(&self) -> usize {
392 self.pairs.len()
393 }
394 pub fn is_empty(&self) -> bool {
396 self.pairs.is_empty()
397 }
398}
399#[allow(dead_code)]
401pub struct MemoSlot<T: Clone> {
402 cached: Option<T>,
403}
404#[allow(dead_code)]
405impl<T: Clone> MemoSlot<T> {
406 pub fn new() -> Self {
408 Self { cached: None }
409 }
410 pub fn get_or_compute(&mut self, f: impl FnOnce() -> T) -> &T {
412 if self.cached.is_none() {
413 self.cached = Some(f());
414 }
415 self.cached
416 .as_ref()
417 .expect("cached value must be initialized before access")
418 }
419 pub fn invalidate(&mut self) {
421 self.cached = None;
422 }
423 pub fn is_cached(&self) -> bool {
425 self.cached.is_some()
426 }
427}
428#[allow(dead_code)]
430pub struct CheckedEquiv {
431 lhs: u64,
432 rhs: u64,
433 proof: EquivProofTerm,
434}
435#[allow(dead_code)]
436impl CheckedEquiv {
437 pub fn refl(id: u64) -> Self {
439 Self {
440 lhs: id,
441 rhs: id,
442 proof: EquivProofTerm::Refl(id),
443 }
444 }
445 pub fn by_axiom(lhs: u64, rhs: u64, name: impl Into<String>) -> Self {
447 Self {
448 lhs,
449 rhs,
450 proof: EquivProofTerm::Axiom(name.into()),
451 }
452 }
453 pub fn lhs(&self) -> u64 {
455 self.lhs
456 }
457 pub fn rhs(&self) -> u64 {
459 self.rhs
460 }
461 pub fn proof(&self) -> &EquivProofTerm {
463 &self.proof
464 }
465 pub fn is_trivial(&self) -> bool {
467 self.lhs == self.rhs
468 }
469}
470#[allow(dead_code)]
472pub struct EventCounter {
473 counts: std::collections::HashMap<String, u64>,
474}
475#[allow(dead_code)]
476impl EventCounter {
477 pub fn new() -> Self {
479 Self {
480 counts: std::collections::HashMap::new(),
481 }
482 }
483 pub fn inc(&mut self, event: &str) {
485 *self.counts.entry(event.to_string()).or_insert(0) += 1;
486 }
487 pub fn add(&mut self, event: &str, n: u64) {
489 *self.counts.entry(event.to_string()).or_insert(0) += n;
490 }
491 pub fn get(&self, event: &str) -> u64 {
493 self.counts.get(event).copied().unwrap_or(0)
494 }
495 pub fn total(&self) -> u64 {
497 self.counts.values().sum()
498 }
499 pub fn reset(&mut self) {
501 self.counts.clear();
502 }
503 pub fn event_names(&self) -> Vec<&str> {
505 self.counts.keys().map(|s| s.as_str()).collect()
506 }
507}
508#[allow(dead_code)]
510pub struct AnnotationTable {
511 map: std::collections::HashMap<String, Vec<String>>,
512}
513#[allow(dead_code)]
514impl AnnotationTable {
515 pub fn new() -> Self {
517 Self {
518 map: std::collections::HashMap::new(),
519 }
520 }
521 pub fn annotate(&mut self, key: impl Into<String>, val: impl Into<String>) {
523 self.map.entry(key.into()).or_default().push(val.into());
524 }
525 pub fn get_all(&self, key: &str) -> &[String] {
527 self.map.get(key).map(|v| v.as_slice()).unwrap_or(&[])
528 }
529 pub fn num_keys(&self) -> usize {
531 self.map.len()
532 }
533 pub fn has(&self, key: &str) -> bool {
535 self.map.contains_key(key)
536 }
537}
538#[allow(dead_code)]
540pub struct WorkQueue<T> {
541 items: std::collections::VecDeque<T>,
542}
543#[allow(dead_code)]
544impl<T> WorkQueue<T> {
545 pub fn new() -> Self {
547 Self {
548 items: std::collections::VecDeque::new(),
549 }
550 }
551 pub fn enqueue(&mut self, item: T) {
553 self.items.push_back(item);
554 }
555 pub fn dequeue(&mut self) -> Option<T> {
557 self.items.pop_front()
558 }
559 pub fn is_empty(&self) -> bool {
561 self.items.is_empty()
562 }
563 pub fn len(&self) -> usize {
565 self.items.len()
566 }
567}
568#[allow(dead_code)]
570pub struct IdDispenser<T> {
571 next: u32,
572 _phantom: std::marker::PhantomData<T>,
573}
574#[allow(dead_code)]
575impl<T> IdDispenser<T> {
576 pub fn new() -> Self {
578 Self {
579 next: 0,
580 _phantom: std::marker::PhantomData,
581 }
582 }
583 #[allow(clippy::should_implement_trait)]
585 pub fn next(&mut self) -> TypedId<T> {
586 let id = TypedId::new(self.next);
587 self.next += 1;
588 id
589 }
590 pub fn count(&self) -> u32 {
592 self.next
593 }
594}
595#[allow(dead_code)]
597pub struct Slot<T> {
598 inner: Option<T>,
599}
600#[allow(dead_code)]
601impl<T> Slot<T> {
602 pub fn empty() -> Self {
604 Self { inner: None }
605 }
606 pub fn fill(&mut self, val: T) {
608 assert!(self.inner.is_none(), "Slot: already filled");
609 self.inner = Some(val);
610 }
611 pub fn get(&self) -> Option<&T> {
613 self.inner.as_ref()
614 }
615 pub fn is_filled(&self) -> bool {
617 self.inner.is_some()
618 }
619 pub fn take(&mut self) -> Option<T> {
621 self.inner.take()
622 }
623 pub fn get_or_fill_with(&mut self, f: impl FnOnce() -> T) -> &T {
625 if self.inner.is_none() {
626 self.inner = Some(f());
627 }
628 self.inner
629 .as_ref()
630 .expect("inner value must be initialized before access")
631 }
632}
633#[allow(dead_code)]
635#[allow(missing_docs)]
636pub struct EquivClass {
637 pub repr: usize,
639 pub members: Vec<usize>,
641}
642#[allow(dead_code)]
643impl EquivClass {
644 pub fn singleton(id: usize) -> Self {
646 Self {
647 repr: id,
648 members: vec![id],
649 }
650 }
651 pub fn contains(&self, id: usize) -> bool {
653 self.members.contains(&id)
654 }
655 pub fn size(&self) -> usize {
657 self.members.len()
658 }
659}
660#[allow(dead_code)]
662#[derive(Debug, Clone)]
663pub enum EquivProofTerm {
664 Refl(u64),
666 Symm(Box<EquivProofTerm>),
668 Trans(Box<EquivProofTerm>, Box<EquivProofTerm>),
670 Axiom(String),
672}
673#[allow(dead_code)]
674impl EquivProofTerm {
675 pub fn depth(&self) -> usize {
677 match self {
678 EquivProofTerm::Refl(_) => 0,
679 EquivProofTerm::Axiom(_) => 0,
680 EquivProofTerm::Symm(p) => 1 + p.depth(),
681 EquivProofTerm::Trans(p, q) => 1 + p.depth().max(q.depth()),
682 }
683 }
684 pub fn is_refl(&self) -> bool {
686 matches!(self, EquivProofTerm::Refl(_))
687 }
688}
689#[derive(Debug)]
691struct UnionFindEntry {
692 parent: usize,
693 rank: u32,
694}
695#[derive(Clone, Debug, Default)]
697pub struct EquivStats {
698 pub total_queries: u64,
700 pub equiv_hits: u64,
702 pub failure_hits: u64,
704 pub cache_misses: u64,
706 pub equiv_additions: u64,
708 pub failure_additions: u64,
710}
711impl EquivStats {
712 pub fn new() -> Self {
714 Self::default()
715 }
716 pub fn record_equiv_hit(&mut self) {
718 self.total_queries += 1;
719 self.equiv_hits += 1;
720 }
721 pub fn record_failure_hit(&mut self) {
723 self.total_queries += 1;
724 self.failure_hits += 1;
725 }
726 pub fn record_miss(&mut self) {
728 self.total_queries += 1;
729 self.cache_misses += 1;
730 }
731 pub fn record_equiv_addition(&mut self) {
733 self.equiv_additions += 1;
734 }
735 pub fn record_failure_addition(&mut self) {
737 self.failure_additions += 1;
738 }
739 pub fn hit_rate(&self) -> f64 {
741 if self.total_queries == 0 {
742 return 1.0;
743 }
744 (self.equiv_hits + self.failure_hits) as f64 / self.total_queries as f64
745 }
746}
747#[allow(dead_code)]
749pub struct IntervalSet {
750 intervals: Vec<(i64, i64)>,
751}
752#[allow(dead_code)]
753impl IntervalSet {
754 pub fn new() -> Self {
756 Self {
757 intervals: Vec::new(),
758 }
759 }
760 pub fn add(&mut self, lo: i64, hi: i64) {
762 if lo > hi {
763 return;
764 }
765 let mut new_lo = lo;
766 let mut new_hi = hi;
767 let mut i = 0;
768 while i < self.intervals.len() {
769 let (il, ih) = self.intervals[i];
770 if ih < new_lo - 1 {
771 i += 1;
772 continue;
773 }
774 if il > new_hi + 1 {
775 break;
776 }
777 new_lo = new_lo.min(il);
778 new_hi = new_hi.max(ih);
779 self.intervals.remove(i);
780 }
781 self.intervals.insert(i, (new_lo, new_hi));
782 }
783 pub fn contains(&self, x: i64) -> bool {
785 self.intervals.iter().any(|&(lo, hi)| x >= lo && x <= hi)
786 }
787 pub fn num_intervals(&self) -> usize {
789 self.intervals.len()
790 }
791 pub fn cardinality(&self) -> i64 {
793 self.intervals.iter().map(|&(lo, hi)| hi - lo + 1).sum()
794 }
795}
796#[derive(Debug)]
805pub struct EquivManager {
806 equiv_set: HashSet<(Expr, Expr)>,
808 failure_set: HashSet<(Expr, Expr)>,
810 expr_to_idx: HashMap<Expr, usize>,
813 entries: Vec<UnionFindEntry>,
815}
816impl EquivManager {
817 pub fn new() -> Self {
819 EquivManager {
820 equiv_set: HashSet::new(),
821 failure_set: HashSet::new(),
822 expr_to_idx: HashMap::new(),
823 entries: Vec::new(),
824 }
825 }
826 pub fn add_equiv(&mut self, a: &Expr, b: &Expr) {
828 if a == b {
829 return;
830 }
831 let pair = canonicalize_pair(a.clone(), b.clone());
832 self.equiv_set.insert(pair);
833 let idx_a = self.get_or_create_idx(a);
834 let idx_b = self.get_or_create_idx(b);
835 self.union(idx_a, idx_b);
836 }
837 pub fn is_equiv(&mut self, a: &Expr, b: &Expr) -> bool {
839 if a == b {
840 return true;
841 }
842 let pair = canonicalize_pair(a.clone(), b.clone());
843 if self.equiv_set.contains(&pair) {
844 return true;
845 }
846 if let (Some(&idx_a), Some(&idx_b)) = (self.expr_to_idx.get(a), self.expr_to_idx.get(b)) {
847 return self.find(idx_a) == self.find(idx_b);
848 }
849 false
850 }
851 pub fn add_failure(&mut self, a: &Expr, b: &Expr) {
853 let pair = canonicalize_pair(a.clone(), b.clone());
854 self.failure_set.insert(pair);
855 }
856 pub fn is_failure(&self, a: &Expr, b: &Expr) -> bool {
858 let pair = canonicalize_pair(a.clone(), b.clone());
859 self.failure_set.contains(&pair)
860 }
861 pub fn clear(&mut self) {
863 self.equiv_set.clear();
864 self.failure_set.clear();
865 self.expr_to_idx.clear();
866 self.entries.clear();
867 }
868 pub fn num_equiv(&self) -> usize {
870 self.equiv_set.len()
871 }
872 pub fn num_failures(&self) -> usize {
874 self.failure_set.len()
875 }
876 fn get_or_create_idx(&mut self, e: &Expr) -> usize {
877 if let Some(&idx) = self.expr_to_idx.get(e) {
878 return idx;
879 }
880 let idx = self.entries.len();
881 self.entries.push(UnionFindEntry {
882 parent: idx,
883 rank: 0,
884 });
885 self.expr_to_idx.insert(e.clone(), idx);
886 idx
887 }
888 fn find(&mut self, mut x: usize) -> usize {
889 while self.entries[x].parent != x {
890 let grandparent = self.entries[self.entries[x].parent].parent;
891 self.entries[x].parent = grandparent;
892 x = grandparent;
893 }
894 x
895 }
896 fn union(&mut self, x: usize, y: usize) {
897 let rx = self.find(x);
898 let ry = self.find(y);
899 if rx == ry {
900 return;
901 }
902 match self.entries[rx].rank.cmp(&self.entries[ry].rank) {
903 std::cmp::Ordering::Less => {
904 self.entries[rx].parent = ry;
905 }
906 std::cmp::Ordering::Greater => {
907 self.entries[ry].parent = rx;
908 }
909 std::cmp::Ordering::Equal => {
910 self.entries[ry].parent = rx;
911 self.entries[rx].rank += 1;
912 }
913 }
914 }
915}
916#[derive(Clone, Debug, Default)]
918pub struct IndexEquivManager {
919 parent: Vec<usize>,
920 rank: Vec<u32>,
921}
922impl IndexEquivManager {
923 pub fn new(n: usize) -> Self {
925 Self {
926 parent: (0..n).collect(),
927 rank: vec![0; n],
928 }
929 }
930 pub fn find(&mut self, x: usize) -> usize {
932 if self.parent[x] != x {
933 self.parent[x] = self.find(self.parent[x]);
934 }
935 self.parent[x]
936 }
937 pub fn union(&mut self, x: usize, y: usize) {
939 let rx = self.find(x);
940 let ry = self.find(y);
941 if rx == ry {
942 return;
943 }
944 match self.rank[rx].cmp(&self.rank[ry]) {
945 std::cmp::Ordering::Less => self.parent[rx] = ry,
946 std::cmp::Ordering::Greater => self.parent[ry] = rx,
947 std::cmp::Ordering::Equal => {
948 self.parent[ry] = rx;
949 self.rank[rx] += 1;
950 }
951 }
952 }
953 pub fn same_class(&mut self, x: usize, y: usize) -> bool {
955 self.find(x) == self.find(y)
956 }
957 pub fn num_classes(&mut self) -> usize {
959 let n = self.parent.len();
960 let roots: std::collections::HashSet<usize> = (0..n).map(|i| self.find(i)).collect();
961 roots.len()
962 }
963}
964#[allow(dead_code)]
966pub struct DiagMeta {
967 pub(super) entries: Vec<(String, String)>,
968}
969#[allow(dead_code)]
970impl DiagMeta {
971 pub fn new() -> Self {
973 Self {
974 entries: Vec::new(),
975 }
976 }
977 pub fn add(&mut self, key: impl Into<String>, val: impl Into<String>) {
979 self.entries.push((key.into(), val.into()));
980 }
981 pub fn get(&self, key: &str) -> Option<&str> {
983 self.entries
984 .iter()
985 .find(|(k, _)| k == key)
986 .map(|(_, v)| v.as_str())
987 }
988 pub fn len(&self) -> usize {
990 self.entries.len()
991 }
992 pub fn is_empty(&self) -> bool {
994 self.entries.is_empty()
995 }
996}
997#[allow(dead_code)]
999#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
1000pub struct TypedId<T> {
1001 pub(super) id: u32,
1002 _phantom: std::marker::PhantomData<T>,
1003}
1004#[allow(dead_code)]
1005impl<T> TypedId<T> {
1006 pub const fn new(id: u32) -> Self {
1008 Self {
1009 id,
1010 _phantom: std::marker::PhantomData,
1011 }
1012 }
1013 pub fn raw(&self) -> u32 {
1015 self.id
1016 }
1017}
1018#[allow(dead_code)]
1020#[allow(missing_docs)]
1021pub struct StatCache<K: std::hash::Hash + Eq + Clone, V: Clone> {
1022 pub inner: SimpleLruCache<K, V>,
1024 pub hits: u64,
1026 pub misses: u64,
1028}
1029#[allow(dead_code)]
1030impl<K: std::hash::Hash + Eq + Clone, V: Clone> StatCache<K, V> {
1031 pub fn new(capacity: usize) -> Self {
1033 Self {
1034 inner: SimpleLruCache::new(capacity),
1035 hits: 0,
1036 misses: 0,
1037 }
1038 }
1039 pub fn get(&mut self, key: &K) -> Option<&V> {
1041 let result = self.inner.get(key);
1042 if result.is_some() {
1043 self.hits += 1;
1044 } else {
1045 self.misses += 1;
1046 }
1047 None
1048 }
1049 pub fn put(&mut self, key: K, val: V) {
1051 self.inner.put(key, val);
1052 }
1053 pub fn hit_rate(&self) -> f64 {
1055 let total = self.hits + self.misses;
1056 if total == 0 {
1057 return 0.0;
1058 }
1059 self.hits as f64 / total as f64
1060 }
1061}
1062#[allow(dead_code)]
1064pub struct ScopeStack {
1065 names: Vec<String>,
1066}
1067#[allow(dead_code)]
1068impl ScopeStack {
1069 pub fn new() -> Self {
1071 Self { names: Vec::new() }
1072 }
1073 pub fn push(&mut self, name: impl Into<String>) {
1075 self.names.push(name.into());
1076 }
1077 pub fn pop(&mut self) -> Option<String> {
1079 self.names.pop()
1080 }
1081 pub fn current(&self) -> Option<&str> {
1083 self.names.last().map(|s| s.as_str())
1084 }
1085 pub fn depth(&self) -> usize {
1087 self.names.len()
1088 }
1089 pub fn is_empty(&self) -> bool {
1091 self.names.is_empty()
1092 }
1093 pub fn path(&self) -> String {
1095 self.names.join(".")
1096 }
1097}
1098#[allow(dead_code)]
1100#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
1101pub struct SeqNum(u64);
1102#[allow(dead_code)]
1103impl SeqNum {
1104 pub const ZERO: SeqNum = SeqNum(0);
1106 pub fn next(self) -> SeqNum {
1108 SeqNum(self.0 + 1)
1109 }
1110 pub fn value(self) -> u64 {
1112 self.0
1113 }
1114}
1115#[derive(Debug, Default)]
1117pub struct InstrumentedEquivManager {
1118 inner: EquivManager,
1120 stats: EquivStats,
1122}
1123impl InstrumentedEquivManager {
1124 pub fn new() -> Self {
1126 Self::default()
1127 }
1128 pub fn add_equiv(&mut self, a: &Expr, b: &Expr) {
1130 self.stats.record_equiv_addition();
1131 self.inner.add_equiv(a, b);
1132 }
1133 pub fn add_failure(&mut self, a: &Expr, b: &Expr) {
1135 self.stats.record_failure_addition();
1136 self.inner.add_failure(a, b);
1137 }
1138 pub fn is_equiv(&mut self, a: &Expr, b: &Expr) -> bool {
1140 let result = self.inner.is_equiv(a, b);
1141 if result {
1142 self.stats.record_equiv_hit();
1143 } else {
1144 self.stats.record_miss();
1145 }
1146 result
1147 }
1148 pub fn is_failure(&self, a: &Expr, b: &Expr) -> bool {
1150 self.inner.is_failure(a, b)
1151 }
1152 pub fn stats(&self) -> &EquivStats {
1154 &self.stats
1155 }
1156 pub fn clear(&mut self) {
1158 self.inner.clear();
1159 self.stats = EquivStats::new();
1160 }
1161}
1162#[allow(dead_code)]
1164#[allow(missing_docs)]
1165pub struct EquivManagerStats {
1166 pub checks: u64,
1168 pub hits: u64,
1170 pub merges: u64,
1172 pub classes: usize,
1174}
1175#[allow(dead_code)]
1176impl EquivManagerStats {
1177 pub fn new() -> Self {
1179 Self {
1180 checks: 0,
1181 hits: 0,
1182 merges: 0,
1183 classes: 0,
1184 }
1185 }
1186 pub fn hit_rate(&self) -> f64 {
1188 if self.checks == 0 {
1189 return 0.0;
1190 }
1191 self.hits as f64 / self.checks as f64
1192 }
1193}
1194pub struct EquivQuery<'a> {
1196 manager: &'a EquivManager,
1197}
1198impl<'a> EquivQuery<'a> {
1199 pub fn new(manager: &'a EquivManager) -> Self {
1201 Self { manager }
1202 }
1203 pub fn is_known_failure(&self, a: &Expr, b: &Expr) -> bool {
1205 self.manager.is_failure(a, b)
1206 }
1207 pub fn num_equiv(&self) -> usize {
1209 self.manager.num_equiv()
1210 }
1211 pub fn num_failures(&self) -> usize {
1213 self.manager.num_failures()
1214 }
1215}
1216#[derive(Clone, Debug, Default)]
1221pub struct PersistentEquivManager {
1222 pairs: Vec<(String, String)>,
1223}
1224impl PersistentEquivManager {
1225 pub fn new() -> Self {
1227 Self::default()
1228 }
1229 pub fn add_equiv(&mut self, a: &Expr, b: &Expr) {
1231 let ka = format!("{:?}", a);
1232 let kb = format!("{:?}", b);
1233 let pair = if ka <= kb { (ka, kb) } else { (kb, ka) };
1234 if !self.pairs.contains(&pair) {
1235 self.pairs.push(pair);
1236 self.pairs.sort();
1237 }
1238 }
1239 pub fn is_equiv(&self, a: &Expr, b: &Expr) -> bool {
1241 if a == b {
1242 return true;
1243 }
1244 let ka = format!("{:?}", a);
1245 let kb = format!("{:?}", b);
1246 let pair = if ka <= kb {
1247 (ka.clone(), kb.clone())
1248 } else {
1249 (kb.clone(), ka.clone())
1250 };
1251 self.pairs.contains(&pair)
1252 }
1253 pub fn len(&self) -> usize {
1255 self.pairs.len()
1256 }
1257 pub fn is_empty(&self) -> bool {
1259 self.pairs.is_empty()
1260 }
1261 pub fn serialize(&self) -> Vec<(String, String)> {
1263 self.pairs.clone()
1264 }
1265}
1266#[allow(dead_code)]
1268pub struct ExprEquivCache {
1269 proven: std::collections::HashSet<(u64, u64)>,
1270 disproven: std::collections::HashSet<(u64, u64)>,
1271}
1272#[allow(dead_code)]
1273impl ExprEquivCache {
1274 pub fn new() -> Self {
1276 Self {
1277 proven: std::collections::HashSet::new(),
1278 disproven: std::collections::HashSet::new(),
1279 }
1280 }
1281 pub fn mark_equal(&mut self, a: u64, b: u64) {
1283 let key = if a <= b { (a, b) } else { (b, a) };
1284 self.proven.insert(key);
1285 }
1286 pub fn mark_unequal(&mut self, a: u64, b: u64) {
1288 let key = if a <= b { (a, b) } else { (b, a) };
1289 self.disproven.insert(key);
1290 }
1291 pub fn query(&self, a: u64, b: u64) -> Option<bool> {
1293 let key = if a <= b { (a, b) } else { (b, a) };
1294 if self.proven.contains(&key) {
1295 return Some(true);
1296 }
1297 if self.disproven.contains(&key) {
1298 return Some(false);
1299 }
1300 None
1301 }
1302 pub fn proven_count(&self) -> usize {
1304 self.proven.len()
1305 }
1306}
1307#[allow(dead_code)]
1309pub struct StringInterner {
1310 strings: Vec<String>,
1311 map: std::collections::HashMap<String, u32>,
1312}
1313#[allow(dead_code)]
1314impl StringInterner {
1315 pub fn new() -> Self {
1317 Self {
1318 strings: Vec::new(),
1319 map: std::collections::HashMap::new(),
1320 }
1321 }
1322 pub fn intern(&mut self, s: &str) -> u32 {
1324 if let Some(&id) = self.map.get(s) {
1325 return id;
1326 }
1327 let id = self.strings.len() as u32;
1328 self.strings.push(s.to_string());
1329 self.map.insert(s.to_string(), id);
1330 id
1331 }
1332 pub fn get(&self, id: u32) -> Option<&str> {
1334 self.strings.get(id as usize).map(|s| s.as_str())
1335 }
1336 pub fn len(&self) -> usize {
1338 self.strings.len()
1339 }
1340 pub fn is_empty(&self) -> bool {
1342 self.strings.is_empty()
1343 }
1344}
1345#[allow(dead_code)]
1347pub struct UnionFind {
1348 parent: Vec<usize>,
1349 rank: Vec<usize>,
1350 count: usize,
1351}
1352#[allow(dead_code)]
1353impl UnionFind {
1354 pub fn new(n: usize) -> Self {
1356 Self {
1357 parent: (0..n).collect(),
1358 rank: vec![0; n],
1359 count: n,
1360 }
1361 }
1362 pub fn find(&mut self, x: usize) -> usize {
1364 if self.parent[x] != x {
1365 self.parent[x] = self.find(self.parent[x]);
1366 }
1367 self.parent[x]
1368 }
1369 pub fn union(&mut self, x: usize, y: usize) -> bool {
1371 let rx = self.find(x);
1372 let ry = self.find(y);
1373 if rx == ry {
1374 return false;
1375 }
1376 if self.rank[rx] < self.rank[ry] {
1377 self.parent[rx] = ry;
1378 } else if self.rank[rx] > self.rank[ry] {
1379 self.parent[ry] = rx;
1380 } else {
1381 self.parent[ry] = rx;
1382 self.rank[rx] += 1;
1383 }
1384 self.count -= 1;
1385 true
1386 }
1387 pub fn same(&mut self, x: usize, y: usize) -> bool {
1389 self.find(x) == self.find(y)
1390 }
1391 pub fn num_classes(&self) -> usize {
1393 self.count
1394 }
1395 pub fn num_elements(&self) -> usize {
1397 self.parent.len()
1398 }
1399}
1400#[derive(Debug, Default)]
1405pub struct ScopedEquivManager {
1406 scopes: Vec<Vec<(Expr, Expr)>>,
1408 inner: EquivManager,
1410}
1411impl ScopedEquivManager {
1412 pub fn new() -> Self {
1414 Self {
1415 scopes: vec![Vec::new()],
1416 inner: EquivManager::new(),
1417 }
1418 }
1419 pub fn push_scope(&mut self) {
1421 self.scopes.push(Vec::new());
1422 }
1423 pub fn pop_scope(&mut self) {
1425 if self.scopes.len() > 1 {
1426 self.scopes.pop();
1427 self.inner.clear();
1428 for scope in &self.scopes {
1429 for (a, b) in scope {
1430 self.inner.add_equiv(a, b);
1431 }
1432 }
1433 }
1434 }
1435 pub fn add_equiv(&mut self, a: &Expr, b: &Expr) {
1437 if let Some(scope) = self.scopes.last_mut() {
1438 scope.push((a.clone(), b.clone()));
1439 }
1440 self.inner.add_equiv(a, b);
1441 }
1442 pub fn is_equiv(&mut self, a: &Expr, b: &Expr) -> bool {
1444 self.inner.is_equiv(a, b)
1445 }
1446 pub fn scope_depth(&self) -> usize {
1448 self.scopes.len()
1449 }
1450 pub fn total_equivs(&self) -> usize {
1452 self.scopes.iter().map(|s| s.len()).sum()
1453 }
1454}
1455#[allow(dead_code)]
1457pub struct RingBuffer<T> {
1458 data: Vec<Option<T>>,
1459 head: usize,
1460 tail: usize,
1461 count: usize,
1462 capacity: usize,
1463}
1464#[allow(dead_code)]
1465impl<T> RingBuffer<T> {
1466 pub fn new(capacity: usize) -> Self {
1468 let mut data = Vec::with_capacity(capacity);
1469 for _ in 0..capacity {
1470 data.push(None);
1471 }
1472 Self {
1473 data,
1474 head: 0,
1475 tail: 0,
1476 count: 0,
1477 capacity,
1478 }
1479 }
1480 pub fn push(&mut self, val: T) {
1482 if self.count == self.capacity {
1483 self.data[self.head] = Some(val);
1484 self.head = (self.head + 1) % self.capacity;
1485 self.tail = (self.tail + 1) % self.capacity;
1486 } else {
1487 self.data[self.tail] = Some(val);
1488 self.tail = (self.tail + 1) % self.capacity;
1489 self.count += 1;
1490 }
1491 }
1492 pub fn pop(&mut self) -> Option<T> {
1494 if self.count == 0 {
1495 return None;
1496 }
1497 let val = self.data[self.head].take();
1498 self.head = (self.head + 1) % self.capacity;
1499 self.count -= 1;
1500 val
1501 }
1502 pub fn len(&self) -> usize {
1504 self.count
1505 }
1506 pub fn is_empty(&self) -> bool {
1508 self.count == 0
1509 }
1510 pub fn is_full(&self) -> bool {
1512 self.count == self.capacity
1513 }
1514}