Trait Stack

Source

pub trait Stack {
    // Required methods
    fn push(&mut self) -> Result<()>;
    fn pop_n(&mut self, n: usize) -> Result<()>;

    // Provided method
    fn pop(&mut self) -> Result<()> { ... }
}

Expand description

Trait to model entities that can push and pop their state on a stack structure.

Many components in formally allow to push and pop their state as a stack structure, most prominently SMT solvers from the smt crate. This trait abstracts this capability.

Since the logic to support these operations can sometimes be factored out, we also provide the Stacked type to help implementing Stack on your own data structure.

Implementors should note that popping out a number of frames equal or larger than the number of frames pushed should, by convention, result into an object equivalent to its Default value.