Enum CommandOutput 

pub enum CommandOutput {
    PrintFunctionSize(usize),
    PrintAllFunctionsSize(Vec<(String, usize)>),
    ExtractBest(TermDag, DefaultCost, TermId),
    ExtractVariants(TermDag, Vec<TermId>),
    ProveExists {
        proof_store: ProofStore,
        proof_id: ProofId,
    },
    OverallStatistics(RunReport),
    PrintFunction(Function, TermDag, Vec<(TermId, TermId)>, PrintFunctionMode),
    RunSchedule(RunReport),
    UserDefined(Arc<dyn UserDefinedCommandOutput>),
}

Output from a command.

Variants

PrintFunctionSize(usize)

The size of a function

PrintAllFunctionsSize(Vec<(String, usize)>)

The name of all functions and their sizes

ExtractBest(TermDag, DefaultCost, TermId)

The best term found after extracting

ExtractVariants(TermDag, Vec<TermId>)

The variants of a function found after extracting. Like normal extraction, but has to choose one extraction per e-node in the e-class.

ProveExists

A high-level proof witnessing constructor existence

Fields

proof_store: ProofStore

proof_id: ProofId

OverallStatistics(RunReport)

The report from all runs

PrintFunction(Function, TermDag, Vec<(TermId, TermId)>, PrintFunctionMode)

A printed function and all its values

RunSchedule(RunReport)

The report from a single run

UserDefined(Arc<dyn UserDefinedCommandOutput>)

A user defined output

Implementations

impl CommandOutput

pub fn snapshot_stable_under_proof_encoding(outputs: &[CommandOutput]) -> String

Render command outputs to a string that is identical whether the program ran normally or under proof encoding (--proofs). Drops outputs that legitimately differ or are non-deterministic (timing, PrintFunction per #793, extraction variants) and reduces ExtractBest to its cost.

Trait Implementations

impl Clone for CommandOutput

fn clone(&self) -> CommandOutput

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CommandOutput

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

Formats the value using the given formatter.

impl Display for CommandOutput

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

Format the command output for display, ending with a newline.