Enum TLExpr 

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>,
    },
}

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>

Implementations

impl TLExpr

pub fn free_vars(&self) -> HashSet<String>

Collect all free variables in this expression

pub fn all_predicates(&self) -> HashMap<String, usize>

Collect all predicates and their arities

impl TLExpr

pub fn validate_domains(&self, registry: &DomainRegistry) -> Result<(), IrError>

Validate all domain references in this expression.

Checks that:

• All quantifier domains exist in the registry
• Variables used consistently across different quantifiers

pub fn referenced_domains(&self) -> Vec<String>

Extract all domains referenced in this expression.

impl TLExpr

pub fn validate_arity(&self) -> Result<(), String>

Validate that all predicates with the same name have consistent arity

impl TLExpr

pub fn pred(name: impl Into<String>, args: Vec<Term>) -> Self

pub fn and(left: TLExpr, right: TLExpr) -> Self

pub fn or(left: TLExpr, right: TLExpr) -> Self

pub fn negate(expr: TLExpr) -> Self

pub fn exists( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn forall( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn imply(premise: TLExpr, conclusion: TLExpr) -> Self

pub fn score(expr: TLExpr) -> Self

pub fn add(left: TLExpr, right: TLExpr) -> Self

pub fn sub(left: TLExpr, right: TLExpr) -> Self

pub fn mul(left: TLExpr, right: TLExpr) -> Self

pub fn div(left: TLExpr, right: TLExpr) -> Self

pub fn pow(left: TLExpr, right: TLExpr) -> Self

pub fn modulo(left: TLExpr, right: TLExpr) -> Self

pub fn min(left: TLExpr, right: TLExpr) -> Self

pub fn max(left: TLExpr, right: TLExpr) -> Self

pub fn abs(expr: TLExpr) -> Self

pub fn floor(expr: TLExpr) -> Self

pub fn ceil(expr: TLExpr) -> Self

pub fn round(expr: TLExpr) -> Self

pub fn sqrt(expr: TLExpr) -> Self

pub fn exp(expr: TLExpr) -> Self

pub fn log(expr: TLExpr) -> Self

pub fn sin(expr: TLExpr) -> Self

pub fn cos(expr: TLExpr) -> Self

pub fn tan(expr: TLExpr) -> Self

pub fn eq(left: TLExpr, right: TLExpr) -> Self

pub fn lt(left: TLExpr, right: TLExpr) -> Self

pub fn gt(left: TLExpr, right: TLExpr) -> Self

pub fn lte(left: TLExpr, right: TLExpr) -> Self

pub fn gte(left: TLExpr, right: TLExpr) -> Self

pub fn if_then_else( condition: TLExpr, then_branch: TLExpr, else_branch: TLExpr, ) -> Self

pub fn constant(value: f64) -> Self

pub fn aggregate( op: AggregateOp, var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn aggregate_with_group_by( op: AggregateOp, var: impl Into<String>, domain: impl Into<String>, body: TLExpr, group_by: Vec<String>, ) -> Self

pub fn count( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn sum( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn average( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn max_agg( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn min_agg( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn product( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn let_binding(var: impl Into<String>, value: TLExpr, body: TLExpr) -> Self

pub fn modal_box(expr: TLExpr) -> Self

Create a Box (necessity) operator.

□P: “P is necessarily true” - holds in all possible worlds/states

pub fn modal_diamond(expr: TLExpr) -> Self

Create a Diamond (possibility) operator.

◇P: “P is possibly true” - holds in at least one possible world/state

pub fn next(expr: TLExpr) -> Self

Create a Next operator.

XP: “P is true in the next state”

pub fn eventually(expr: TLExpr) -> Self

Create an Eventually operator.

FP: “P will eventually be true” - true in some future state

pub fn always(expr: TLExpr) -> Self

Create an Always operator.

GP: “P is always true” - true in all future states

pub fn until(before: TLExpr, after: TLExpr) -> Self

Create an Until operator.

P U Q: “P holds until Q becomes true”

pub fn tnorm(kind: TNormKind, left: TLExpr, right: TLExpr) -> Self

Create a T-norm (fuzzy AND) operation with specified semantics.

pub fn fuzzy_and(left: TLExpr, right: TLExpr) -> Self

Create a minimum T-norm (standard fuzzy AND).

pub fn probabilistic_and(left: TLExpr, right: TLExpr) -> Self

Create a product T-norm (probabilistic AND).

pub fn tconorm(kind: TCoNormKind, left: TLExpr, right: TLExpr) -> Self

Create a T-conorm (fuzzy OR) operation with specified semantics.

pub fn fuzzy_or(left: TLExpr, right: TLExpr) -> Self

Create a maximum T-conorm (standard fuzzy OR).

pub fn probabilistic_or(left: TLExpr, right: TLExpr) -> Self

Create a probabilistic sum T-conorm.

pub fn fuzzy_not(kind: FuzzyNegationKind, expr: TLExpr) -> Self

Create a fuzzy negation with specified semantics.

pub fn standard_fuzzy_not(expr: TLExpr) -> Self

Create a standard fuzzy negation (1 - x).

pub fn fuzzy_imply( kind: FuzzyImplicationKind, premise: TLExpr, conclusion: TLExpr, ) -> Self

Create a fuzzy implication with specified semantics.

pub fn soft_exists( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, temperature: f64, ) -> Self

Create a soft existential quantifier with temperature parameter.

Arguments

• var - Variable name
• domain - Domain name
• body - Expression body
• temperature - Temperature parameter (default 1.0). Lower = harder max.

pub fn soft_forall( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, temperature: f64, ) -> Self

Create a soft universal quantifier with temperature parameter.

Arguments

• var - Variable name
• domain - Domain name
• body - Expression body
• temperature - Temperature parameter (default 1.0). Lower = harder min.

pub fn weighted_rule(weight: f64, rule: TLExpr) -> Self

Create a weighted rule with confidence/probability.

Arguments

• weight - Weight/confidence (typically in [0,1] for probabilities)
• rule - The rule expression

pub fn probabilistic_choice(alternatives: Vec<(f64, TLExpr)>) -> Self

Create a probabilistic choice between alternatives.

Arguments

• alternatives - Vector of (probability, expression) pairs. Should sum to 1.0.

pub fn release(released: TLExpr, releaser: TLExpr) -> Self

Create a Release operator (R).

P R Q: “Q holds until and including when P becomes true”

pub fn weak_until(before: TLExpr, after: TLExpr) -> Self

Create a Weak Until operator (W).

P W Q: “P holds until Q, but Q may never hold”

pub fn strong_release(released: TLExpr, releaser: TLExpr) -> Self

Create a Strong Release operator (M).

P M Q: Dual of weak until

Trait Implementations

impl Clone for TLExpr

fn clone(&self) -> TLExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TLExpr

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for TLExpr

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for TLExpr

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

Formats the value using the given formatter.

impl PartialEq for TLExpr

fn eq(&self, other: &TLExpr) -> 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 Serialize for TLExpr

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for TLExpr