Struct FrameManager 

pub struct FrameManager { /* private fields */ }

Global frame manager for all predicates

Implementations

impl FrameManager

pub fn new() -> Self

Create a new frame manager

pub fn get_or_create(&mut self, pred: PredId) -> &mut PredicateFrames

Get or create frames for a predicate

pub fn get(&self, pred: PredId) -> Option<&PredicateFrames>

Get frames for a predicate

pub fn get_mut(&mut self, pred: PredId) -> Option<&mut PredicateFrames>

Get mutable frames for a predicate

pub fn current_level(&self) -> u32

Get the current global level

pub fn next_level(&mut self)

Advance to the next level

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

Add a lemma for a predicate at a level

pub fn is_fixpoint(&self) -> bool

Check for fixpoint: all lemmas at current level are inductive

pub fn propagate(&mut self) -> bool

Try to propagate all frames Returns true if a fixpoint is detected

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

Compress all frames by removing old lemmas Returns the total number of lemmas removed

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

Get total memory usage statistics across all predicates

pub fn reset(&mut self)

Reset all frames

pub fn stats(&self) -> FrameStats

Get statistics

Trait Implementations

impl Debug for FrameManager

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

Formats the value using the given formatter.

impl Default for FrameManager

fn default() -> Self

Returns the “default value” for a type.