Type Alias TLExpr 

pub type TLExpr = TLExpr;

Type alias for TensorLogic expressions

Aliased Type

pub enum TLExpr {
    Pred {
        name: String,
        args: Vec<Term>,
    },
    And(Box<TLExpr>, Box<TLExpr>),
    Or(Box<TLExpr>, Box<TLExpr>),
    Not(Box<TLExpr>),
    Exists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    ForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    Imply(Box<TLExpr>, Box<TLExpr>),
    Score(Box<TLExpr>),
    Add(Box<TLExpr>, Box<TLExpr>),
    Sub(Box<TLExpr>, Box<TLExpr>),
    Mul(Box<TLExpr>, Box<TLExpr>),
    Div(Box<TLExpr>, Box<TLExpr>),
    Pow(Box<TLExpr>, Box<TLExpr>),
    Mod(Box<TLExpr>, Box<TLExpr>),
    Min(Box<TLExpr>, Box<TLExpr>),
    Max(Box<TLExpr>, Box<TLExpr>),
    Abs(Box<TLExpr>),
    Floor(Box<TLExpr>),
    Ceil(Box<TLExpr>),
    Round(Box<TLExpr>),
    Sqrt(Box<TLExpr>),
    Exp(Box<TLExpr>),
    Log(Box<TLExpr>),
    Sin(Box<TLExpr>),
    Cos(Box<TLExpr>),
    Tan(Box<TLExpr>),
    Eq(Box<TLExpr>, Box<TLExpr>),
    Lt(Box<TLExpr>, Box<TLExpr>),
    Gt(Box<TLExpr>, Box<TLExpr>),
    Lte(Box<TLExpr>, Box<TLExpr>),
    Gte(Box<TLExpr>, Box<TLExpr>),
    IfThenElse {
        condition: Box<TLExpr>,
        then_branch: Box<TLExpr>,
        else_branch: Box<TLExpr>,
    },
    Constant(f64),
    Aggregate {
        op: AggregateOp,
        var: String,
        domain: String,
        body: Box<TLExpr>,
        group_by: Option<Vec<String>>,
    },
    Let {
        var: String,
        value: Box<TLExpr>,
        body: Box<TLExpr>,
    },
    Box(Box<TLExpr>),
    Diamond(Box<TLExpr>),
    Next(Box<TLExpr>),
    Eventually(Box<TLExpr>),
    Always(Box<TLExpr>),
    Until {
        before: Box<TLExpr>,
        after: Box<TLExpr>,
    },
    TNorm {
        kind: TNormKind,
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    TCoNorm {
        kind: TCoNormKind,
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    FuzzyNot {
        kind: FuzzyNegationKind,
        expr: Box<TLExpr>,
    },
    FuzzyImplication {
        kind: FuzzyImplicationKind,
        premise: Box<TLExpr>,
        conclusion: Box<TLExpr>,
    },
    SoftExists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        temperature: f64,
    },
    SoftForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        temperature: f64,
    },
    WeightedRule {
        weight: f64,
        rule: Box<TLExpr>,
    },
    ProbabilisticChoice {
        alternatives: Vec<(f64, TLExpr)>,
    },
    Release {
        released: Box<TLExpr>,
        releaser: Box<TLExpr>,
    },
    WeakUntil {
        before: Box<TLExpr>,
        after: Box<TLExpr>,
    },
    StrongRelease {
        released: Box<TLExpr>,
        releaser: Box<TLExpr>,
    },
    Lambda {
        var: String,
        var_type: Option<String>,
        body: Box<TLExpr>,
    },
    Apply {
        function: Box<TLExpr>,
        argument: Box<TLExpr>,
    },
    SetMembership {
        element: Box<TLExpr>,
        set: Box<TLExpr>,
    },
    SetUnion {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetIntersection {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetDifference {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetCardinality {
        set: Box<TLExpr>,
    },
    EmptySet,
    SetComprehension {
        var: String,
        domain: String,
        condition: Box<TLExpr>,
    },
    CountingExists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        min_count: usize,
    },
    CountingForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        min_count: usize,
    },
    ExactCount {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        count: usize,
    },
    Majority {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    LeastFixpoint {
        var: String,
        body: Box<TLExpr>,
    },
    GreatestFixpoint {
        var: String,
        body: Box<TLExpr>,
    },
    Nominal {
        name: String,
    },
    At {
        nominal: String,
        formula: Box<TLExpr>,
    },
    Somewhere {
        formula: Box<TLExpr>,
    },
    Everywhere {
        formula: Box<TLExpr>,
    },
    AllDifferent {
        variables: Vec<String>,
    },
    GlobalCardinality {
        variables: Vec<String>,
        values: Vec<TLExpr>,
        min_occurrences: Vec<usize>,
        max_occurrences: Vec<usize>,
    },
    Abducible {
        name: String,
        cost: f64,
    },
    Explain {
        formula: Box<TLExpr>,
    },
}

Variants

Pred

Fields

name: String

args: Vec<Term>

And(Box<TLExpr>, Box<TLExpr>)

Or(Box<TLExpr>, Box<TLExpr>)

Not(Box<TLExpr>)

Exists

Fields

var: String

domain: String

body: Box<TLExpr>

ForAll

Fields

var: String

domain: String

body: Box<TLExpr>

Imply(Box<TLExpr>, Box<TLExpr>)

Score(Box<TLExpr>)

Add(Box<TLExpr>, Box<TLExpr>)

Sub(Box<TLExpr>, Box<TLExpr>)

Mul(Box<TLExpr>, Box<TLExpr>)

Div(Box<TLExpr>, Box<TLExpr>)

Pow(Box<TLExpr>, Box<TLExpr>)

Mod(Box<TLExpr>, Box<TLExpr>)

Min(Box<TLExpr>, Box<TLExpr>)

Max(Box<TLExpr>, Box<TLExpr>)

Abs(Box<TLExpr>)

Floor(Box<TLExpr>)

Ceil(Box<TLExpr>)

Round(Box<TLExpr>)

Sqrt(Box<TLExpr>)

Exp(Box<TLExpr>)

Log(Box<TLExpr>)

Sin(Box<TLExpr>)

Cos(Box<TLExpr>)

Tan(Box<TLExpr>)

Eq(Box<TLExpr>, Box<TLExpr>)

Lt(Box<TLExpr>, Box<TLExpr>)

Gt(Box<TLExpr>, Box<TLExpr>)

Lte(Box<TLExpr>, Box<TLExpr>)

Gte(Box<TLExpr>, Box<TLExpr>)

IfThenElse

Fields

condition: Box<TLExpr>

then_branch: Box<TLExpr>

else_branch: Box<TLExpr>

Constant(f64)

Aggregate

Fields

op: AggregateOp

var: String

domain: String

body: Box<TLExpr>

group_by: Option<Vec<String>>

Optional group-by variables

Let

Fields

var: String

value: Box<TLExpr>

body: Box<TLExpr>

Box(Box<TLExpr>)

Necessity operator (□, “box”): something is necessarily true In all possible worlds or states, the expression holds

Diamond(Box<TLExpr>)

Possibility operator (◇, “diamond”): something is possibly true In at least one possible world or state, the expression holds Related to Box by: ◇P = ¬□¬P

Next(Box<TLExpr>)

Next operator (X): true in the next state

Eventually(Box<TLExpr>)

Eventually operator (F): true in some future state

Always(Box<TLExpr>)

Always/Globally operator (G): true in all future states

Until

Until operator (U): first expression holds until second becomes true

Fields

before: Box<TLExpr>

after: Box<TLExpr>

TNorm

T-norm (fuzzy AND) with specified semantics

Fields

kind: TNormKind

left: Box<TLExpr>

right: Box<TLExpr>

TCoNorm

T-conorm (fuzzy OR) with specified semantics

Fields

kind: TCoNormKind

left: Box<TLExpr>

right: Box<TLExpr>

FuzzyNot

Fuzzy negation with specified semantics

Fields

kind: FuzzyNegationKind

expr: Box<TLExpr>

FuzzyImplication

Fuzzy implication operator

Fields

kind: FuzzyImplicationKind

premise: Box<TLExpr>

conclusion: Box<TLExpr>

SoftExists

Soft existential quantifier with temperature parameter Temperature controls how “soft” the quantifier is:

• Low temperature (→0): approaches hard max (standard exists)
• High temperature: smoother aggregation (log-sum-exp)

Fields

var: String

domain: String

body: Box<TLExpr>

temperature: f64

Temperature parameter (default: 1.0)

SoftForAll

Soft universal quantifier with temperature parameter Temperature controls how “soft” the quantifier is:

• Low temperature (→0): approaches hard min (standard forall)
• High temperature: smoother aggregation

Fields

var: String

domain: String

body: Box<TLExpr>

temperature: f64

Temperature parameter (default: 1.0)

WeightedRule

Weighted rule with confidence/probability Used in probabilistic logic programming

Fields

weight: f64

rule: Box<TLExpr>

ProbabilisticChoice

Probabilistic choice between alternatives with given probabilities Probabilities should sum to 1.0

Fields

alternatives: Vec<(f64, TLExpr)>

Release

Release operator (R): dual of Until P R Q means Q holds until and including when P becomes true

Fields

released: Box<TLExpr>

releaser: Box<TLExpr>

WeakUntil

Weak Until (W): P W Q means P holds until Q, but Q may never hold

Fields

before: Box<TLExpr>

after: Box<TLExpr>

StrongRelease

Strong Release (M): dual of weak until

Fields

released: Box<TLExpr>

releaser: Box<TLExpr>

Lambda

Lambda abstraction: λvar. body Creates a function that binds var in body

Fields

var: String

var_type: Option<String>

Optional type annotation for the parameter

body: Box<TLExpr>

Apply

Function application: Apply(f, arg) represents f(arg)

Fields

function: Box<TLExpr>

argument: Box<TLExpr>

SetMembership

Set membership: elem ∈ set

Fields

element: Box<TLExpr>

set: Box<TLExpr>

SetUnion

Set union: A ∪ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetIntersection

Set intersection: A ∩ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetDifference

Set difference: A \ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetCardinality

Set cardinality: |S|

Fields

set: Box<TLExpr>

EmptySet

Empty set: ∅

SetComprehension

Set comprehension: { var : domain | condition }

Fields

var: String

domain: String

condition: Box<TLExpr>

CountingExists

Counting existential quantifier: ∃≥k x. P(x) “There exist at least k elements satisfying P”

Fields

var: String

domain: String

body: Box<TLExpr>

min_count: usize

Minimum count threshold

CountingForAll

Counting universal quantifier: ∀≥k x. P(x) “At least k elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

min_count: usize

Minimum count threshold

ExactCount

Exact count quantifier: ∃=k x. P(x) “Exactly k elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

count: usize

Exact count required

Majority

Majority quantifier: Majority x. P(x) “More than half of the elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

LeastFixpoint

Least fixed point (mu): μX. F(X) Used for inductive definitions

Fields

var: String

Variable representing the fixed point

body: Box<TLExpr>

Function body that references var

GreatestFixpoint

Greatest fixed point (nu): νX. F(X) Used for coinductive definitions

Fields

var: String

Variable representing the fixed point

body: Box<TLExpr>

Function body that references var

Nominal

Nominal (named state/world): @i Represents a specific named state in a model

Fields

name: String

At

Satisfaction operator: @i φ “Formula φ is true at the nominal state i”

Fields

nominal: String

formula: Box<TLExpr>

Somewhere

Universal modality: E φ “φ is true in some state reachable from here”

Fields

formula: Box<TLExpr>

Everywhere

Universal modality (dual): A φ “φ is true in all reachable states”

Fields

formula: Box<TLExpr>

AllDifferent

All-different constraint: all variables must have different values

Fields

variables: Vec<String>

GlobalCardinality

Global cardinality constraint Each value in values must occur at least min and at most max times in variables

Fields

variables: Vec<String>

values: Vec<TLExpr>

min_occurrences: Vec<usize>

max_occurrences: Vec<usize>

Abducible

Abducible literal: can be assumed true for explanation

Fields

name: String

cost: f64

Explain

Explanation marker: indicates this part needs explanation

Fields

formula: Box<TLExpr>