smt_scope/parsers/z3/
stack.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{
5    items::{CdclIdx, ENodeIdx, InstIdx, MatchIdx, ProofIdx, StackFrame, StackIdx},
6    Error, Result, TiVec,
7};
8
9use super::Z3Parser;
10
11#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
12#[derive(Debug)]
13pub struct Stack {
14    stack: Vec<StackIdx>,
15    pub(super) stack_frames: TiVec<StackIdx, StackFrame>,
16    timestamp: u32,
17}
18
19impl Default for Stack {
20    fn default() -> Self {
21        let mut stack_frames: TiVec<StackIdx, StackFrame> = TiVec::default();
22        let idx = stack_frames.push_and_get_key(StackFrame::new(0, false));
23        assert_eq!(idx, Self::ZERO_FRAME);
24        Self {
25            stack: vec![idx],
26            stack_frames,
27            timestamp: 1,
28        }
29    }
30}
31
32impl Stack {
33    pub const ZERO_FRAME: StackIdx = StackIdx::ZERO;
34
35    fn height(&self) -> usize {
36        self.stack.len() - 1
37    }
38
39    fn add_frame(&mut self, from_cdcl: bool) -> Result<()> {
40        self.stack_frames.raw.try_reserve(1)?;
41        let idx = self
42            .stack_frames
43            .push_and_get_key(StackFrame::new(self.timestamp, from_cdcl));
44        self.stack.try_reserve(1)?;
45        self.stack.push(idx);
46        self.timestamp += 1;
47        Ok(())
48    }
49    fn remove_frame(&mut self, active: bool, from_cdcl: bool) {
50        let idx = self.stack.pop().unwrap();
51        assert!(!self.stack.is_empty());
52        let frame = &mut self.stack_frames[idx];
53        frame.active.end(self.timestamp, active);
54        frame.from_cdcl = from_cdcl;
55        self.timestamp += 1;
56    }
57    pub(super) fn ensure_height(&mut self, height: usize) -> Result<()> {
58        let mut res = Ok(());
59        // Neither condition should hold, but handle it as best we can.
60        while height > self.height() {
61            // Have not run into this case, so make tests fail if it happens.
62            res = Err(Error::StackFrameNotPushed);
63            let from_cdcl = self.is_speculative();
64            self.add_frame(from_cdcl)?;
65        }
66        while height < self.height() {
67            // This can happen when pushing a new frame in e.g. z3 v4.8.17 and
68            // v4.11.2.
69            // It seems that there is a bug where the pop doesn't get emitted
70            // and so we need to conservatively leak the frame and treat it as
71            // always active.
72            let from_cdcl = self.is_speculative();
73            self.remove_frame(true, from_cdcl);
74        }
75        res
76    }
77
78    pub(super) fn new_frame(&mut self, idx: usize, from_cdcl: bool) -> Result<()> {
79        let res = self.ensure_height(idx);
80        self.add_frame(from_cdcl)?;
81        res
82    }
83
84    pub(super) fn pop_frames(
85        &mut self,
86        count: core::num::NonZeroUsize,
87        idx: usize,
88        after_conflict: bool,
89    ) -> Result<bool> {
90        let count = count.get();
91        debug_assert!(0 < count && count <= idx);
92        let result = self.ensure_height(idx);
93        let from_cdcl = after_conflict
94            || (0..count).any(|idx| self[self.stack[self.stack.len() - 1 - idx]].from_cdcl);
95        if from_cdcl {
96            // TODO: actually mark the frames as from CDCL (e.g. also in `smt2.rs`).
97            for idx in 0..count {
98                let frame = self.stack[self.stack.len() - 1 - idx];
99                self.stack_frames[frame].from_cdcl = true;
100            }
101        }
102        debug_assert!(
103            !from_cdcl
104                || (0..count)
105                    .all(|idx| self[self.stack[self.stack.len() - 1 - idx]].from_cdcl == from_cdcl)
106        );
107        for _ in 0..count {
108            self.remove_frame(false, from_cdcl);
109        }
110        result.map(|()| from_cdcl)
111    }
112
113    /// Called during a decision assign, immediately following a push. This
114    /// marks the push as `from_cdcl` and returns true if it wasn't already.
115    pub(super) fn new_decision(&mut self) -> bool {
116        debug_assert!(self.stack.len() > 1);
117        let frame = self.active_frame();
118        let frame = &mut self.stack_frames[frame];
119        !core::mem::replace(&mut frame.from_cdcl, true)
120    }
121
122    pub(super) fn active_frame(&self) -> StackIdx {
123        *self.stack.last().unwrap()
124    }
125
126    /// For use in CDCL only.
127    pub(super) fn pre_active_frame(&self) -> StackIdx {
128        self.stack[self.stack.len() - 2]
129    }
130
131    pub(super) fn is_speculative(&self) -> bool {
132        self.stack_frames[self.active_frame()].from_cdcl
133    }
134
135    pub(super) fn is_alive(&self, frame: StackIdx) -> bool {
136        self[frame].active.status().is_alive()
137    }
138
139    #[cfg(any())]
140    pub(super) fn is_global(&self, frame: StackIdx) -> bool {
141        frame == Self::ZERO_FRAME
142    }
143}
144
145impl std::ops::Index<StackIdx> for Stack {
146    type Output = StackFrame;
147    fn index(&self, idx: StackIdx) -> &Self::Output {
148        &self.stack_frames[idx]
149    }
150}
151
152pub trait HasFrame {
153    fn frame(self, parser: &Z3Parser) -> StackIdx;
154}
155
156macro_rules! impl_has_frame {
157    ($($ty:ty),*) => {
158        $(impl HasFrame for $ty {
159            fn frame(self, parser: &Z3Parser) -> StackIdx {
160                parser[self].frame
161            }
162        })*
163    };
164}
165
166impl_has_frame!(ENodeIdx, MatchIdx, InstIdx, ProofIdx, CdclIdx);
smt_scope/parsers/z3/stack.rs

smt_scope/parsers/z3/
stack.rs
