Struct PredicateFrames 

pub struct PredicateFrames {
    pub pred: PredId,
    /* private fields */
}

Frame sequence for a single predicate transformer

Fields

pred: PredId

The predicate this frame sequence is for

Implementations

impl PredicateFrames

pub fn new(pred: PredId) -> Self

Create a new frame sequence for a predicate

pub fn num_frames(&self) -> u32

Get the number of frames

pub fn add_frame(&mut self)

Add a new frame

pub fn add_lemma(&mut self, formula: TermId, level: u32) -> LemmaId

Add a lemma at a given level

pub fn add_background(&mut self, formula: TermId) -> LemmaId

Add a background invariant

pub fn get_lemma(&self, id: LemmaId) -> Option<&Lemma>

Get a lemma by ID

pub fn get_lemma_mut(&mut self, id: LemmaId) -> Option<&mut Lemma>

Get a mutable lemma by ID

pub fn active_lemmas(&self) -> impl Iterator<Item = &Lemma>

Get all active lemmas

pub fn lemmas_at_level(&self, level: u32) -> impl Iterator<Item = &Lemma>

Get lemmas at a specific level

pub fn lemmas_geq_level(&self, level: u32) -> impl Iterator<Item = &Lemma>

Get lemmas at or above a level (for frame queries)

pub fn inductive_lemmas(&self) -> impl Iterator<Item = &Lemma>

Get all inductive lemmas

pub fn background_invariants(&self) -> impl Iterator<Item = &Lemma>

Get background invariants

pub fn propagate(&mut self, id: LemmaId, new_level: u32) -> bool

Propagate a lemma to a higher level

pub fn propagate_to_infinity(&mut self, from_level: u32)

Propagate lemmas to infinity (inductive)

pub fn propagate_level(&mut self, level: u32) -> bool

Try to propagate all lemmas at a level to the next level Returns true if all lemmas were successfully propagated

pub fn deactivate(&mut self, id: LemmaId)

Deactivate a lemma (mark as subsumed)

pub fn is_active(&self, id: LemmaId) -> bool

Check if a lemma is active

pub fn num_active_lemmas(&self) -> usize

Get number of active lemmas

pub fn num_inductive(&self) -> usize

Get number of inductive lemmas

pub fn remove_subsumed_syntactic(&mut self) -> usize

Remove subsumed lemmas using syntactic subsumption Returns the number of lemmas removed

pub fn sort_lemmas(&mut self)

Sort lemmas by level (for efficient queries)

pub fn clear(&mut self)

Clear all lemmas (reset)

pub fn compress(&mut self, keep_above_level: u32) -> usize

Compress frames by removing lemmas at lower levels that have been pushed This is a memory optimization to reduce the number of stored lemmas Returns the number of lemmas removed

pub fn memory_stats(&self) -> (usize, usize, usize)

Get memory usage statistics

Trait Implementations

impl Debug for PredicateFrames

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.