formally_support/
stack.rs

1//
2// ::formally - the open-source formal methods toolchain
3//
4// Copyright (c) 2025 Nicola Gigante
5//
6// Permission is hereby granted, free of charge, to any person obtaining a copy
7// of this software and associated documentation files (the "Software"), to deal
8// in the Software without restriction, including without limitation the rights
9// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10// copies of the Software, and to permit persons to whom the Software is
11// furnished to do so, subject to the following conditions:
12//
13// The above copyright notice and this permission notice shall be included in
14// all copies or substantial portions of the Software.
15//
16// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22// SOFTWARE.
23//
24
25use crate::*;
26use std::ops::{Deref, DerefMut};
27
28/// Trait to model entities that can push and pop their state on a stack structure.
29///
30/// Many components in `formally` allow to push and pop their state as a stack structure, most
31/// prominently SMT solvers from the `smt` crate. This trait abstracts this capability.
32///
33/// Since the logic to support these operations can sometimes be factored out, we also provide the
34/// [Stacked] type to help implementing [Stack] on your own data structure.
35///
36/// Implementors should note that popping out a number of frames equal or larger than the number of
37/// frames pushed should, by convention, result into an object equivalent to its [Default] value.
38pub trait Stack {
39    /// Push the current state of the object to the stack.
40    fn push(&mut self) -> Result<()>;
41
42    /// Pop `n` frames from the stack, restoring the state of the `n`th topmost frame.
43    ///
44    /// It is allowed to provide a value of `n` larger than the number of frames.
45    fn pop_n(&mut self, n: usize) -> Result<()>;
46
47    /// Shortcut for `pop_n(1)`
48    fn pop(&mut self) -> Result<()> {
49        self.pop_n(1)
50    }
51}
52
53/// A helper type to implement the [Stack] trait
54///
55/// This type is a wrapper for any clonable type `T` that implements [Stack] on top of it.
56/// Access to the current topmost frame is granted via [Deref] and [DerefMut].
57///
58/// The stack structure is implemented as a vector where the current value of the inner object is
59/// pushed when [Stack::push] is called, and popped when [Stack::pop_n] is called. This means that
60/// types used with [Stacked] should be *efficiently* clonable. Efficient clonability is often
61/// achieved in `formally` by using immutable/persistent data structures, usually from the `rpds`
62/// crate.
63///
64/// To construct a [Stacked] object, the underlying type must implement [Default]. The [Stack]
65/// traits suggests that popping out more frames than those pushed should result into an object
66/// equivalent to the [Default] instance. This requirement is satisfied by [Stacked].
67#[derive(Clone)]
68pub struct Stacked<T> {
69    current: T,
70    stack: rpds::VectorSync<T>,
71}
72
73impl<T: Clone + Default> Default for Stacked<T> {
74    fn default() -> Self {
75        Stacked {
76            current: T::default(),
77            stack: rpds::Vector::new_sync(),
78        }
79    }
80}
81
82impl<T: Default> Stacked<T> {
83    /// Creates a new default-valued stacked object.
84    pub fn new(current: T) -> Self {
85        Self {
86            current,
87            stack: Default::default(),
88        }
89    }
90
91    /// Turns the stacked into the current topmost frame.
92    pub fn into_current(self) -> T {
93        self.current
94    }
95}
96
97impl<T: Clone + Default> Stack for Stacked<T> {
98    fn push(&mut self) -> Result<()> {
99        self.stack.push_back_mut(self.current.clone());
100        Ok(())
101    }
102
103    fn pop_n(&mut self, n: usize) -> Result<()> {
104        let mut i = n;
105        while !self.stack.is_empty() && i > 0 {
106            self.current = std::mem::take(self.stack.get_mut(self.stack.len() - 1).unwrap());
107            self.stack.drop_last_mut();
108            i -= 1;
109        }
110
111        if self.stack.is_empty() && i > 0 {
112            self.current = Default::default();
113        }
114
115        Ok(())
116    }
117}
118
119impl<T: Clone + Default> Deref for Stacked<T> {
120    type Target = T;
121
122    fn deref(&self) -> &Self::Target {
123        &self.current
124    }
125}
126
127impl<T: Clone + Default> DerefMut for Stacked<T> {
128    fn deref_mut(&mut self) -> &mut Self::Target {
129        &mut self.current
130    }
131}
132
133#[cfg(test)]
134mod tests {
135    use super::*;
136
137    #[test]
138    fn stacked() -> Result<()> {
139        let mut stacked: Stacked<Vec<i32>> = Stacked::default();
140
141        (*stacked).push(42);
142
143        assert_eq!(*stacked, vec![42]);
144
145        stacked.push()?;
146
147        (*stacked).push(37);
148
149        assert_eq!(*stacked, vec![42, 37]);
150
151        stacked.pop()?;
152
153        assert_eq!(*stacked, vec![42]);
154
155        stacked.pop()?;
156
157        assert!(stacked.is_empty());
158        
159        Ok(())
160    }
161}
formally_support/stack.rs

formally_support/
stack.rs
