Enum z3tracer::syntax::Equality

pub enum Equality {
    Root,
    Literal(Ident, Ident),
    Congruence(Vec<(Ident, Ident)>, Ident),
    Theory(String, Ident),
}

Description of an E-matching step.

Variants

Root

Literal(Ident, Ident)

Congruence(Vec<(Ident, Ident)>, Ident)

Theory(String, Ident)

Trait Implementations

impl Clone for Equality

fn clone(&self) -> Equality

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Equality

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

Formats the value using the given formatter.

impl Eq for Equality

impl PartialEq<Equality> for Equality

fn eq(&self, other: &Equality) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Equality) -> bool

This method tests for !=.

impl StructuralEq for Equality

impl StructuralPartialEq for Equality

impl<'a, F, E> Visitor<'a, F, E> for Equality where
    F: FnMut(&'a Ident) -> Result<(), E>, 

fn visit(&'a self, f: &mut F) -> Result<(), E>