Struct QuantifiedFormula 

pub struct QuantifiedFormula {
    pub term: TermId,
    pub bound_vars: SmallVec<[(Spur, SortId); 2]>,
    pub body: TermId,
    pub universal: bool,
    pub instantiation_count: usize,
    pub max_instantiations: usize,
}

A quantified formula tracked by MBQI

Fields

term: TermId

The original quantified term

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

Bound variables (name, sort)

body: TermId

The body of the quantifier

universal: bool

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

instantiation_count: usize

Number of times this quantifier has been instantiated

max_instantiations: usize

Maximum allowed instantiations

Implementations

impl QuantifiedFormula

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

Create a new tracked quantified formula

pub fn can_instantiate(&self) -> bool

Check if we can instantiate more

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.