tensorlogic_ir/expr/
mod.rs

1//! TensorLogic expressions (TLExpr).
2
3pub mod ac_matching;
4pub mod advanced_analysis;
5pub mod advanced_rewriting;
6mod analysis;
7pub mod confluence;
8pub mod defuzzification;
9pub mod distributive_laws;
10mod domain_validation;
11pub mod ltl_ctl_utilities;
12pub mod modal_axioms;
13pub mod modal_equivalences;
14pub mod normal_forms;
15pub mod optimization;
16pub mod optimization_pipeline;
17pub mod probabilistic_reasoning;
18pub mod rewriting;
19pub mod strategy_selector;
20pub mod temporal_equivalences;
21mod validation;
22
23use serde::{Deserialize, Serialize};
24
25use crate::term::Term;
26
27/// Aggregation operation type.
28#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
29pub enum AggregateOp {
30    /// Count the number of elements
31    Count,
32    /// Sum of all elements
33    Sum,
34    /// Average (mean) of elements
35    Average,
36    /// Maximum element
37    Max,
38    /// Minimum element
39    Min,
40    /// Product of all elements
41    Product,
42    /// Any (existential - true if any element is true)
43    Any,
44    /// All (universal - true if all elements are true)
45    All,
46}
47
48/// T-norm (triangular norm) kinds for fuzzy AND operations.
49/// A t-norm is a binary operation T: [0,1] × [0,1] → [0,1] that is:
50/// - Commutative: T(a,b) = T(b,a)
51/// - Associative: T(a,T(b,c)) = T(T(a,b),c)
52/// - Monotonic: If a ≤ b then T(a,c) ≤ T(b,c)
53/// - Has 1 as identity: T(a,1) = a
54#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
55pub enum TNormKind {
56    /// Minimum t-norm (Gödel): T(a,b) = min(a,b)
57    /// Standard fuzzy AND, also known as Zadeh t-norm
58    Minimum,
59
60    /// Product t-norm: T(a,b) = a * b
61    /// Probabilistic interpretation of independence
62    Product,
63
64    /// Łukasiewicz t-norm: T(a,b) = max(0, a + b - 1)
65    /// Strong conjunction in Łukasiewicz logic
66    Lukasiewicz,
67
68    /// Drastic t-norm: T(a,b) = { b if a=1, a if b=1, 0 otherwise }
69    /// Most restrictive t-norm
70    Drastic,
71
72    /// Nilpotent minimum: T(a,b) = { min(a,b) if a+b>1, 0 otherwise }
73    NilpotentMinimum,
74
75    /// Hamacher product: T(a,b) = ab/(a+b-ab) for a,b > 0
76    /// Generalizes product t-norm
77    Hamacher,
78}
79
80/// T-conorm (triangular conorm) kinds for fuzzy OR operations.
81/// A t-conorm is the dual of a t-norm: S(a,b) = 1 - T(1-a, 1-b)
82#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
83pub enum TCoNormKind {
84    /// Maximum t-conorm (Gödel): S(a,b) = max(a,b)
85    /// Standard fuzzy OR, dual of minimum t-norm
86    Maximum,
87
88    /// Probabilistic sum: S(a,b) = a + b - a*b
89    /// Dual of product t-norm
90    ProbabilisticSum,
91
92    /// Łukasiewicz t-conorm: S(a,b) = min(1, a + b)
93    /// Bounded sum, dual of Łukasiewicz t-norm
94    BoundedSum,
95
96    /// Drastic t-conorm: S(a,b) = { b if a=0, a if b=0, 1 otherwise }
97    /// Most permissive t-conorm, dual of drastic t-norm
98    Drastic,
99
100    /// Nilpotent maximum: S(a,b) = { max(a,b) if a+b<1, 1 otherwise }
101    /// Dual of nilpotent minimum
102    NilpotentMaximum,
103
104    /// Hamacher sum: dual of Hamacher product
105    Hamacher,
106}
107
108/// Fuzzy negation kinds.
109#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
110pub enum FuzzyNegationKind {
111    /// Standard fuzzy negation: N(a) = 1 - a
112    Standard,
113
114    /// Sugeno negation: N(a) = (1-a)/(1+λa) for λ > -1
115    /// Parameterized family of negations
116    Sugeno {
117        /// Lambda parameter, must be > -1
118        lambda: i32, // Using i32 to maintain Eq trait; actual value is lambda/100
119    },
120
121    /// Yager negation: N(a) = (1 - a^w)^(1/w) for w > 0
122    Yager {
123        /// w parameter stored as integer (actual = w/10)
124        w: u32,
125    },
126}
127
128/// Fuzzy implication operator kinds.
129#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
130pub enum FuzzyImplicationKind {
131    /// Gödel implication: I(a,b) = { 1 if a≤b, b otherwise }
132    Godel,
133
134    /// Łukasiewicz implication: I(a,b) = min(1, 1-a+b)
135    Lukasiewicz,
136
137    /// Reichenbach implication: I(a,b) = 1 - a + ab
138    Reichenbach,
139
140    /// Kleene-Dienes implication: I(a,b) = max(1-a, b)
141    KleeneDienes,
142
143    /// Rescher implication: I(a,b) = { 1 if a≤b, 0 otherwise }
144    Rescher,
145
146    /// Goguen implication: I(a,b) = { 1 if a≤b, b/a otherwise }
147    Goguen,
148}
149
150#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
151pub enum TLExpr {
152    Pred {
153        name: String,
154        args: Vec<Term>,
155    },
156    And(Box<TLExpr>, Box<TLExpr>),
157    Or(Box<TLExpr>, Box<TLExpr>),
158    Not(Box<TLExpr>),
159    Exists {
160        var: String,
161        domain: String,
162        body: Box<TLExpr>,
163    },
164    ForAll {
165        var: String,
166        domain: String,
167        body: Box<TLExpr>,
168    },
169    Imply(Box<TLExpr>, Box<TLExpr>),
170    Score(Box<TLExpr>),
171
172    // Arithmetic operations
173    Add(Box<TLExpr>, Box<TLExpr>),
174    Sub(Box<TLExpr>, Box<TLExpr>),
175    Mul(Box<TLExpr>, Box<TLExpr>),
176    Div(Box<TLExpr>, Box<TLExpr>),
177    Pow(Box<TLExpr>, Box<TLExpr>),
178    Mod(Box<TLExpr>, Box<TLExpr>),
179    Min(Box<TLExpr>, Box<TLExpr>),
180    Max(Box<TLExpr>, Box<TLExpr>),
181
182    // Unary mathematical operations
183    Abs(Box<TLExpr>),
184    Floor(Box<TLExpr>),
185    Ceil(Box<TLExpr>),
186    Round(Box<TLExpr>),
187    Sqrt(Box<TLExpr>),
188    Exp(Box<TLExpr>),
189    Log(Box<TLExpr>),
190    Sin(Box<TLExpr>),
191    Cos(Box<TLExpr>),
192    Tan(Box<TLExpr>),
193
194    // Comparison operations
195    Eq(Box<TLExpr>, Box<TLExpr>),
196    Lt(Box<TLExpr>, Box<TLExpr>),
197    Gt(Box<TLExpr>, Box<TLExpr>),
198    Lte(Box<TLExpr>, Box<TLExpr>),
199    Gte(Box<TLExpr>, Box<TLExpr>),
200
201    // Conditional expression
202    IfThenElse {
203        condition: Box<TLExpr>,
204        then_branch: Box<TLExpr>,
205        else_branch: Box<TLExpr>,
206    },
207
208    // Numeric literal
209    Constant(f64),
210
211    // Aggregation operations (re-enabled with explicit output tracking support)
212    Aggregate {
213        op: AggregateOp,
214        var: String,
215        domain: String,
216        body: Box<TLExpr>,
217        /// Optional group-by variables
218        group_by: Option<Vec<String>>,
219    },
220
221    // Let binding for local variable definitions
222    Let {
223        var: String,
224        value: Box<TLExpr>,
225        body: Box<TLExpr>,
226    },
227
228    // Modal logic operators
229    /// Necessity operator (□, "box"): something is necessarily true
230    /// In all possible worlds or states, the expression holds
231    Box(Box<TLExpr>),
232
233    /// Possibility operator (◇, "diamond"): something is possibly true
234    /// In at least one possible world or state, the expression holds
235    /// Related to Box by: ◇P = ¬□¬P
236    Diamond(Box<TLExpr>),
237
238    // Temporal logic operators
239    /// Next operator (X): true in the next state
240    Next(Box<TLExpr>),
241
242    /// Eventually operator (F): true in some future state
243    Eventually(Box<TLExpr>),
244
245    /// Always/Globally operator (G): true in all future states
246    Always(Box<TLExpr>),
247
248    /// Until operator (U): first expression holds until second becomes true
249    Until {
250        before: Box<TLExpr>,
251        after: Box<TLExpr>,
252    },
253
254    // Fuzzy logic operators
255    /// T-norm (fuzzy AND) with specified semantics
256    TNorm {
257        kind: TNormKind,
258        left: Box<TLExpr>,
259        right: Box<TLExpr>,
260    },
261
262    /// T-conorm (fuzzy OR) with specified semantics
263    TCoNorm {
264        kind: TCoNormKind,
265        left: Box<TLExpr>,
266        right: Box<TLExpr>,
267    },
268
269    /// Fuzzy negation with specified semantics
270    FuzzyNot {
271        kind: FuzzyNegationKind,
272        expr: Box<TLExpr>,
273    },
274
275    /// Fuzzy implication operator
276    FuzzyImplication {
277        kind: FuzzyImplicationKind,
278        premise: Box<TLExpr>,
279        conclusion: Box<TLExpr>,
280    },
281
282    // Probabilistic operators
283    /// Soft existential quantifier with temperature parameter
284    /// Temperature controls how "soft" the quantifier is:
285    /// - Low temperature (→0): approaches hard max (standard exists)
286    /// - High temperature: smoother aggregation (log-sum-exp)
287    SoftExists {
288        var: String,
289        domain: String,
290        body: Box<TLExpr>,
291        /// Temperature parameter (default: 1.0)
292        temperature: f64,
293    },
294
295    /// Soft universal quantifier with temperature parameter
296    /// Temperature controls how "soft" the quantifier is:
297    /// - Low temperature (→0): approaches hard min (standard forall)
298    /// - High temperature: smoother aggregation
299    SoftForAll {
300        var: String,
301        domain: String,
302        body: Box<TLExpr>,
303        /// Temperature parameter (default: 1.0)
304        temperature: f64,
305    },
306
307    /// Weighted rule with confidence/probability
308    /// Used in probabilistic logic programming
309    WeightedRule {
310        weight: f64,
311        rule: Box<TLExpr>,
312    },
313
314    /// Probabilistic choice between alternatives with given probabilities
315    /// Probabilities should sum to 1.0
316    ProbabilisticChoice {
317        alternatives: Vec<(f64, TLExpr)>, // (probability, expression) pairs
318    },
319
320    // Extended temporal logic (LTL properties)
321    /// Release operator (R): dual of Until
322    /// P R Q means Q holds until and including when P becomes true
323    Release {
324        released: Box<TLExpr>,
325        releaser: Box<TLExpr>,
326    },
327
328    /// Weak Until (W): P W Q means P holds until Q, but Q may never hold
329    WeakUntil {
330        before: Box<TLExpr>,
331        after: Box<TLExpr>,
332    },
333
334    /// Strong Release (M): dual of weak until
335    StrongRelease {
336        released: Box<TLExpr>,
337        releaser: Box<TLExpr>,
338    },
339}
340
341impl TLExpr {
342    pub fn pred(name: impl Into<String>, args: Vec<Term>) -> Self {
343        TLExpr::Pred {
344            name: name.into(),
345            args,
346        }
347    }
348
349    pub fn and(left: TLExpr, right: TLExpr) -> Self {
350        TLExpr::And(Box::new(left), Box::new(right))
351    }
352
353    pub fn or(left: TLExpr, right: TLExpr) -> Self {
354        TLExpr::Or(Box::new(left), Box::new(right))
355    }
356
357    pub fn negate(expr: TLExpr) -> Self {
358        TLExpr::Not(Box::new(expr))
359    }
360
361    pub fn exists(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
362        TLExpr::Exists {
363            var: var.into(),
364            domain: domain.into(),
365            body: Box::new(body),
366        }
367    }
368
369    pub fn forall(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
370        TLExpr::ForAll {
371            var: var.into(),
372            domain: domain.into(),
373            body: Box::new(body),
374        }
375    }
376
377    pub fn imply(premise: TLExpr, conclusion: TLExpr) -> Self {
378        TLExpr::Imply(Box::new(premise), Box::new(conclusion))
379    }
380
381    pub fn score(expr: TLExpr) -> Self {
382        TLExpr::Score(Box::new(expr))
383    }
384
385    // Arithmetic operations
386    #[allow(clippy::should_implement_trait)]
387    pub fn add(left: TLExpr, right: TLExpr) -> Self {
388        TLExpr::Add(Box::new(left), Box::new(right))
389    }
390
391    #[allow(clippy::should_implement_trait)]
392    pub fn sub(left: TLExpr, right: TLExpr) -> Self {
393        TLExpr::Sub(Box::new(left), Box::new(right))
394    }
395
396    #[allow(clippy::should_implement_trait)]
397    pub fn mul(left: TLExpr, right: TLExpr) -> Self {
398        TLExpr::Mul(Box::new(left), Box::new(right))
399    }
400
401    #[allow(clippy::should_implement_trait)]
402    pub fn div(left: TLExpr, right: TLExpr) -> Self {
403        TLExpr::Div(Box::new(left), Box::new(right))
404    }
405
406    pub fn pow(left: TLExpr, right: TLExpr) -> Self {
407        TLExpr::Pow(Box::new(left), Box::new(right))
408    }
409
410    pub fn modulo(left: TLExpr, right: TLExpr) -> Self {
411        TLExpr::Mod(Box::new(left), Box::new(right))
412    }
413
414    pub fn min(left: TLExpr, right: TLExpr) -> Self {
415        TLExpr::Min(Box::new(left), Box::new(right))
416    }
417
418    pub fn max(left: TLExpr, right: TLExpr) -> Self {
419        TLExpr::Max(Box::new(left), Box::new(right))
420    }
421
422    // Unary mathematical operations
423    pub fn abs(expr: TLExpr) -> Self {
424        TLExpr::Abs(Box::new(expr))
425    }
426
427    pub fn floor(expr: TLExpr) -> Self {
428        TLExpr::Floor(Box::new(expr))
429    }
430
431    pub fn ceil(expr: TLExpr) -> Self {
432        TLExpr::Ceil(Box::new(expr))
433    }
434
435    pub fn round(expr: TLExpr) -> Self {
436        TLExpr::Round(Box::new(expr))
437    }
438
439    pub fn sqrt(expr: TLExpr) -> Self {
440        TLExpr::Sqrt(Box::new(expr))
441    }
442
443    pub fn exp(expr: TLExpr) -> Self {
444        TLExpr::Exp(Box::new(expr))
445    }
446
447    pub fn log(expr: TLExpr) -> Self {
448        TLExpr::Log(Box::new(expr))
449    }
450
451    pub fn sin(expr: TLExpr) -> Self {
452        TLExpr::Sin(Box::new(expr))
453    }
454
455    pub fn cos(expr: TLExpr) -> Self {
456        TLExpr::Cos(Box::new(expr))
457    }
458
459    pub fn tan(expr: TLExpr) -> Self {
460        TLExpr::Tan(Box::new(expr))
461    }
462
463    // Comparison operations
464    pub fn eq(left: TLExpr, right: TLExpr) -> Self {
465        TLExpr::Eq(Box::new(left), Box::new(right))
466    }
467
468    pub fn lt(left: TLExpr, right: TLExpr) -> Self {
469        TLExpr::Lt(Box::new(left), Box::new(right))
470    }
471
472    pub fn gt(left: TLExpr, right: TLExpr) -> Self {
473        TLExpr::Gt(Box::new(left), Box::new(right))
474    }
475
476    pub fn lte(left: TLExpr, right: TLExpr) -> Self {
477        TLExpr::Lte(Box::new(left), Box::new(right))
478    }
479
480    pub fn gte(left: TLExpr, right: TLExpr) -> Self {
481        TLExpr::Gte(Box::new(left), Box::new(right))
482    }
483
484    // Conditional
485    pub fn if_then_else(condition: TLExpr, then_branch: TLExpr, else_branch: TLExpr) -> Self {
486        TLExpr::IfThenElse {
487            condition: Box::new(condition),
488            then_branch: Box::new(then_branch),
489            else_branch: Box::new(else_branch),
490        }
491    }
492
493    // Constant
494    pub fn constant(value: f64) -> Self {
495        TLExpr::Constant(value)
496    }
497
498    // Aggregation operations
499    pub fn aggregate(
500        op: AggregateOp,
501        var: impl Into<String>,
502        domain: impl Into<String>,
503        body: TLExpr,
504    ) -> Self {
505        TLExpr::Aggregate {
506            op,
507            var: var.into(),
508            domain: domain.into(),
509            body: Box::new(body),
510            group_by: None,
511        }
512    }
513
514    pub fn aggregate_with_group_by(
515        op: AggregateOp,
516        var: impl Into<String>,
517        domain: impl Into<String>,
518        body: TLExpr,
519        group_by: Vec<String>,
520    ) -> Self {
521        TLExpr::Aggregate {
522            op,
523            var: var.into(),
524            domain: domain.into(),
525            body: Box::new(body),
526            group_by: Some(group_by),
527        }
528    }
529
530    pub fn count(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
531        Self::aggregate(AggregateOp::Count, var, domain, body)
532    }
533
534    pub fn sum(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
535        Self::aggregate(AggregateOp::Sum, var, domain, body)
536    }
537
538    pub fn average(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
539        Self::aggregate(AggregateOp::Average, var, domain, body)
540    }
541
542    pub fn max_agg(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
543        Self::aggregate(AggregateOp::Max, var, domain, body)
544    }
545
546    pub fn min_agg(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
547        Self::aggregate(AggregateOp::Min, var, domain, body)
548    }
549
550    pub fn product(var: impl Into<String>, domain: impl Into<String>, body: TLExpr) -> Self {
551        Self::aggregate(AggregateOp::Product, var, domain, body)
552    }
553
554    // Let binding
555    pub fn let_binding(var: impl Into<String>, value: TLExpr, body: TLExpr) -> Self {
556        TLExpr::Let {
557            var: var.into(),
558            value: Box::new(value),
559            body: Box::new(body),
560        }
561    }
562
563    // Modal logic operators
564    /// Create a Box (necessity) operator.
565    ///
566    /// □P: "P is necessarily true" - holds in all possible worlds/states
567    pub fn modal_box(expr: TLExpr) -> Self {
568        TLExpr::Box(Box::new(expr))
569    }
570
571    /// Create a Diamond (possibility) operator.
572    ///
573    /// ◇P: "P is possibly true" - holds in at least one possible world/state
574    pub fn modal_diamond(expr: TLExpr) -> Self {
575        TLExpr::Diamond(Box::new(expr))
576    }
577
578    // Temporal logic operators
579    /// Create a Next operator.
580    ///
581    /// XP: "P is true in the next state"
582    pub fn next(expr: TLExpr) -> Self {
583        TLExpr::Next(Box::new(expr))
584    }
585
586    /// Create an Eventually operator.
587    ///
588    /// FP: "P will eventually be true" - true in some future state
589    pub fn eventually(expr: TLExpr) -> Self {
590        TLExpr::Eventually(Box::new(expr))
591    }
592
593    /// Create an Always operator.
594    ///
595    /// GP: "P is always true" - true in all future states
596    pub fn always(expr: TLExpr) -> Self {
597        TLExpr::Always(Box::new(expr))
598    }
599
600    /// Create an Until operator.
601    ///
602    /// P U Q: "P holds until Q becomes true"
603    pub fn until(before: TLExpr, after: TLExpr) -> Self {
604        TLExpr::Until {
605            before: Box::new(before),
606            after: Box::new(after),
607        }
608    }
609
610    // Fuzzy logic builders
611
612    /// Create a T-norm (fuzzy AND) operation with specified semantics.
613    pub fn tnorm(kind: TNormKind, left: TLExpr, right: TLExpr) -> Self {
614        TLExpr::TNorm {
615            kind,
616            left: Box::new(left),
617            right: Box::new(right),
618        }
619    }
620
621    /// Create a minimum T-norm (standard fuzzy AND).
622    pub fn fuzzy_and(left: TLExpr, right: TLExpr) -> Self {
623        Self::tnorm(TNormKind::Minimum, left, right)
624    }
625
626    /// Create a product T-norm (probabilistic AND).
627    pub fn probabilistic_and(left: TLExpr, right: TLExpr) -> Self {
628        Self::tnorm(TNormKind::Product, left, right)
629    }
630
631    /// Create a T-conorm (fuzzy OR) operation with specified semantics.
632    pub fn tconorm(kind: TCoNormKind, left: TLExpr, right: TLExpr) -> Self {
633        TLExpr::TCoNorm {
634            kind,
635            left: Box::new(left),
636            right: Box::new(right),
637        }
638    }
639
640    /// Create a maximum T-conorm (standard fuzzy OR).
641    pub fn fuzzy_or(left: TLExpr, right: TLExpr) -> Self {
642        Self::tconorm(TCoNormKind::Maximum, left, right)
643    }
644
645    /// Create a probabilistic sum T-conorm.
646    pub fn probabilistic_or(left: TLExpr, right: TLExpr) -> Self {
647        Self::tconorm(TCoNormKind::ProbabilisticSum, left, right)
648    }
649
650    /// Create a fuzzy negation with specified semantics.
651    pub fn fuzzy_not(kind: FuzzyNegationKind, expr: TLExpr) -> Self {
652        TLExpr::FuzzyNot {
653            kind,
654            expr: Box::new(expr),
655        }
656    }
657
658    /// Create a standard fuzzy negation (1 - x).
659    pub fn standard_fuzzy_not(expr: TLExpr) -> Self {
660        Self::fuzzy_not(FuzzyNegationKind::Standard, expr)
661    }
662
663    /// Create a fuzzy implication with specified semantics.
664    pub fn fuzzy_imply(kind: FuzzyImplicationKind, premise: TLExpr, conclusion: TLExpr) -> Self {
665        TLExpr::FuzzyImplication {
666            kind,
667            premise: Box::new(premise),
668            conclusion: Box::new(conclusion),
669        }
670    }
671
672    // Probabilistic operators builders
673
674    /// Create a soft existential quantifier with temperature parameter.
675    ///
676    /// # Arguments
677    /// * `var` - Variable name
678    /// * `domain` - Domain name
679    /// * `body` - Expression body
680    /// * `temperature` - Temperature parameter (default 1.0). Lower = harder max.
681    pub fn soft_exists(
682        var: impl Into<String>,
683        domain: impl Into<String>,
684        body: TLExpr,
685        temperature: f64,
686    ) -> Self {
687        TLExpr::SoftExists {
688            var: var.into(),
689            domain: domain.into(),
690            body: Box::new(body),
691            temperature,
692        }
693    }
694
695    /// Create a soft universal quantifier with temperature parameter.
696    ///
697    /// # Arguments
698    /// * `var` - Variable name
699    /// * `domain` - Domain name
700    /// * `body` - Expression body
701    /// * `temperature` - Temperature parameter (default 1.0). Lower = harder min.
702    pub fn soft_forall(
703        var: impl Into<String>,
704        domain: impl Into<String>,
705        body: TLExpr,
706        temperature: f64,
707    ) -> Self {
708        TLExpr::SoftForAll {
709            var: var.into(),
710            domain: domain.into(),
711            body: Box::new(body),
712            temperature,
713        }
714    }
715
716    /// Create a weighted rule with confidence/probability.
717    ///
718    /// # Arguments
719    /// * `weight` - Weight/confidence (typically in [0,1] for probabilities)
720    /// * `rule` - The rule expression
721    pub fn weighted_rule(weight: f64, rule: TLExpr) -> Self {
722        TLExpr::WeightedRule {
723            weight,
724            rule: Box::new(rule),
725        }
726    }
727
728    /// Create a probabilistic choice between alternatives.
729    ///
730    /// # Arguments
731    /// * `alternatives` - Vector of (probability, expression) pairs. Should sum to 1.0.
732    pub fn probabilistic_choice(alternatives: Vec<(f64, TLExpr)>) -> Self {
733        TLExpr::ProbabilisticChoice { alternatives }
734    }
735
736    // Extended temporal logic builders
737
738    /// Create a Release operator (R).
739    ///
740    /// P R Q: "Q holds until and including when P becomes true"
741    pub fn release(released: TLExpr, releaser: TLExpr) -> Self {
742        TLExpr::Release {
743            released: Box::new(released),
744            releaser: Box::new(releaser),
745        }
746    }
747
748    /// Create a Weak Until operator (W).
749    ///
750    /// P W Q: "P holds until Q, but Q may never hold"
751    pub fn weak_until(before: TLExpr, after: TLExpr) -> Self {
752        TLExpr::WeakUntil {
753            before: Box::new(before),
754            after: Box::new(after),
755        }
756    }
757
758    /// Create a Strong Release operator (M).
759    ///
760    /// P M Q: Dual of weak until
761    pub fn strong_release(released: TLExpr, releaser: TLExpr) -> Self {
762        TLExpr::StrongRelease {
763            released: Box::new(released),
764            releaser: Box::new(releaser),
765        }
766    }
767}
tensorlogic_ir/expr/mod.rs

tensorlogic_ir/expr/
mod.rs
