Enum Statement 

pub enum Statement<'a> {
    Domain(Located<'a, &'a str>),
    Import {
        path: Located<'a, &'a str>,
        alias: Option<Located<'a, &'a str>>,
    },
    Fact(Located<'a, Atom<'a>>),
    Negation(Located<'a, Atom<'a>>),
    Assume(Located<'a, Literal<'a>>),
    Set {
        name: Located<'a, &'a str>,
        elements: Vec<Located<'a, &'a str>>,
    },
    Close {
        relation: Located<'a, &'a str>,
        kind: CloseKind,
    },
    Premise {
        name: Located<'a, &'a str>,
        quant: Option<Quant<'a>>,
        body: Body<'a>,
    },
    Rule {
        name: Located<'a, &'a str>,
        quant: Option<Quant<'a>>,
        body: Body<'a>,
    },
    Check {
        subject: Option<Located<'a, &'a str>>,
        bidirectional: bool,
    },
}

A top-level statement.

Variants

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

DOMAIN <name> — declare the domain this file’s atoms belong to. Required once per file, as the first statement; it is the identity namespace into which bare atoms fall.

Import

IMPORT "path" [AS <alias>] — reuse another source (resolved by the compiler). The optional alias is the local name the imported domain is referenced by; without it, the imported file’s own declared domain name is used.

Fields

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

The quoted source path.

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

The local alias for the imported domain, if AS <alias> was given.

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.

Set

SET <name> then one element identifier per line — declare a finite set to quantify a PREMISE/RULE over via FOR EACH <binder> IN <name>.

Fields

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

The set’s name (referenced by FOR EACH … IN <name>).

elements: Vec<Located<'a, &'a str>>

Its elements, one per line (at least one).

Close

CLOSE <relation> TRANSITIVE — close a relation’s FACT pairs under the given kind at compile time (a graph operation, no solver cost). A cycle is a compile error.

Fields

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

The relation predicate to close (e.g. depends_on).

kind: CloseKind

Which closure to apply.

Premise

PREMISE <name> [FOR EACH …]: ... — a checked first principle, optionally quantified over a declared set.

Fields

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

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

quant: Option<Quant<'a>>

An optional FOR EACH … IN … header quantifier (at most one).

body: Body<'a>

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

Rule

RULE <name> [FOR EACH …]: ... — a fact-producing inference rule.

Fields

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

The rule’s label.

quant: Option<Quant<'a>>

An optional FOR EACH … IN … header quantifier (at most one).

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>