Struct InstrumentedCC 

pub struct InstrumentedCC {
    pub cc: CongruenceClosure,
    pub stats: CongrClosureStats,
}

A congruence closure augmented with statistics collection.

Fields

cc: CongruenceClosure

Inner closure.

stats: CongrClosureStats

Collected statistics.

Implementations

impl InstrumentedCC

pub fn new() -> Self

Create a new instrumented congruence closure.

pub fn add_equality(&mut self, e1: Expr, e2: Expr)

Add an equality and record the operation.

pub fn are_equal(&mut self, e1: &Expr, e2: &Expr) -> bool

Check equality (delegates to inner CC).

pub fn reset(&mut self)

Reset everything.

pub fn num_classes(&mut self) -> usize

Number of equivalence classes.

Trait Implementations

impl Default for InstrumentedCC

fn default() -> Self

Returns the “default value” for a type.