Enum EqualityExpl 

pub enum EqualityExpl {
    Root {
        id: ENodeIdx,
    },
    Literal {
        from: ENodeIdx,
        eq: LitIdx,
        to: ENodeIdx,
    },
    Congruence {
        from: ENodeIdx,
        arg_eqs: Box<[(ENodeIdx, ENodeIdx)]>,
        to: ENodeIdx,
        uses: Vec<BoxSlice<EqTransIdx>>,
    },
    Theory {
        from: ENodeIdx,
        theory: TheoryKind,
        to: ENodeIdx,
    },
    Axiom {
        from: ENodeIdx,
        to: ENodeIdx,
    },
    Unknown {
        kind: IString,
        from: ENodeIdx,
        args: BoxSlice<IString>,
        to: ENodeIdx,
    },
}

A Z3 equality explanation. Root represents a term that is a root of its equivalence class. All other variants represent an equality between two terms and where it came from.

Variants

Root

Fields

id: ENodeIdx

Literal

Fields

from: ENodeIdx

eq: LitIdx

The equality term this is from

to: ENodeIdx

Congruence

Fields

from: ENodeIdx

arg_eqs: Box<[(ENodeIdx, ENodeIdx)]>

to: ENodeIdx

uses: Vec<BoxSlice<EqTransIdx>>

The arg_eqs need to be evaluated whenever this is used.

Theory

Fields

from: ENodeIdx

theory: TheoryKind

to: ENodeIdx

Axiom

Fields

from: ENodeIdx

to: ENodeIdx

Unknown

Fields

kind: IString

from: ENodeIdx

args: BoxSlice<IString>

to: ENodeIdx

Implementations

impl EqualityExpl

pub fn is_trivial(&self) -> bool

pub fn from(&self) -> ENodeIdx

pub fn to(&self) -> ENodeIdx

pub fn walk_any(&self, from: ENodeIdx) -> ENodeIdx

pub fn walk(&self, from: ENodeIdx, fwd: bool) -> Option<ENodeIdx>

pub fn kind(&self) -> Result<&'static str, IString>

pub fn kind_str<'a>(&self, strings: &'a StringTable) -> &'a str

Trait Implementations

impl Clone for EqualityExpl

fn clone(&self) -> EqualityExpl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EqualityExpl

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

Formats the value using the given formatter.

impl PartialEq for EqualityExpl

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for EqualityExpl