smt_scope/items/
stack.rs

1use core::fmt;
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5
6#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
7#[cfg_attr(feature = "mem_dbg", copy_type)]
8#[derive(Debug, Clone, Copy)]
9pub struct StackFrame {
10    /// Is this frame definitely from CDCL? If this is false then it may still
11    /// be from CDCL.
12    pub from_cdcl: bool,
13    pub active: TimeRange,
14}
15
16impl StackFrame {
17    pub fn new(start: u32, from_cdcl: bool) -> Self {
18        Self {
19            from_cdcl,
20            active: TimeRange {
21                start,
22                end: u32::MAX,
23                leaked: false,
24            },
25        }
26    }
27}
28
29#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
30#[cfg_attr(feature = "mem_dbg", copy_type)]
31#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
32pub struct TimeRange {
33    start: u32,
34    end: u32,
35    leaked: bool,
36}
37
38impl TimeRange {
39    pub fn sorted_overlap(&self, greater: &Self) -> bool {
40        debug_assert!(self.start <= greater.start);
41        debug_assert!(greater.end <= self.end || self.end < greater.start);
42        greater.end <= self.end
43    }
44
45    pub fn status(&self) -> TimeRangeStatus {
46        match (self.start, self.end, self.leaked) {
47            (0, end, leaked) => {
48                debug_assert!(end == u32::MAX && !leaked);
49                TimeRangeStatus::Global
50            }
51            (_, u32::MAX, leaked) => {
52                debug_assert!(!leaked);
53                TimeRangeStatus::Active
54            }
55            (_, _, true) => TimeRangeStatus::Leaked,
56            (_, _, false) => TimeRangeStatus::Ended,
57        }
58    }
59
60    pub fn end(&mut self, end: u32, leaked: bool) {
61        debug_assert!(self.status().is_active());
62        self.end = end;
63        self.leaked = leaked;
64    }
65}
66
67#[derive(Debug, Clone, Copy, PartialEq, Eq)]
68pub enum TimeRangeStatus {
69    Global,
70    Active,
71    Leaked,
72    Ended,
73}
74
75impl TimeRangeStatus {
76    pub fn is_global(self) -> bool {
77        matches!(self, Self::Global)
78    }
79    pub fn is_active(self) -> bool {
80        matches!(self, Self::Active)
81    }
82    pub fn is_leaked(self) -> bool {
83        matches!(self, Self::Leaked)
84    }
85    pub fn is_ended(self) -> bool {
86        matches!(self, Self::Ended)
87    }
88
89    pub fn is_alive(self) -> bool {
90        !self.is_ended()
91    }
92}
93
94impl fmt::Display for TimeRange {
95    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
96        match self.status() {
97            TimeRangeStatus::Global => write!(f, "∞"),
98            TimeRangeStatus::Active => write!(f, "t{}→", self.start),
99            TimeRangeStatus::Leaked => write!(f, "t{}→t{}?", self.start, self.end),
100            TimeRangeStatus::Ended => write!(f, "t{}→t{}", self.start, self.end),
101        }
102    }
103}
smt_scope/items/stack.rs

smt_scope/items/
stack.rs
