Type Alias NCommand

Source

pub type NCommand = GenericNCommand<String, String>;

Aliased Type§

pub enum NCommand {
Show 19 variants    Sort {
        span: Span,
        name: String,
        presort_and_args: Option<(String, Vec<GenericExpr<String, String>>)>,
        uf: Option<String>,
        proof_func: Option<String>,
        unionable: bool,
    },
    Function(GenericFunctionDecl<String, String>),
    AddRuleset(Span, String),
    UnstableCombinedRuleset(Span, String, Vec<String>),
    NormRule {
        rule: GenericRule<String, String>,
    },
    CoreAction(GenericAction<String, String>),
    Extract(Span, GenericExpr<String, String>, GenericExpr<String, String>),
    RunSchedule(GenericSchedule<String, String>),
    PrintOverallStatistics(Span, Option<String>),
    Check(Span, Vec<GenericFact<String, String>>),
    PrintFunction(Span, String, Option<usize>, Option<String>, PrintFunctionMode),
    ProveExists(Span, String),
    PrintSize(Span, Option<String>),
    Output {
        span: Span,
        file: String,
        exprs: Vec<GenericExpr<String, String>>,
    },
    Push(usize),
    Pop(Span, usize),
    Fail(Span, Box<GenericNCommand<String, String>>),
    Input {
        span: Span,
        name: String,
        file: String,
    },
    UserDefined(Span, String, Vec<GenericExpr<String, String>>),
}

Variants§

§

Sort

Fields

§span: Span

§name: String

§presort_and_args: Option<(String, Vec<GenericExpr<String, String>>)>

§uf: Option<String>

The name of the union-find function for this sort. Used in term encoding to canonicalize values during extraction.

§proof_func: Option<String>

The name of the proof function for this sort. Set by proof desugaring to record where proofs are stored for this sort.

§unionable: bool

Whether values of this sort can be unioned. Defaults to true for user-defined sorts. Set to false for relations and term tables that should not allow union.

§