tensorlogic_compiler/optimize/
negation.rs

1//! Negation optimization pass.
2//!
3//! This module optimizes negation operations in logical expressions:
4//! - Eliminate double negations: NOT(NOT(x)) → x
5//! - Apply De Morgan's laws: NOT(AND(x, y)) → OR(NOT(x), NOT(y))
6//! - Push negations through quantifiers: NOT(EXISTS x. P(x)) → FORALL x. NOT(P(x))
7
8use tensorlogic_ir::TLExpr;
9
10/// Statistics from negation optimization
11#[derive(Debug, Clone, Default)]
12pub struct NegationOptStats {
13    /// Double negations eliminated
14    pub double_negations_eliminated: usize,
15    /// De Morgan's laws applied
16    pub demorgans_applied: usize,
17    /// Quantifier negations pushed
18    pub quantifier_negations_pushed: usize,
19}
20
21impl std::fmt::Display for NegationOptStats {
22    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
23        write!(
24            f,
25            "NegationOptStats {{ double_negations: {}, demorgans: {}, quantifier_pushes: {} }}",
26            self.double_negations_eliminated,
27            self.demorgans_applied,
28            self.quantifier_negations_pushed
29        )
30    }
31}
32
33/// Optimize negations in an expression
34pub fn optimize_negations(expr: &TLExpr) -> (TLExpr, NegationOptStats) {
35    let mut stats = NegationOptStats::default();
36    let optimized = optimize_negations_impl(expr, &mut stats);
37    (optimized, stats)
38}
39
40fn optimize_negations_impl(expr: &TLExpr, stats: &mut NegationOptStats) -> TLExpr {
41    match expr {
42        #[allow(unreachable_patterns)] // Double negation elimination: NOT(NOT(x)) → x
43        TLExpr::Not(inner) => {
44            if let TLExpr::Not(inner_inner) = inner.as_ref() {
45                stats.double_negations_eliminated += 1;
46                optimize_negations_impl(inner_inner, stats)
47            } else {
48                // Apply De Morgan's laws
49                match inner.as_ref() {
50                    // NOT(AND(x, y)) → OR(NOT(x), NOT(y))
51                    TLExpr::And(a, b) => {
52                        stats.demorgans_applied += 1;
53                        let not_a =
54                            optimize_negations_impl(&TLExpr::negate(a.as_ref().clone()), stats);
55                        let not_b =
56                            optimize_negations_impl(&TLExpr::negate(b.as_ref().clone()), stats);
57                        TLExpr::or(not_a, not_b)
58                    }
59                    // NOT(OR(x, y)) → AND(NOT(x), NOT(y))
60                    TLExpr::Or(a, b) => {
61                        stats.demorgans_applied += 1;
62                        let not_a =
63                            optimize_negations_impl(&TLExpr::negate(a.as_ref().clone()), stats);
64                        let not_b =
65                            optimize_negations_impl(&TLExpr::negate(b.as_ref().clone()), stats);
66                        TLExpr::and(not_a, not_b)
67                    }
68                    // NOT(EXISTS x. P(x)) → FORALL x. NOT(P(x))
69                    TLExpr::Exists { var, domain, body } => {
70                        stats.quantifier_negations_pushed += 1;
71                        let not_body =
72                            optimize_negations_impl(&TLExpr::negate(body.as_ref().clone()), stats);
73                        TLExpr::forall(var.clone(), domain.clone(), not_body)
74                    }
75                    // NOT(FORALL x. P(x)) → EXISTS x. NOT(P(x))
76                    TLExpr::ForAll { var, domain, body } => {
77                        stats.quantifier_negations_pushed += 1;
78                        let not_body =
79                            optimize_negations_impl(&TLExpr::negate(body.as_ref().clone()), stats);
80                        TLExpr::exists(var.clone(), domain.clone(), not_body)
81                    }
82                    // Keep negation for other expressions, but optimize inner
83                    _ => TLExpr::negate(optimize_negations_impl(inner, stats)),
84                }
85            }
86        }
87        // Recurse into subexpressions
88        TLExpr::And(a, b) => {
89            let opt_a = optimize_negations_impl(a, stats);
90            let opt_b = optimize_negations_impl(b, stats);
91            TLExpr::and(opt_a, opt_b)
92        }
93        TLExpr::Or(a, b) => {
94            let opt_a = optimize_negations_impl(a, stats);
95            let opt_b = optimize_negations_impl(b, stats);
96            TLExpr::or(opt_a, opt_b)
97        }
98        TLExpr::Imply(premise, conclusion) => {
99            let opt_premise = optimize_negations_impl(premise, stats);
100            let opt_conclusion = optimize_negations_impl(conclusion, stats);
101            TLExpr::imply(opt_premise, opt_conclusion)
102        }
103        TLExpr::Exists { var, domain, body } => {
104            let opt_body = optimize_negations_impl(body, stats);
105            TLExpr::exists(var.clone(), domain.clone(), opt_body)
106        }
107        TLExpr::ForAll { var, domain, body } => {
108            let opt_body = optimize_negations_impl(body, stats);
109            TLExpr::forall(var.clone(), domain.clone(), opt_body)
110        }
111        TLExpr::Add(a, b) => {
112            let opt_a = optimize_negations_impl(a, stats);
113            let opt_b = optimize_negations_impl(b, stats);
114            TLExpr::add(opt_a, opt_b)
115        }
116        TLExpr::Sub(a, b) => {
117            let opt_a = optimize_negations_impl(a, stats);
118            let opt_b = optimize_negations_impl(b, stats);
119            TLExpr::sub(opt_a, opt_b)
120        }
121        TLExpr::Mul(a, b) => {
122            let opt_a = optimize_negations_impl(a, stats);
123            let opt_b = optimize_negations_impl(b, stats);
124            TLExpr::mul(opt_a, opt_b)
125        }
126        TLExpr::Div(a, b) => {
127            let opt_a = optimize_negations_impl(a, stats);
128            let opt_b = optimize_negations_impl(b, stats);
129            TLExpr::div(opt_a, opt_b)
130        }
131        TLExpr::Eq(a, b) => {
132            let opt_a = optimize_negations_impl(a, stats);
133            let opt_b = optimize_negations_impl(b, stats);
134            TLExpr::eq(opt_a, opt_b)
135        }
136        TLExpr::Lt(a, b) => {
137            let opt_a = optimize_negations_impl(a, stats);
138            let opt_b = optimize_negations_impl(b, stats);
139            TLExpr::lt(opt_a, opt_b)
140        }
141        TLExpr::Gt(a, b) => {
142            let opt_a = optimize_negations_impl(a, stats);
143            let opt_b = optimize_negations_impl(b, stats);
144            TLExpr::gt(opt_a, opt_b)
145        }
146        TLExpr::Lte(a, b) => {
147            let opt_a = optimize_negations_impl(a, stats);
148            let opt_b = optimize_negations_impl(b, stats);
149            TLExpr::lte(opt_a, opt_b)
150        }
151        TLExpr::Gte(a, b) => {
152            let opt_a = optimize_negations_impl(a, stats);
153            let opt_b = optimize_negations_impl(b, stats);
154            TLExpr::gte(opt_a, opt_b)
155        }
156        TLExpr::Pow(a, b) => {
157            let opt_a = optimize_negations_impl(a, stats);
158            let opt_b = optimize_negations_impl(b, stats);
159            TLExpr::pow(opt_a, opt_b)
160        }
161        TLExpr::Mod(a, b) => {
162            let opt_a = optimize_negations_impl(a, stats);
163            let opt_b = optimize_negations_impl(b, stats);
164            TLExpr::modulo(opt_a, opt_b)
165        }
166        TLExpr::Min(a, b) => {
167            let opt_a = optimize_negations_impl(a, stats);
168            let opt_b = optimize_negations_impl(b, stats);
169            TLExpr::min(opt_a, opt_b)
170        }
171        TLExpr::Max(a, b) => {
172            let opt_a = optimize_negations_impl(a, stats);
173            let opt_b = optimize_negations_impl(b, stats);
174            TLExpr::max(opt_a, opt_b)
175        }
176        TLExpr::Abs(inner) => {
177            let opt_inner = optimize_negations_impl(inner, stats);
178            TLExpr::abs(opt_inner)
179        }
180        TLExpr::Floor(inner) => {
181            let opt_inner = optimize_negations_impl(inner, stats);
182            TLExpr::floor(opt_inner)
183        }
184        TLExpr::Ceil(inner) => {
185            let opt_inner = optimize_negations_impl(inner, stats);
186            TLExpr::ceil(opt_inner)
187        }
188        TLExpr::Round(inner) => {
189            let opt_inner = optimize_negations_impl(inner, stats);
190            TLExpr::round(opt_inner)
191        }
192        TLExpr::Sqrt(inner) => {
193            let opt_inner = optimize_negations_impl(inner, stats);
194            TLExpr::sqrt(opt_inner)
195        }
196        TLExpr::Exp(inner) => {
197            let opt_inner = optimize_negations_impl(inner, stats);
198            TLExpr::exp(opt_inner)
199        }
200        TLExpr::Log(inner) => {
201            let opt_inner = optimize_negations_impl(inner, stats);
202            TLExpr::log(opt_inner)
203        }
204        TLExpr::Sin(inner) => {
205            let opt_inner = optimize_negations_impl(inner, stats);
206            TLExpr::sin(opt_inner)
207        }
208        TLExpr::Cos(inner) => {
209            let opt_inner = optimize_negations_impl(inner, stats);
210            TLExpr::cos(opt_inner)
211        }
212        TLExpr::Tan(inner) => {
213            let opt_inner = optimize_negations_impl(inner, stats);
214            TLExpr::tan(opt_inner)
215        }
216        TLExpr::Let { var, value, body } => {
217            let opt_value = optimize_negations_impl(value, stats);
218            let opt_body = optimize_negations_impl(body, stats);
219            TLExpr::let_binding(var, opt_value, opt_body)
220        }
221        TLExpr::IfThenElse {
222            condition,
223            then_branch,
224            else_branch,
225        } => {
226            let opt_condition = optimize_negations_impl(condition, stats);
227            let opt_then = optimize_negations_impl(then_branch, stats);
228            let opt_else = optimize_negations_impl(else_branch, stats);
229            TLExpr::if_then_else(opt_condition, opt_then, opt_else)
230        }
231        TLExpr::Aggregate {
232            op,
233            var,
234            domain,
235            body,
236            group_by,
237        } => {
238            let opt_body = optimize_negations_impl(body, stats);
239            TLExpr::Aggregate {
240                op: op.clone(),
241                var: var.clone(),
242                domain: domain.clone(),
243                body: Box::new(opt_body),
244                group_by: group_by.clone(),
245            }
246        }
247        // Fuzzy logic operators
248        TLExpr::TNorm { kind, left, right } => {
249            let opt_left = optimize_negations_impl(left, stats);
250            let opt_right = optimize_negations_impl(right, stats);
251            TLExpr::TNorm {
252                kind: *kind,
253                left: Box::new(opt_left),
254                right: Box::new(opt_right),
255            }
256        }
257        TLExpr::TCoNorm { kind, left, right } => {
258            let opt_left = optimize_negations_impl(left, stats);
259            let opt_right = optimize_negations_impl(right, stats);
260            TLExpr::TCoNorm {
261                kind: *kind,
262                left: Box::new(opt_left),
263                right: Box::new(opt_right),
264            }
265        }
266        TLExpr::FuzzyNot { kind, expr: inner } => {
267            let opt_inner = optimize_negations_impl(inner, stats);
268            TLExpr::FuzzyNot {
269                kind: *kind,
270                expr: Box::new(opt_inner),
271            }
272        }
273        TLExpr::FuzzyImplication {
274            kind,
275            premise,
276            conclusion,
277        } => {
278            let opt_premise = optimize_negations_impl(premise, stats);
279            let opt_conclusion = optimize_negations_impl(conclusion, stats);
280            TLExpr::FuzzyImplication {
281                kind: *kind,
282                premise: Box::new(opt_premise),
283                conclusion: Box::new(opt_conclusion),
284            }
285        }
286        TLExpr::SoftExists {
287            var,
288            domain,
289            body,
290            temperature,
291        } => {
292            let opt_body = optimize_negations_impl(body, stats);
293            TLExpr::SoftExists {
294                var: var.clone(),
295                domain: domain.clone(),
296                body: Box::new(opt_body),
297                temperature: *temperature,
298            }
299        }
300        TLExpr::SoftForAll {
301            var,
302            domain,
303            body,
304            temperature,
305        } => {
306            let opt_body = optimize_negations_impl(body, stats);
307            TLExpr::SoftForAll {
308                var: var.clone(),
309                domain: domain.clone(),
310                body: Box::new(opt_body),
311                temperature: *temperature,
312            }
313        }
314        TLExpr::WeightedRule { weight, rule } => {
315            let opt_rule = optimize_negations_impl(rule, stats);
316            TLExpr::WeightedRule {
317                weight: *weight,
318                rule: Box::new(opt_rule),
319            }
320        }
321        TLExpr::ProbabilisticChoice { alternatives } => {
322            let opt_alts: Vec<_> = alternatives
323                .iter()
324                .map(|(w, e)| (*w, optimize_negations_impl(e, stats)))
325                .collect();
326            TLExpr::ProbabilisticChoice {
327                alternatives: opt_alts,
328            }
329        }
330
331        // Leaf expressions - return as-is
332        // Modal/temporal logic operators - not yet implemented, pass through with recursion
333        TLExpr::Box(inner) => TLExpr::Box(Box::new(optimize_negations_impl(inner, stats))),
334        TLExpr::Diamond(inner) => TLExpr::Diamond(Box::new(optimize_negations_impl(inner, stats))),
335        TLExpr::Next(inner) => TLExpr::Next(Box::new(optimize_negations_impl(inner, stats))),
336        TLExpr::Eventually(inner) => {
337            TLExpr::Eventually(Box::new(optimize_negations_impl(inner, stats)))
338        }
339        TLExpr::Always(inner) => TLExpr::Always(Box::new(optimize_negations_impl(inner, stats))),
340        TLExpr::Until { before, after } => TLExpr::Until {
341            before: Box::new(optimize_negations_impl(before, stats)),
342            after: Box::new(optimize_negations_impl(after, stats)),
343        },
344        TLExpr::Release { released, releaser } => TLExpr::Release {
345            released: Box::new(optimize_negations_impl(released, stats)),
346            releaser: Box::new(optimize_negations_impl(releaser, stats)),
347        },
348        TLExpr::WeakUntil { before, after } => TLExpr::WeakUntil {
349            before: Box::new(optimize_negations_impl(before, stats)),
350            after: Box::new(optimize_negations_impl(after, stats)),
351        },
352        TLExpr::StrongRelease { released, releaser } => TLExpr::StrongRelease {
353            released: Box::new(optimize_negations_impl(released, stats)),
354            releaser: Box::new(optimize_negations_impl(releaser, stats)),
355        },
356
357        TLExpr::Pred { .. } | TLExpr::Score { .. } | TLExpr::Constant(_) => expr.clone(),
358    }
359}
360
361#[cfg(test)]
362mod tests {
363    use super::*;
364    use tensorlogic_ir::Term;
365
366    #[test]
367    fn test_double_negation_elimination() {
368        let x = TLExpr::pred("p", vec![Term::var("x")]);
369        let not_not_x = TLExpr::negate(TLExpr::negate(x.clone()));
370
371        let (optimized, stats) = optimize_negations(&not_not_x);
372
373        assert_eq!(stats.double_negations_eliminated, 1);
374        assert_eq!(optimized, x);
375    }
376
377    #[test]
378    fn test_triple_negation() {
379        let x = TLExpr::pred("p", vec![Term::var("x")]);
380        let not_not_not_x = TLExpr::negate(TLExpr::negate(TLExpr::negate(x.clone())));
381
382        let (optimized, stats) = optimize_negations(&not_not_not_x);
383
384        assert_eq!(stats.double_negations_eliminated, 1);
385        // Should result in NOT(x)
386        matches!(optimized, TLExpr::Not(_));
387    }
388
389    #[test]
390    fn test_demorgan_and() {
391        // NOT(AND(p, q)) → OR(NOT(p), NOT(q))
392        let p = TLExpr::pred("p", vec![Term::var("x")]);
393        let q = TLExpr::pred("q", vec![Term::var("x")]);
394        let not_and = TLExpr::negate(TLExpr::and(p.clone(), q.clone()));
395
396        let (optimized, stats) = optimize_negations(&not_and);
397
398        assert_eq!(stats.demorgans_applied, 1);
399        // Should be OR(NOT(p), NOT(q))
400        matches!(optimized, TLExpr::Or(_, _));
401    }
402
403    #[test]
404    fn test_demorgan_or() {
405        // NOT(OR(p, q)) → AND(NOT(p), NOT(q))
406        let p = TLExpr::pred("p", vec![Term::var("x")]);
407        let q = TLExpr::pred("q", vec![Term::var("x")]);
408        let not_or = TLExpr::negate(TLExpr::or(p.clone(), q.clone()));
409
410        let (optimized, stats) = optimize_negations(&not_or);
411
412        assert_eq!(stats.demorgans_applied, 1);
413        // Should be AND(NOT(p), NOT(q))
414        matches!(optimized, TLExpr::And(_, _));
415    }
416
417    #[test]
418    fn test_quantifier_negation_exists() {
419        // NOT(EXISTS x. P(x)) → FORALL x. NOT(P(x))
420        let p = TLExpr::pred("p", vec![Term::var("x")]);
421        let exists = TLExpr::exists("x", "Domain", p);
422        let not_exists = TLExpr::negate(exists);
423
424        let (optimized, stats) = optimize_negations(&not_exists);
425
426        assert_eq!(stats.quantifier_negations_pushed, 1);
427        // Should be FORALL
428        matches!(optimized, TLExpr::ForAll { .. });
429    }
430
431    #[test]
432    fn test_quantifier_negation_forall() {
433        // NOT(FORALL x. P(x)) → EXISTS x. NOT(P(x))
434        let p = TLExpr::pred("p", vec![Term::var("x")]);
435        let forall = TLExpr::forall("x", "Domain", p);
436        let not_forall = TLExpr::negate(forall);
437
438        let (optimized, stats) = optimize_negations(&not_forall);
439
440        assert_eq!(stats.quantifier_negations_pushed, 1);
441        // Should be EXISTS
442        matches!(optimized, TLExpr::Exists { .. });
443    }
444
445    #[test]
446    fn test_complex_nested_negation() {
447        // NOT(AND(NOT(p), NOT(q))) should become OR(p, q)
448        let p = TLExpr::pred("p", vec![Term::var("x")]);
449        let q = TLExpr::pred("q", vec![Term::var("x")]);
450        let expr = TLExpr::negate(TLExpr::and(
451            TLExpr::negate(p.clone()),
452            TLExpr::negate(q.clone()),
453        ));
454
455        let (_optimized, stats) = optimize_negations(&expr);
456
457        // Should apply De Morgan's law and eliminate double negations
458        assert!(stats.demorgans_applied >= 1);
459        assert!(stats.double_negations_eliminated >= 2);
460    }
461
462    #[test]
463    fn test_no_optimization_needed() {
464        let x = TLExpr::pred("p", vec![Term::var("x")]);
465        let y = TLExpr::pred("q", vec![Term::var("x")]);
466        let expr = TLExpr::and(x, y);
467
468        let (optimized, stats) = optimize_negations(&expr);
469
470        assert_eq!(stats.double_negations_eliminated, 0);
471        assert_eq!(stats.demorgans_applied, 0);
472        assert_eq!(optimized, expr);
473    }
474}
tensorlogic_compiler/optimize/negation.rs

tensorlogic_compiler/optimize/
negation.rs
