Enum IrForm 

pub enum IrForm {
    Predicate {
        relation: Spur,
        args: Vec<IrTerm>,
    },
    ForAll(Spur, Box<IrForm>),
    Exists(Spur, Box<IrForm>),
    And(Box<IrForm>, Box<IrForm>),
    Or(Box<IrForm>, Box<IrForm>),
    Not(Box<IrForm>),
    Past(Box<IrForm>),
    Present(Box<IrForm>),
    Future(Box<IrForm>),
    Obligatory(Box<IrForm>),
    Permitted(Box<IrForm>),
    Count {
        var: Spur,
        count: u32,
        body: Box<IrForm>,
    },
    Biconditional(Box<IrForm>, Box<IrForm>),
    Xor(Box<IrForm>, Box<IrForm>),
}

The Well-Formed Formulas (WFFs) of our First-Order Logic engine.

Variants

Predicate

An n-ary predicate: P(t1, t2, …, tn)

Fields

relation: Spur

args: Vec<IrTerm>

ForAll(Spur, Box<IrForm>)

Universal quantification: ∀x. P(x)

Exists(Spur, Box<IrForm>)

Existential quantification: ∃x. P(x)

And(Box<IrForm>, Box<IrForm>)

Logical Conjunction: A ∧ B

Or(Box<IrForm>, Box<IrForm>)

Logical Disjunction: A ∨ B

Not(Box<IrForm>)

Logical Negation: ¬A

Past(Box<IrForm>)

Past tense wrapper (past P): P was true.

Present(Box<IrForm>)

Present tense wrapper (now P): P is true now.

Future(Box<IrForm>)

Future tense wrapper (future P): P will be true.

Obligatory(Box<IrForm>)

Deontic obligation (must P): P ought to be true.

Permitted(Box<IrForm>)

Deontic permission (may P): P is permitted.

Count

Exactly count distinct x satisfy body. Count(var, count, body)

Fields

var: Spur

count: u32

body: Box<IrForm>

Biconditional(Box<IrForm>, Box<IrForm>)

Biconditional: A ↔ B (expanded at flattening to And(Or(Not(A), B), Or(Not(B), A)))

Xor(Box<IrForm>, Box<IrForm>)

Exclusive or: A ⊕ B (expanded at flattening to And(Or(A, B), Not(And(A, B))))

Trait Implementations

impl Clone for IrForm

fn clone(&self) -> IrForm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IrForm

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

Formats the value using the given formatter.

impl PartialEq for IrForm

fn eq(&self, other: &IrForm) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for IrForm