Struct BatchDefEqChecker 

pub struct BatchDefEqChecker<'env> { /* private fields */ }

A batch checker that can check multiple pairs efficiently.

Implementations

impl<'env> BatchDefEqChecker<'env>

pub fn new(env: &'env Environment) -> Self

Create a new batch checker.

pub fn check(&mut self, t: &Expr, s: &Expr) -> bool

Check definitional equality for a single pair.

pub fn check_all(&mut self, pairs: &[(Expr, Expr)]) -> bool

Check all pairs in a list; returns true iff all pairs are def-equal.

pub fn check_any(&mut self, pairs: &[(Expr, Expr)]) -> bool

Check any pair in a list; returns true iff at least one pair is def-equal.

pub fn count_equal(&mut self, pairs: &[(Expr, Expr)]) -> usize

Count how many pairs in the list are definitionally equal.

pub fn reset(&mut self)

Reset the checker (clears caches).