Enum NodeKind

pub enum NodeKind {
    Instantiation(InstIdx),
    ENode(ENodeIdx),
    GivenEquality(EqGivenIdx, Option<NonMaxU32>),
    TransEquality(EqTransIdx),
    Proof(ProofIdx),
    Cdcl(CdclIdx),
}

Variants

Instantiation(InstIdx)

Corresponds to InstIdx.

Parents: (small) arbitrary count, will always be ENode or TransEquality.
Children: (small) arbitrary count, will always be ENode.

ENode(ENodeIdx)

Corresponds to ENodeIdx.

Parents: will always have 0 or 1 parents, if 1 then this will be an Instantiation.
Children: (large) arbitrary count, will always be either Instantiation or GivenEquality of type EqualityExpl::Literal.

GivenEquality(EqGivenIdx, Option<NonMaxU32>)

Corresponds to EqGivenIdx.

Parents: will always have 0 or 1 parents, if 1 then this will be an ENode or a TransEquality depending on if it’s a Literal or Congruence resp.
Children: (small) arbitrary count, will always be TransEquality of type.

TransEquality(EqTransIdx)

Corresponds to EqTransIdx.

Parents: (small) arbitrary count, will always be GivenEquality or TransEquality. The number of immediately reachable GivenEquality can be found in TransitiveExpl::given_len.
Children: (large) arbitrary count, can be GivenEquality, TransEquality or Instantiation.

Proof(ProofIdx)

Corresponds to ProofIdx.

Parents: (large) arbitrary count, will always be Proof or Instantiation. Children: (small?) arbitrary count, will always be Proof.

Cdcl(CdclIdx)

Corresponds to CdclIdx. Only connected to other Cdcl nodes.

Parents: will always have between 0 and 2 parents, if 2 then only one is a real edge and the other is a backtracking edge. Children: (generally small) arbitrary count, depends on how many times we backtracked here.

Implementations

impl NodeKind

pub fn inst(&self) -> Option<InstIdx>

pub fn enode(&self) -> Option<ENodeIdx>

pub fn eq_given(&self) -> Option<(EqGivenIdx, Option<NonMaxU32>)>

pub fn eq_trans(&self) -> Option<EqTransIdx>

pub fn proof(&self) -> Option<ProofIdx>

pub fn cdcl(&self) -> Option<CdclIdx>

pub fn reconnect_child(&self, _child: &Self) -> bool

Same as reconnect_parents but for children. Do we reconnect hidden children of this visible node or just this node itself?

Trait Implementations

impl Clone for NodeKind

fn clone(&self) -> NodeKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NodeKind

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

Formats the value using the given formatter.

impl Display for NodeKind

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

Formats the value using the given formatter.

impl Copy for NodeKind