Struct ProofStep 

pub struct ProofStep { /* private fields */ }

A single step in a Proof.

Each step records:

• The Formula derived at this step (ProofStep::conclusion)
• The ProofRule used to derive it (ProofStep::rule)
• The indices (into Proof::steps) of the premises this step depends on (ProofStep::premises)
• A discovery-order counter assigned by Vampire (ProofStep::discovery_order)

Implementations

impl ProofStep

pub fn conclusion(&self) -> Formula

Returns the formula derived at this step.

pub fn rule(&self) -> ProofRule

Returns the inference rule used to derive this step.

pub fn premises(&self) -> &[usize]

Returns the indices of the premises this step was derived from.

Each value is an index into the Proof::steps slice (i.e. the position of the premise among the steps that actually appear in the proof, not its ProofStep::discovery_order).

pub fn discovery_order(&self) -> u32

Returns Vampire’s internal discovery-order ID for this step.

As Vampire searches for a proof it assigns every derived fact a monotonically increasing numeric ID. When the proof is extracted, only the facts that were actually used in the refutation are included, so there may be gaps in the sequence. The steps in Proof::steps are sorted by this value, which also gives a valid topological ordering of the proof DAG.

Trait Implementations

impl Clone for ProofStep

fn clone(&self) -> ProofStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofStep

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

Formats the value using the given formatter.

impl Hash for ProofStep

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for ProofStep

fn eq(&self, other: &ProofStep) -> 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 Eq for ProofStep

impl StructuralPartialEq for ProofStep