Enum EvidenceNodeRef 

pub enum EvidenceNodeRef<'a> {
    Satisfaction(&'a SatTrace),
    Failure(&'a Witness),
}

Variants

Satisfaction(&'a SatTrace)

Failure(&'a Witness)

Implementations

impl<'a> EvidenceNodeRef<'a>

pub fn constraint_id(self) -> ShapeId

pub fn node(self) -> Option<&'a Term>

The node this judgment is about, completing the (constraint, node) address the shape memo (validate.rs) is keyed by.

None only for SatTrace::Irrefutable, which is ⊤ and so is about no node at all.

pub fn status(self) -> EvaluationStatus

pub fn evidence_kind(self) -> EvidenceKind

pub fn kind(self) -> &'static str

pub fn children(self) -> Vec<Self>

Immediate evidence children in stable semantic order.

This is the shared grammar of failure and satisfaction evidence. Not crosses polarity; qualified counts can contain both satisfaction traces for matches and failure witnesses for rejected candidates. Callers that only need structure should use this instead of maintaining another variant-specific recursive walk.

Trait Implementations

impl<'a> Clone for EvidenceNodeRef<'a>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Copy for EvidenceNodeRef<'a>

impl<'a> Debug for EvidenceNodeRef<'a>

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

Formats the value using the given formatter.