smt_scope/items/
idx.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4#[macro_export]
5macro_rules! idx {
6    ($struct:ident, $prefix:tt) => {
7        #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
8        #[cfg_attr(feature = "mem_dbg", copy_type)]
9        #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
10        #[derive(Clone, Copy, Eq, PartialEq, PartialOrd, Ord, Hash)]
11        // Note: we use `u32` since this the file would need to be > ~100GB to
12        // overflow this with the number of terms constructed
13        pub struct $struct($crate::NonMaxU32);
14        impl From<usize> for $struct {
15            fn from(value: usize) -> Self {
16                assert!(value < u32::MAX as usize);
17                Self($crate::NonMaxU32::new(value as u32).unwrap())
18            }
19        }
20        impl From<$struct> for usize {
21            fn from(value: $struct) -> Self {
22                value.0.get() as usize
23            }
24        }
25        impl core::fmt::Debug for $struct {
26            fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
27                write!(f, $prefix, self.0)
28            }
29        }
30        impl core::fmt::Display for $struct {
31            fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
32                write!(f, $prefix, self.0)
33            }
34        }
35        impl $struct {
36            pub const ZERO: Self = Self($crate::NonMaxU32::ZERO);
37            pub const MAX: Self = Self($crate::NonMaxU32::MAX);
38        }
39    };
40}
41idx!(TermIdx, "t{}");
42idx!(QuantIdx, "q{}");
43idx!(InstIdx, "i{}");
44idx!(StackIdx, "s{}");
45idx!(ENodeIdx, "e{}");
46idx!(MatchIdx, "m{}");
47idx!(EqGivenIdx, "≡{}");
48idx!(EqTransIdx, "={}");
49idx!(GraphIdx, "g{}");
50idx!(ProofIdx, "p{}");
51idx!(LitIdx, "l{}");
52idx!(CdclIdx, "c{}");
53
54// Not used for TiVec, but just as a typed wrapper
55
56idx!(PatternIdx, "{{{}}}");
smt_scope/items/idx.rs

smt_scope/items/
idx.rs
