Enum Statement 

pub enum Statement<'a> {
    Import(Located<'a, &'a str>),
    Fact(Located<'a, Atom<'a>>),
    Negation(Located<'a, Atom<'a>>),
    Assume(Located<'a, Literal<'a>>),
    Premise {
        name: Located<'a, &'a str>,
        body: Body<'a>,
    },
    Rule {
        name: Located<'a, &'a str>,
        body: Body<'a>,
    },
    Check {
        subject: Option<Located<'a, &'a str>>,
        bidirectional: bool,
    },
}

A top-level statement.

Variants

Import(Located<'a, &'a str>)

IMPORT "path" — reuse another source (resolved by the compiler).

Fact(Located<'a, Atom<'a>>)

FACT <atom> — a TRUE assertion.

Negation(Located<'a, Atom<'a>>)

NOT <atom> — a FALSE assertion.

Assume(Located<'a, Literal<'a>>)

ASSUME [NOT] <atom> — a soft (retractable) assertion. Same shape as a FACT/NOT, but it is a hypothesis, not a commitment: when the assumptions cannot all hold the solver names which to drop, and it never blames a FACT/PREMISE. The Literal carries the optional NOT.

Premise

PREMISE <name>: ... — a checked first principle.

Fields

name: Located<'a, &'a str>

The premise’s label (a per-source name, not a global identifier).

body: Body<'a>

The constraint itself: a list body or a WHEN … THEN implication.

Rule

RULE <name>: ... — a fact-producing inference rule.

Fields

name: Located<'a, &'a str>

The rule’s label.

body: Body<'a>

Always an implication body (the grammar forbids a list body here).

Check

CHECK [subject] [BIDIRECTIONAL] — a query.

Fields

subject: Option<Located<'a, &'a str>>

Restrict the report to this subject; None checks everything.

bidirectional: bool

true enables the backward (all-SAT) pass for UNDERDETERMINED.

Trait Implementations

impl<'a> Clone for Statement<'a>

fn clone(&self) -> Statement<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for Statement<'a>

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

Formats the value using the given formatter.

impl<'a> PartialEq for Statement<'a>

fn eq(&self, other: &Statement<'a>) -> 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<'a> StructuralPartialEq for Statement<'a>