Skip to main content

EquivalenceProver

bitwright::mba

Trait EquivalenceProver 

Source 
pub trait EquivalenceProver: Send + Sync {
    // Required methods
    fn id(&self) -> &str;
    fn prove_equal(
        &self,
        a: &MbaExpr,
        b: &MbaExpr,
        budget: &MbaBudget,
    ) -> Verdict;
}
Expand description

A backend that proves two MBA expressions equal.

Required Methods§

Source

fn id(&self) -> &str

A stable name (it keys the caches).

Source

fn prove_equal(&self, a: &MbaExpr, b: &MbaExpr, budget: &MbaBudget) -> Verdict

Decides whether a and b are equal on every input.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§