Struct QuantifiedFormula 

pub struct QuantifiedFormula {
    pub term: TermId,
    pub bound_vars: SmallVec<[(Spur, SortId); 4]>,
    pub body: TermId,
    pub is_universal: bool,
    pub nesting_depth: u32,
    pub instantiation_count: usize,
    pub max_instantiations: usize,
    pub generation: u32,
    pub weight: f64,
    pub patterns: Vec<Vec<TermId>>,
    pub is_flattened: bool,
    pub specialized_body: Option<TermId>,
}

A quantified formula tracked by MBQI

Fields

term: TermId

The original quantified term

bound_vars: SmallVec<[(Spur, SortId); 4]>

Bound variables (name, sort)

body: TermId

The body of the quantifier

is_universal: bool

Whether this is universal (true) or existential (false)

nesting_depth: u32

Quantifier nesting depth

instantiation_count: usize

Number of times this quantifier has been instantiated

max_instantiations: usize

Maximum allowed instantiations for this quantifier

generation: u32

Generation number (for tracking term age)

weight: f64

Weight for prioritization

patterns: Vec<Vec<TermId>>

Patterns for E-matching (if available)

is_flattened: bool

Whether this quantifier has been flattened

specialized_body: Option<TermId>

Cached specialized body (None if not yet specialized)

Implementations

impl QuantifiedFormula

pub fn new( term: TermId, bound_vars: SmallVec<[(Spur, SortId); 4]>, body: TermId, is_universal: bool, ) -> Self

Create a new tracked quantified formula

pub fn with_params( term: TermId, bound_vars: SmallVec<[(Spur, SortId); 4]>, body: TermId, is_universal: bool, max_instantiations: usize, weight: f64, ) -> Self

Create with custom parameters

pub fn can_instantiate(&self) -> bool

Check if we can instantiate more

pub fn num_vars(&self) -> usize

Get the number of bound variables

pub fn var_name(&self, idx: usize) -> Option<Spur>

Get variable name by index

pub fn var_sort(&self, idx: usize) -> Option<SortId>

Get variable sort by index

pub fn record_instantiation(&mut self)

Record an instantiation

pub fn priority_score(&self) -> f64

Calculate priority score (higher = more important)

Trait Implementations

impl Clone for QuantifiedFormula

fn clone(&self) -> QuantifiedFormula

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for QuantifiedFormula

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

Formats the value using the given formatter.