Struct FrameSequence 

pub struct FrameSequence { /* private fields */ }

The sequence of frames maintained by PDR.

F₀ contains the initial-state clauses. F₁..Fₖ accumulate blocking clauses as cubes are blocked during the strengthen phase.

Implementations

impl FrameSequence

pub fn new() -> Self

Create an empty frame sequence.

pub fn push(&mut self, frame: Frame)

Add a frame to the sequence.

pub fn frontier(&self) -> usize

Current frontier level (index of the last frame).

pub fn len(&self) -> usize

Number of frames.

pub fn frame(&self, level: usize) -> &Frame

Access a frame by index.

pub fn frame_mut(&mut self, level: usize) -> &mut Frame

Mutable access to a frame by index.

pub fn add_blocked_clause(&mut self, level: usize, clause: Vec<Lit>)

Add a blocking clause to a specific frame level. For monotonicity, also add to all frames at lower levels (1..=level).

pub fn check_convergence(&self) -> Option<usize>

Check convergence: if Fᵢ = Fᵢ₊₁ for any i ≥ 1, return Some(i).

Compares frames by their sorted clause sets (order-independent).

Trait Implementations

impl Default for FrameSequence

fn default() -> Self

Returns the “default value” for a type.