Skip to main content

oxisql_parse/optimizer/
simplify.rs

1//! Predicate-simplification pass.
2//!
3//! Rewrites `Filter` predicates to a simpler, semantically-equivalent form:
4//!
5//! * Boolean-algebra identities (`x AND TRUE → x`, `x AND FALSE → FALSE`, …)
6//! * Constant numeric comparison folding (`1 = 1 → TRUE`)
7//! * De-Morgan / NOT-elimination (`NOT(NOT x) → x`, `NOT(a < b) → a >= b`)
8//! * Idempotence (`x AND x → x`)
9//! * Complement laws (`x AND NOT x → FALSE`, `x OR NOT x → TRUE`)
10//! * Single-element IN folding (`a IN (1) → a = 1`)
11//! * Per-column range coalescing across conjuncts
12//!   (`a > 5 AND a > 3 → a > 5`, `a > 10 AND a < 5 → FALSE`)
13//! * Equality dominance (`a = 5 AND a > 3 → a = 5`)
14
15use std::collections::HashMap;
16
17use sqlparser::ast::{BinaryOperator, Expr, UnaryOperator, Value, ValueWithSpan};
18use sqlparser::tokenizer::Span;
19
20use super::expr_util::{canonical_hash, join_conjuncts, parse_predicate, render, split_conjuncts};
21use super::OptPass;
22use crate::LogicalPlan;
23
24// ── Public pass struct ────────────────────────────────────────────────────────
25
26/// Simplify predicates in `Filter` and `Join` nodes to their canonical form.
27pub struct PredicateSimplification;
28
29impl OptPass for PredicateSimplification {
30    fn name(&self) -> &'static str {
31        "PredicateSimplification"
32    }
33
34    fn apply(&self, plan: LogicalPlan) -> LogicalPlan {
35        simplify_plan(plan)
36    }
37}
38
39// ── Plan-level walk ──────────────────────────────────────────────────────────
40
41pub(super) fn simplify_plan(plan: LogicalPlan) -> LogicalPlan {
42    match plan {
43        LogicalPlan::Filter { input, predicate } => {
44            let inner = simplify_plan(*input);
45            let (new_pred, always_true) = simplify_predicate_str(&predicate);
46            if always_true {
47                return inner;
48            }
49            // Detect always-false by checking if the simplified expr is FALSE literal.
50            let is_always_false = parse_predicate(&new_pred)
51                .and_then(|e| is_bool_lit(&e))
52                .map(|b| !b)
53                .unwrap_or(false);
54            if is_always_false {
55                return LogicalPlan::Empty;
56            }
57            LogicalPlan::Filter {
58                input: Box::new(inner),
59                predicate: new_pred,
60            }
61        }
62
63        LogicalPlan::Join {
64            left,
65            right,
66            on,
67            join_type,
68            algo_hint,
69        } => {
70            let new_on = if on.is_empty() {
71                on
72            } else {
73                simplify_predicate_str(&on).0
74            };
75            LogicalPlan::Join {
76                left: Box::new(simplify_plan(*left)),
77                right: Box::new(simplify_plan(*right)),
78                on: new_on,
79                join_type,
80                algo_hint,
81            }
82        }
83
84        LogicalPlan::Project { input, columns } => LogicalPlan::Project {
85            input: Box::new(simplify_plan(*input)),
86            columns,
87        },
88        LogicalPlan::Aggregate {
89            input,
90            group_by,
91            aggregates,
92        } => LogicalPlan::Aggregate {
93            input: Box::new(simplify_plan(*input)),
94            group_by,
95            aggregates,
96        },
97        LogicalPlan::Sort { input, order_by } => LogicalPlan::Sort {
98            input: Box::new(simplify_plan(*input)),
99            order_by,
100        },
101        LogicalPlan::Limit {
102            input,
103            count,
104            offset,
105        } => LogicalPlan::Limit {
106            input: Box::new(simplify_plan(*input)),
107            count,
108            offset,
109        },
110        LogicalPlan::Window { input, functions } => LogicalPlan::Window {
111            input: Box::new(simplify_plan(*input)),
112            functions,
113        },
114        LogicalPlan::Cte {
115            name,
116            query,
117            recursive,
118        } => LogicalPlan::Cte {
119            name,
120            query: Box::new(simplify_plan(*query)),
121            recursive,
122        },
123        LogicalPlan::Subquery { query, alias } => LogicalPlan::Subquery {
124            query: Box::new(simplify_plan(*query)),
125            alias,
126        },
127        LogicalPlan::Exists { subquery, negated } => LogicalPlan::Exists {
128            subquery: Box::new(simplify_plan(*subquery)),
129            negated,
130        },
131        LogicalPlan::InSubquery {
132            expr,
133            subquery,
134            negated,
135        } => LogicalPlan::InSubquery {
136            expr,
137            subquery: Box::new(simplify_plan(*subquery)),
138            negated,
139        },
140        LogicalPlan::Compute { input, bindings } => LogicalPlan::Compute {
141            input: Box::new(simplify_plan(*input)),
142            bindings,
143        },
144        LogicalPlan::SetOp {
145            op,
146            all,
147            left,
148            right,
149        } => LogicalPlan::SetOp {
150            op,
151            all,
152            left: Box::new(simplify_plan(*left)),
153            right: Box::new(simplify_plan(*right)),
154        },
155        // Leaves: Scan, Values, Empty, CteRef
156        other => other,
157    }
158}
159
160// ── Predicate-string simplification ─────────────────────────────────────────
161
162/// Simplify a predicate string to a fixpoint.
163///
164/// Returns `(simplified_predicate, is_always_true)`.
165/// On parse failure the original string is returned unchanged with `false`.
166pub(super) fn simplify_predicate_str(pred: &str) -> (String, bool) {
167    let Some(mut e) = parse_predicate(pred) else {
168        return (pred.to_string(), false);
169    };
170    for _ in 0..20 {
171        let new_e = simplify_expr(e.clone());
172        let same = canonical_hash(&new_e) == canonical_hash(&e);
173        e = new_e;
174        if same {
175            break;
176        }
177    }
178    let is_true = is_bool_lit(&e) == Some(true);
179    (render(&e), is_true)
180}
181
182// ── Expression simplifier ────────────────────────────────────────────────────
183
184/// Recursively simplify an expression bottom-up to a fixpoint.
185pub(crate) fn simplify_expr(e: Expr) -> Expr {
186    // Step 1: recurse into children so rules apply bottom-up.
187    let e = apply_to_children(e);
188    // Step 2: apply single-node rules.
189    let e = apply_bool_rules(e);
190    // Step 3: conjunct-level range reasoning if this is an AND tree.
191    let conjuncts = split_conjuncts(e.clone());
192    if conjuncts.len() > 1 {
193        let (simplified, always_false) = simplify_conjuncts(conjuncts);
194        if always_false {
195            return make_bool(false);
196        }
197        match join_conjuncts(simplified) {
198            Some(joined) => joined,
199            None => make_bool(true),
200        }
201    } else {
202        e
203    }
204}
205
206/// Apply `simplify_expr` to every direct child of `e`.
207fn apply_to_children(e: Expr) -> Expr {
208    match e {
209        Expr::BinaryOp { left, op, right } => Expr::BinaryOp {
210            left: Box::new(simplify_expr(*left)),
211            op,
212            right: Box::new(simplify_expr(*right)),
213        },
214        Expr::UnaryOp { op, expr } => Expr::UnaryOp {
215            op,
216            expr: Box::new(simplify_expr(*expr)),
217        },
218        Expr::Nested(inner) => Expr::Nested(Box::new(simplify_expr(*inner))),
219        Expr::Between {
220            expr,
221            negated,
222            low,
223            high,
224        } => Expr::Between {
225            expr: Box::new(simplify_expr(*expr)),
226            negated,
227            low: Box::new(simplify_expr(*low)),
228            high: Box::new(simplify_expr(*high)),
229        },
230        Expr::InList {
231            expr,
232            list,
233            negated,
234        } => Expr::InList {
235            expr: Box::new(simplify_expr(*expr)),
236            list: list.into_iter().map(simplify_expr).collect(),
237            negated,
238        },
239        other => other,
240    }
241}
242
243// ── Boolean algebra rules ────────────────────────────────────────────────────
244
245fn apply_bool_rules(e: Expr) -> Expr {
246    use BinaryOperator as B;
247    use UnaryOperator as U;
248
249    match e {
250        // Unwrap nested (already recursed, just strip the wrapper)
251        Expr::Nested(inner) => *inner,
252
253        Expr::BinaryOp { left, op, right } => {
254            let l = *left;
255            let r = *right;
256
257            // Numeric literal comparison folding: 1 = 1 → TRUE, 1 = 2 → FALSE, etc.
258            if let (Some(lv), Some(rv)) = (numeric_val(&l), numeric_val(&r)) {
259                let folded = match &op {
260                    B::Eq => Some((lv - rv).abs() < f64::EPSILON),
261                    B::NotEq => Some((lv - rv).abs() >= f64::EPSILON),
262                    B::Lt => Some(lv < rv),
263                    B::LtEq => Some(lv <= rv),
264                    B::Gt => Some(lv > rv),
265                    B::GtEq => Some(lv >= rv),
266                    _ => None,
267                };
268                if let Some(b) = folded {
269                    return make_bool(b);
270                }
271            }
272
273            match op {
274                B::And => {
275                    if is_bool_lit(&l) == Some(true) {
276                        return r;
277                    }
278                    if is_bool_lit(&r) == Some(true) {
279                        return l;
280                    }
281                    if is_bool_lit(&l) == Some(false) {
282                        return make_bool(false);
283                    }
284                    if is_bool_lit(&r) == Some(false) {
285                        return make_bool(false);
286                    }
287                    // Idempotence: x AND x → x
288                    if canonical_hash(&l) == canonical_hash(&r) {
289                        return l;
290                    }
291                    // Complement: x AND NOT(x) → FALSE
292                    if let Expr::UnaryOp {
293                        op: U::Not,
294                        expr: ref neg,
295                    } = r
296                    {
297                        if canonical_hash(&l) == canonical_hash(neg) {
298                            return make_bool(false);
299                        }
300                    }
301                    if let Expr::UnaryOp {
302                        op: U::Not,
303                        expr: ref neg,
304                    } = l
305                    {
306                        if canonical_hash(&r) == canonical_hash(neg) {
307                            return make_bool(false);
308                        }
309                    }
310                    Expr::BinaryOp {
311                        left: Box::new(l),
312                        op: B::And,
313                        right: Box::new(r),
314                    }
315                }
316                B::Or => {
317                    if is_bool_lit(&l) == Some(false) {
318                        return r;
319                    }
320                    if is_bool_lit(&r) == Some(false) {
321                        return l;
322                    }
323                    if is_bool_lit(&l) == Some(true) {
324                        return make_bool(true);
325                    }
326                    if is_bool_lit(&r) == Some(true) {
327                        return make_bool(true);
328                    }
329                    // Idempotence: x OR x → x
330                    if canonical_hash(&l) == canonical_hash(&r) {
331                        return l;
332                    }
333                    // Complement: x OR NOT(x) → TRUE
334                    if let Expr::UnaryOp {
335                        op: U::Not,
336                        expr: ref neg,
337                    } = r
338                    {
339                        if canonical_hash(&l) == canonical_hash(neg) {
340                            return make_bool(true);
341                        }
342                    }
343                    if let Expr::UnaryOp {
344                        op: U::Not,
345                        expr: ref neg,
346                    } = l
347                    {
348                        if canonical_hash(&r) == canonical_hash(neg) {
349                            return make_bool(true);
350                        }
351                    }
352                    Expr::BinaryOp {
353                        left: Box::new(l),
354                        op: B::Or,
355                        right: Box::new(r),
356                    }
357                }
358                _ => Expr::BinaryOp {
359                    left: Box::new(l),
360                    op,
361                    right: Box::new(r),
362                },
363            }
364        }
365
366        Expr::UnaryOp { op, expr } => {
367            let inner = *expr;
368            match op {
369                U::Not => {
370                    // NOT NOT x → x
371                    if let Expr::UnaryOp {
372                        op: U::Not,
373                        expr: inner2,
374                    } = inner
375                    {
376                        return *inner2;
377                    }
378                    // NOT TRUE → FALSE, NOT FALSE → TRUE
379                    if let Some(b) = is_bool_lit(&inner) {
380                        return make_bool(!b);
381                    }
382                    // NOT comparison → flip
383                    if let Expr::BinaryOp {
384                        ref left,
385                        ref op,
386                        ref right,
387                    } = inner
388                    {
389                        if let Some(neg_op) = negate_comparison(op) {
390                            return Expr::BinaryOp {
391                                left: left.clone(),
392                                op: neg_op,
393                                right: right.clone(),
394                            };
395                        }
396                    }
397                    Expr::UnaryOp {
398                        op: U::Not,
399                        expr: Box::new(inner),
400                    }
401                }
402                _ => Expr::UnaryOp {
403                    op,
404                    expr: Box::new(inner),
405                },
406            }
407        }
408
409        // IN (single item) → equality or inequality
410        Expr::InList {
411            expr,
412            mut list,
413            negated,
414        } if list.len() == 1 => {
415            let item = list.remove(0);
416            Expr::BinaryOp {
417                left: expr,
418                op: if negated {
419                    BinaryOperator::NotEq
420                } else {
421                    BinaryOperator::Eq
422                },
423                right: Box::new(item),
424            }
425        }
426
427        other => other,
428    }
429}
430
431// ── Per-column range reasoning ────────────────────────────────────────────────
432
433#[derive(Debug, Clone, PartialEq)]
434enum BoundKind {
435    Gt,
436    GtEq,
437    Lt,
438    LtEq,
439    Eq,
440}
441
442#[derive(Debug, Clone)]
443struct ColNumericBound {
444    kind: BoundKind,
445    value: f64,
446    original: Expr,
447}
448
449/// Simplify a list of conjuncts using per-column range reasoning.
450///
451/// Returns `(simplified_conjuncts, always_false)`.
452fn simplify_conjuncts(conjuncts: Vec<Expr>) -> (Vec<Expr>, bool) {
453    let mut col_groups: HashMap<String, Vec<ColNumericBound>> = HashMap::new();
454    let mut other: Vec<Expr> = Vec::new();
455
456    for e in conjuncts {
457        if let Some((col_key, bound)) = extract_numeric_col_bound(&e) {
458            col_groups.entry(col_key).or_default().push(bound);
459        } else {
460            other.push(e);
461        }
462    }
463
464    let mut result = other;
465    for (_col_key, bounds) in col_groups {
466        let (simplified_exprs, is_false) = merge_numeric_bounds(bounds);
467        if is_false {
468            return (vec![], true);
469        }
470        result.extend(simplified_exprs);
471    }
472
473    (result, false)
474}
475
476/// Try to extract a single-column numeric bound from `e`.
477///
478/// Returns `Some((col_key, bound))` for comparisons of the form `col op lit`
479/// or `lit op col`, where `col` is a bare or qualified identifier and `lit` is
480/// a numeric literal.
481fn extract_numeric_col_bound(e: &Expr) -> Option<(String, ColNumericBound)> {
482    let Expr::BinaryOp { left, op, right } = e else {
483        return None;
484    };
485
486    // col op lit (normal orientation)
487    if let Some(col_key) = expr_col_key(left) {
488        if let Some(val) = numeric_val(right) {
489            let kind = op_to_bound_kind(op, false)?;
490            return Some((
491                col_key,
492                ColNumericBound {
493                    kind,
494                    value: val,
495                    original: e.clone(),
496                },
497            ));
498        }
499    }
500
501    // lit op col (flipped orientation, e.g. 5 < a ≡ a > 5)
502    if let Some(col_key) = expr_col_key(right) {
503        if let Some(val) = numeric_val(left) {
504            let kind = op_to_bound_kind(op, true)?;
505            return Some((
506                col_key,
507                ColNumericBound {
508                    kind,
509                    value: val,
510                    original: e.clone(),
511                },
512            ));
513        }
514    }
515
516    None
517}
518
519fn expr_col_key(e: &Expr) -> Option<String> {
520    match e {
521        Expr::Identifier(id) => Some(id.value.clone()),
522        Expr::CompoundIdentifier(parts) => Some(
523            parts
524                .iter()
525                .map(|p| p.value.as_str())
526                .collect::<Vec<_>>()
527                .join("."),
528        ),
529        _ => None,
530    }
531}
532
533fn op_to_bound_kind(op: &BinaryOperator, flipped: bool) -> Option<BoundKind> {
534    let kind = match op {
535        BinaryOperator::Gt => {
536            if flipped {
537                BoundKind::Lt
538            } else {
539                BoundKind::Gt
540            }
541        }
542        BinaryOperator::GtEq => {
543            if flipped {
544                BoundKind::LtEq
545            } else {
546                BoundKind::GtEq
547            }
548        }
549        BinaryOperator::Lt => {
550            if flipped {
551                BoundKind::Gt
552            } else {
553                BoundKind::Lt
554            }
555        }
556        BinaryOperator::LtEq => {
557            if flipped {
558                BoundKind::GtEq
559            } else {
560                BoundKind::LtEq
561            }
562        }
563        BinaryOperator::Eq => BoundKind::Eq,
564        _ => return None,
565    };
566    Some(kind)
567}
568
569/// Merge a set of single-column numeric bounds into the strictest satisfiable set.
570///
571/// Returns `(simplified_exprs, always_false)`.
572fn merge_numeric_bounds(bounds: Vec<ColNumericBound>) -> (Vec<Expr>, bool) {
573    let mut equalities: Vec<(f64, Expr)> = Vec::new();
574    // (value, is_strict, original)
575    let mut lower_bounds: Vec<(f64, bool, Expr)> = Vec::new();
576    let mut upper_bounds: Vec<(f64, bool, Expr)> = Vec::new();
577
578    for b in bounds {
579        match b.kind {
580            BoundKind::Gt => lower_bounds.push((b.value, true, b.original)),
581            BoundKind::GtEq => lower_bounds.push((b.value, false, b.original)),
582            BoundKind::Lt => upper_bounds.push((b.value, true, b.original)),
583            BoundKind::LtEq => upper_bounds.push((b.value, false, b.original)),
584            BoundKind::Eq => equalities.push((b.value, b.original)),
585        }
586    }
587
588    // Equality contradiction: two distinct equality values
589    if equalities.len() > 1 {
590        let first = equalities[0].0;
591        if equalities
592            .iter()
593            .any(|(v, _)| (*v - first).abs() > f64::EPSILON)
594        {
595            return (vec![], true);
596        }
597    }
598
599    // Strictest lower bound: highest value; prefer strict (Gt) over inclusive (GtEq) at same value.
600    let best_lower = lower_bounds.into_iter().max_by(|a, b| {
601        a.0.partial_cmp(&b.0)
602            .unwrap_or(std::cmp::Ordering::Equal)
603            .then_with(|| match (a.1, b.1) {
604                (true, false) => std::cmp::Ordering::Greater,
605                (false, true) => std::cmp::Ordering::Less,
606                _ => std::cmp::Ordering::Equal,
607            })
608    });
609
610    // Strictest upper bound: lowest value; prefer strict (Lt) over inclusive (LtEq) at same value.
611    let best_upper = upper_bounds.into_iter().min_by(|a, b| {
612        a.0.partial_cmp(&b.0)
613            .unwrap_or(std::cmp::Ordering::Equal)
614            .then_with(|| match (a.1, b.1) {
615                (true, false) => std::cmp::Ordering::Greater,
616                (false, true) => std::cmp::Ordering::Less,
617                _ => std::cmp::Ordering::Equal,
618            })
619    });
620
621    // Equality dominance: equality must be within [lower, upper]
622    if let Some((eq_val, eq_expr)) = equalities.into_iter().next() {
623        if let Some((lb, strict, _)) = &best_lower {
624            let violates = if *strict { eq_val <= *lb } else { eq_val < *lb };
625            if violates {
626                return (vec![], true);
627            }
628        }
629        if let Some((ub, strict, _)) = &best_upper {
630            let violates = if *strict { eq_val >= *ub } else { eq_val > *ub };
631            if violates {
632                return (vec![], true);
633            }
634        }
635        // Equality dominates all bounds.
636        return (vec![eq_expr], false);
637    }
638
639    // Check lower-upper contradiction
640    if let (Some((lb, lb_strict, _)), Some((ub, ub_strict, _))) = (&best_lower, &best_upper) {
641        if lb > ub {
642            return (vec![], true);
643        }
644        if (lb - ub).abs() < f64::EPSILON && (*lb_strict || *ub_strict) {
645            return (vec![], true);
646        }
647    }
648
649    let mut result = Vec::new();
650    if let Some((_, _, orig)) = best_lower {
651        result.push(orig);
652    }
653    if let Some((_, _, orig)) = best_upper {
654        result.push(orig);
655    }
656    (result, false)
657}
658
659// ── Helpers ───────────────────────────────────────────────────────────────────
660
661fn make_bool(b: bool) -> Expr {
662    Expr::Value(ValueWithSpan {
663        value: Value::Boolean(b),
664        span: Span::empty(),
665    })
666}
667
668fn is_bool_lit(e: &Expr) -> Option<bool> {
669    match e {
670        Expr::Value(ValueWithSpan {
671            value: Value::Boolean(b),
672            ..
673        }) => Some(*b),
674        _ => None,
675    }
676}
677
678fn numeric_val(e: &Expr) -> Option<f64> {
679    match e {
680        Expr::Value(ValueWithSpan {
681            value: Value::Number(s, _),
682            ..
683        }) => s.parse::<f64>().ok(),
684        _ => None,
685    }
686}
687
688fn negate_comparison(op: &BinaryOperator) -> Option<BinaryOperator> {
689    match op {
690        BinaryOperator::Eq => Some(BinaryOperator::NotEq),
691        BinaryOperator::NotEq => Some(BinaryOperator::Eq),
692        BinaryOperator::Lt => Some(BinaryOperator::GtEq),
693        BinaryOperator::LtEq => Some(BinaryOperator::Gt),
694        BinaryOperator::Gt => Some(BinaryOperator::LtEq),
695        BinaryOperator::GtEq => Some(BinaryOperator::Lt),
696        _ => None,
697    }
698}
699
700// ── Tests ─────────────────────────────────────────────────────────────────────
701
702#[cfg(test)]
703mod tests {
704    use super::*;
705    use crate::optimizer::expr_util::parse_predicate;
706
707    fn simplify_str(pred: &str) -> String {
708        simplify_predicate_str(pred).0
709    }
710
711    fn simplify_is_true(pred: &str) -> bool {
712        simplify_predicate_str(pred).1
713    }
714
715    fn filter(pred: &str) -> LogicalPlan {
716        LogicalPlan::Filter {
717            input: Box::new(LogicalPlan::Scan {
718                table: "t".to_string(),
719                alias: None,
720                limit: None,
721            }),
722            predicate: pred.to_string(),
723        }
724    }
725
726    // 1. TRUE identity eliminates
727    #[test]
728    fn test_true_identity() {
729        let pred = "1 = 1 AND x > 0";
730        assert_eq!(simplify_str(pred), "x > 0");
731        assert!(!simplify_is_true(pred));
732    }
733
734    // 2. AND FALSE → Empty
735    #[test]
736    fn test_and_false_empty() {
737        let plan = filter("x > 0 AND FALSE");
738        let result = PredicateSimplification.apply(plan);
739        assert!(matches!(result, LogicalPlan::Empty));
740    }
741
742    // 3. Range coalescing: a > 5 AND a > 3 → a > 5
743    #[test]
744    fn test_range_coalesce_lower_bound() {
745        let simplified = simplify_str("a > 5 AND a > 3");
746        // Should be just a > 5
747        assert!(
748            simplified.contains("> 5") || simplified.contains(">5"),
749            "got: {simplified}"
750        );
751        assert!(
752            !simplified.contains("> 3"),
753            "should not contain > 3: {simplified}"
754        );
755    }
756
757    // 4. Contradiction: a > 10 AND a < 5 → Empty
758    #[test]
759    fn test_contradiction_empty() {
760        let plan = filter("a > 10 AND a < 5");
761        let result = PredicateSimplification.apply(plan);
762        assert!(matches!(result, LogicalPlan::Empty), "got {result:?}");
763    }
764
765    // 5. Equality contradiction: a = 5 AND a = 6 → Empty
766    #[test]
767    fn test_equality_contradiction() {
768        let plan = filter("a = 5 AND a = 6");
769        let result = PredicateSimplification.apply(plan);
770        assert!(matches!(result, LogicalPlan::Empty), "got {result:?}");
771    }
772
773    // 6. Idempotence: x > 0 AND x > 0 → x > 0
774    #[test]
775    fn test_idempotence() {
776        let simplified = simplify_str("x > 0 AND x > 0");
777        let e = parse_predicate(&simplified).expect("parse");
778        // Should be a single expression (no AND)
779        assert!(
780            !matches!(
781                e,
782                Expr::BinaryOp {
783                    op: BinaryOperator::And,
784                    ..
785                }
786            ),
787            "expected single conjunct, got: {simplified}"
788        );
789    }
790
791    // 7. IN (1) → equality
792    #[test]
793    fn test_in_single_element() {
794        let simplified = simplify_str("a IN (1)");
795        // Should be rewritten to a = 1
796        assert!(
797            simplified.contains('=') && !simplified.contains("IN"),
798            "expected equality, got: {simplified}"
799        );
800    }
801
802    // 8. NOT NOT elimination
803    #[test]
804    fn test_not_not_elimination() {
805        let simplified = simplify_str("NOT (NOT (x > 0))");
806        assert!(
807            simplified.contains('>'),
808            "expected x > 0, got: {simplified}"
809        );
810    }
811
812    // 9. NOT comparison flip
813    #[test]
814    fn test_not_comparison_flip() {
815        let simplified = simplify_str("NOT (a < b)");
816        // NOT(a < b) → a >= b
817        assert!(simplified.contains(">="), "expected >=, got: {simplified}");
818    }
819
820    // 10. Equality dominance: a = 5 AND a > 3 → a = 5
821    #[test]
822    fn test_equality_dominance() {
823        let simplified = simplify_str("a = 5 AND a > 3");
824        assert!(
825            simplified.contains("= 5"),
826            "expected a = 5, got: {simplified}"
827        );
828        assert!(
829            !simplified.contains("> 3"),
830            "should not contain > 3: {simplified}"
831        );
832    }
833}