sea_core/policy/
normalize.rs

1//! Canonical Expression Normalizer
2//!
3//! Transforms policy expressions into a deterministic, minimal canonical form.
4//! This enables:
5//! - Semantic equivalence checking via normalized comparison
6//! - Stable caching with deterministic hash keys
7//! - Consistent hover signatures in LSP
8//! - Deterministic golden test output
9//!
10//! # Normalization Rules Applied
11//!
12//! 1. **Commutativity**: Sort operands of AND/OR/==/!=/+/* lexicographically
13//! 2. **Identity**: Remove identity elements (`true AND x` → `x`, `false OR x` → `x`)
14//! 3. **Idempotence**: Deduplicate identical operands (`a AND a` → `a`)
15//! 4. **Absorption**: Remove absorbed terms (`a OR (a AND b)` → `a`)
16//! 5. **Domination**: Short-circuit dominating elements (`false AND x` → `false`)
17//! 6. **Double Negation**: Eliminate `NOT NOT x` → `x`
18//! 7. **Chain Flattening**: Flatten nested same-operator chains
19//! 8. Comparison negation: NOT (a == b) → a != b
20
21use super::{BinaryOp, Expression, UnaryOp};
22use std::fmt;
23use std::hash::{Hash, Hasher};
24use xxhash_rust::xxh64::Xxh64;
25
26/// A normalized expression with precomputed stable hash.
27///
28/// `NormalizedExpression` wraps an `Expression` that has been transformed
29/// into canonical form, along with a stable hash value that remains consistent
30/// across runs and platforms.
31#[derive(Clone)]
32pub struct NormalizedExpression {
33    inner: Expression,
34    hash: u64,
35}
36
37impl NormalizedExpression {
38    /// Create a normalized form of the given expression.
39    pub fn new(expr: &Expression) -> Self {
40        let normalized = normalize_expr(expr);
41        let hash = compute_stable_hash(&normalized);
42        Self {
43            inner: normalized,
44            hash,
45        }
46    }
47
48    /// Access the normalized expression.
49    pub fn inner(&self) -> &Expression {
50        &self.inner
51    }
52
53    /// Consume and return the inner normalized expression.
54    pub fn into_inner(self) -> Expression {
55        self.inner
56    }
57
58    /// Get the stable hash value for this normalized expression.
59    ///
60    /// This hash is deterministic across runs and platforms, making it
61    /// suitable for cache keys.
62    pub fn stable_hash(&self) -> u64 {
63        self.hash
64    }
65}
66
67impl PartialEq for NormalizedExpression {
68    fn eq(&self, other: &Self) -> bool {
69        // Fast path: compare hashes first
70        self.hash == other.hash && self.inner == other.inner
71    }
72}
73
74impl Eq for NormalizedExpression {}
75
76impl Hash for NormalizedExpression {
77    fn hash<H: Hasher>(&self, state: &mut H) {
78        self.hash.hash(state);
79    }
80}
81
82impl fmt::Display for NormalizedExpression {
83    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
84        write!(f, "{}", self.inner)
85    }
86}
87
88impl fmt::Debug for NormalizedExpression {
89    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
90        f.debug_struct("NormalizedExpression")
91            .field("inner", &self.inner)
92            .field("hash", &format!("{:016x}", self.hash))
93            .finish()
94    }
95}
96
97// ============================================================================
98// Stable Hashing
99// ============================================================================
100
101/// Compute a stable hash using Xxh64 which is portable and deterministic.
102fn compute_stable_hash(expr: &Expression) -> u64 {
103    // Use a fixed seed (0) for stability across runs and updates
104    let mut hasher = Xxh64::new(0);
105    hash_expression(expr, &mut hasher);
106    hasher.finish()
107}
108
109/// Recursively hash an expression in a stable, deterministic manner.
110fn hash_expression<H: Hasher>(expr: &Expression, hasher: &mut H) {
111    // Hash discriminant first for type differentiation
112    std::mem::discriminant(expr).hash(hasher);
113
114    match expr {
115        Expression::Literal(v) => {
116            // Use string representation for consistent JSON value hashing
117            v.to_string().hash(hasher);
118        }
119        Expression::Variable(s) => s.hash(hasher),
120        Expression::QuantityLiteral { value, unit } => {
121            value.to_string().hash(hasher);
122            unit.hash(hasher);
123        }
124        Expression::TimeLiteral(s) => s.hash(hasher),
125        Expression::IntervalLiteral { start, end } => {
126            start.hash(hasher);
127            end.hash(hasher);
128        }
129        Expression::MemberAccess { object, member } => {
130            object.hash(hasher);
131            member.hash(hasher);
132        }
133        Expression::Binary { op, left, right } => {
134            std::mem::discriminant(op).hash(hasher);
135            hash_expression(left, hasher);
136            hash_expression(right, hasher);
137        }
138        Expression::Unary { op, operand } => {
139            std::mem::discriminant(op).hash(hasher);
140            hash_expression(operand, hasher);
141        }
142        Expression::Cast {
143            operand,
144            target_type,
145        } => {
146            hash_expression(operand, hasher);
147            target_type.hash(hasher);
148        }
149        Expression::Quantifier {
150            quantifier,
151            variable,
152            collection,
153            condition,
154        } => {
155            std::mem::discriminant(quantifier).hash(hasher);
156            variable.hash(hasher);
157            hash_expression(collection, hasher);
158            hash_expression(condition, hasher);
159        }
160        Expression::GroupBy {
161            variable,
162            collection,
163            filter,
164            key,
165            condition,
166        } => {
167            variable.hash(hasher);
168            hash_expression(collection, hasher);
169            if let Some(f) = filter {
170                true.hash(hasher);
171                hash_expression(f, hasher);
172            } else {
173                false.hash(hasher);
174            }
175            hash_expression(key, hasher);
176            hash_expression(condition, hasher);
177        }
178        Expression::Aggregation {
179            function,
180            collection,
181            field,
182            filter,
183        } => {
184            std::mem::discriminant(function).hash(hasher);
185            hash_expression(collection, hasher);
186            field.hash(hasher);
187            if let Some(f) = filter {
188                true.hash(hasher);
189                hash_expression(f, hasher);
190            } else {
191                false.hash(hasher);
192            }
193        }
194        Expression::AggregationComprehension {
195            function,
196            variable,
197            collection,
198            window,
199            predicate,
200            projection,
201            target_unit,
202        } => {
203            std::mem::discriminant(function).hash(hasher);
204            variable.hash(hasher);
205            hash_expression(collection, hasher);
206            if let Some(w) = window {
207                true.hash(hasher);
208                w.duration.hash(hasher);
209                w.unit.hash(hasher);
210            } else {
211                false.hash(hasher);
212            }
213            hash_expression(predicate, hasher);
214            hash_expression(projection, hasher);
215            target_unit.hash(hasher);
216        }
217    }
218}
219
220// ============================================================================
221// Main Normalization Logic
222// ============================================================================
223
224/// Normalize an expression into canonical form.
225fn normalize_expr(expr: &Expression) -> Expression {
226    match expr {
227        // Leaf nodes: pass through as-is
228        Expression::Literal(_)
229        | Expression::Variable(_)
230        | Expression::QuantityLiteral { .. }
231        | Expression::TimeLiteral(_)
232        | Expression::IntervalLiteral { .. }
233        | Expression::MemberAccess { .. } => expr.clone(),
234
235        // Binary: normalize children, apply optimizations, sort commutative ops
236        Expression::Binary { op, left, right } => {
237            let l = normalize_expr(left);
238            let r = normalize_expr(right);
239            normalize_binary(op.clone(), l, r)
240        }
241
242        // Unary: normalize child, apply double negation and De Morgan
243        Expression::Unary { op, operand } => {
244            let inner = normalize_expr(operand);
245            normalize_unary(op.clone(), inner)
246        }
247
248        // Cast: normalize operand
249        Expression::Cast {
250            operand,
251            target_type,
252        } => Expression::Cast {
253            operand: Box::new(normalize_expr(operand)),
254            target_type: target_type.clone(),
255        },
256
257        // Quantifier: normalize collection and condition
258        Expression::Quantifier {
259            quantifier,
260            variable,
261            collection,
262            condition,
263        } => Expression::Quantifier {
264            quantifier: quantifier.clone(),
265            variable: variable.clone(),
266            collection: Box::new(normalize_expr(collection)),
267            condition: Box::new(normalize_expr(condition)),
268        },
269
270        // GroupBy: normalize all sub-expressions
271        Expression::GroupBy {
272            variable,
273            collection,
274            filter,
275            key,
276            condition,
277        } => Expression::GroupBy {
278            variable: variable.clone(),
279            collection: Box::new(normalize_expr(collection)),
280            filter: filter.as_ref().map(|f| Box::new(normalize_expr(f))),
281            key: Box::new(normalize_expr(key)),
282            condition: Box::new(normalize_expr(condition)),
283        },
284
285        // Aggregation: normalize sub-expressions
286        Expression::Aggregation {
287            function,
288            collection,
289            field,
290            filter,
291        } => Expression::Aggregation {
292            function: function.clone(),
293            collection: Box::new(normalize_expr(collection)),
294            field: field.clone(),
295            filter: filter.as_ref().map(|f| Box::new(normalize_expr(f))),
296        },
297
298        // AggregationComprehension: normalize sub-expressions
299        Expression::AggregationComprehension {
300            function,
301            variable,
302            collection,
303            window,
304            predicate,
305            projection,
306            target_unit,
307        } => Expression::AggregationComprehension {
308            function: function.clone(),
309            variable: variable.clone(),
310            collection: Box::new(normalize_expr(collection)),
311            window: window.clone(),
312            predicate: Box::new(normalize_expr(predicate)),
313            projection: Box::new(normalize_expr(projection)),
314            target_unit: target_unit.clone(),
315        },
316    }
317}
318
319// ============================================================================
320// Binary Expression Normalization
321// ============================================================================
322
323/// Normalize a binary expression with comprehensive optimization rules.
324fn normalize_binary(op: BinaryOp, left: Expression, right: Expression) -> Expression {
325    // 1. Identity elimination for AND
326    if op == BinaryOp::And {
327        if is_true_literal(&left) {
328            return right;
329        }
330        if is_true_literal(&right) {
331            return left;
332        }
333    }
334
335    // 2. Identity elimination for OR
336    if op == BinaryOp::Or {
337        if is_false_literal(&left) {
338            return right;
339        }
340        if is_false_literal(&right) {
341            return left;
342        }
343    }
344
345    // 3. Domination rules (short-circuit)
346    if op == BinaryOp::And && (is_false_literal(&left) || is_false_literal(&right)) {
347        return Expression::Literal(serde_json::Value::Bool(false));
348    }
349    if op == BinaryOp::Or && (is_true_literal(&left) || is_true_literal(&right)) {
350        return Expression::Literal(serde_json::Value::Bool(true));
351    }
352
353    // 4. Idempotence: a AND a → a, a OR a → a
354    if (op == BinaryOp::And || op == BinaryOp::Or) && left == right {
355        return left;
356    }
357
358    // 5. Absorption: a OR (a AND b) → a, a AND (a OR b) → a
359    if op == BinaryOp::Or {
360        if let Some(result) = try_absorb(&left, &right, BinaryOp::And) {
361            return result;
362        }
363        if let Some(result) = try_absorb(&right, &left, BinaryOp::And) {
364            return result;
365        }
366    }
367    if op == BinaryOp::And {
368        if let Some(result) = try_absorb(&left, &right, BinaryOp::Or) {
369            return result;
370        }
371        if let Some(result) = try_absorb(&right, &left, BinaryOp::Or) {
372            return result;
373        }
374    }
375
376    // 6. Flatten chains: (a AND b) AND c → collect [a, b, c] and rebuild sorted
377    if is_commutative(&op) {
378        let mut operands = collect_chain(&op, &left);
379        operands.extend(collect_chain(&op, &right));
380
381        // Deduplicate (idempotence across chain)
382        operands.sort_by_key(expr_cmp_key);
383        operands.dedup();
384
385        // Re-apply absorption across the flattened chain
386        // e.g. (A) AND (A OR B) -> A
387        let partner_op = match op {
388            BinaryOp::Or => Some(BinaryOp::And),
389            BinaryOp::And => Some(BinaryOp::Or),
390            _ => None,
391        };
392
393        if let Some(partner) = partner_op {
394            let mut indices_to_remove = std::collections::HashSet::new();
395            for i in 0..operands.len() {
396                if indices_to_remove.contains(&i) {
397                    continue;
398                }
399                for j in (i + 1)..operands.len() {
400                    if indices_to_remove.contains(&j) {
401                        continue;
402                    }
403
404                    // Check if i absorbs j
405                    if try_absorb(&operands[i], &operands[j], partner.clone()).is_some() {
406                        indices_to_remove.insert(j);
407                        continue;
408                    }
409
410                    // Check if j absorbs i
411                    if try_absorb(&operands[j], &operands[i], partner.clone()).is_some() {
412                        indices_to_remove.insert(i);
413                        break; // i is removed, move to next i
414                    }
415                }
416            }
417
418            if !indices_to_remove.is_empty() {
419                let mut new_operands = Vec::with_capacity(operands.len() - indices_to_remove.len());
420                for (i, op) in operands.into_iter().enumerate() {
421                    if !indices_to_remove.contains(&i) {
422                        new_operands.push(op);
423                    }
424                }
425                operands = new_operands;
426                // Re-sort/dedup not strictly necessary if order preserved and absorption is clean,
427                // but good for safety if absorption produced duplicates (unlikely here).
428            }
429        }
430
431        // Rebuild balanced tree
432        return build_balanced_tree(op, operands);
433    }
434
435    // 7. Non-commutative: just preserve order
436    Expression::Binary {
437        op,
438        left: Box::new(left),
439        right: Box::new(right),
440    }
441}
442
443/// Check for absorption pattern: if `outer` can absorb `inner`.
444/// Returns `Some(outer)` if absorption applies, `None` otherwise.
445fn try_absorb(outer: &Expression, inner: &Expression, inner_op: BinaryOp) -> Option<Expression> {
446    // Check if inner is a binary expression with inner_op containing outer
447    if let Expression::Binary { op, left, right } = inner {
448        if *op == inner_op && (left.as_ref() == outer || right.as_ref() == outer) {
449            return Some(outer.clone());
450        }
451    }
452    None
453}
454
455/// Collect all operands from a chain of the same operator.
456fn collect_chain(op: &BinaryOp, expr: &Expression) -> Vec<Expression> {
457    if let Expression::Binary {
458        op: inner_op,
459        left,
460        right,
461    } = expr
462    {
463        if inner_op == op {
464            let mut result = collect_chain(op, left);
465            result.extend(collect_chain(op, right));
466            return result;
467        }
468    }
469    vec![expr.clone()]
470}
471
472/// Build a balanced binary tree from a list of operands.
473fn build_balanced_tree(op: BinaryOp, mut operands: Vec<Expression>) -> Expression {
474    if operands.is_empty() {
475        // Return identity element
476        return match op {
477            BinaryOp::And => Expression::Literal(serde_json::Value::Bool(true)),
478            BinaryOp::Or => Expression::Literal(serde_json::Value::Bool(false)),
479            BinaryOp::Plus => Expression::Literal(serde_json::Value::Number(0.into())),
480            BinaryOp::Multiply => Expression::Literal(serde_json::Value::Number(1.into())),
481            _ => Expression::Literal(serde_json::Value::Null),
482        };
483    }
484
485    if operands.len() == 1 {
486        return operands.remove(0);
487    }
488
489    // Build left-to-right for determinism (after sorting)
490    let first = operands.remove(0);
491    operands
492        .into_iter()
493        .fold(first, |acc, next| Expression::Binary {
494            op: op.clone(),
495            left: Box::new(acc),
496            right: Box::new(next),
497        })
498}
499
500// ============================================================================
501// Unary Expression Normalization
502// ============================================================================
503
504/// Normalize a unary expression with double negation elimination and De Morgan.
505fn normalize_unary(op: UnaryOp, operand: Expression) -> Expression {
506    match op {
507        UnaryOp::Not => {
508            // Double negation elimination: NOT NOT x → x
509            if let Expression::Unary {
510                op: UnaryOp::Not,
511                operand: inner,
512            } = &operand
513            {
514                return inner.as_ref().clone();
515            }
516
517            // Comparison negation: NOT (a == b) → a != b, NOT (a != b) → a == b
518            if let Expression::Binary {
519                op: inner_op,
520                left,
521                right,
522            } = &operand
523            {
524                let maybe_negated = match inner_op {
525                    BinaryOp::Equal => Some(BinaryOp::NotEqual),
526                    BinaryOp::NotEqual => Some(BinaryOp::Equal),
527                    BinaryOp::GreaterThan => Some(BinaryOp::LessThanOrEqual),
528                    BinaryOp::LessThan => Some(BinaryOp::GreaterThanOrEqual),
529                    BinaryOp::GreaterThanOrEqual => Some(BinaryOp::LessThan),
530                    BinaryOp::LessThanOrEqual => Some(BinaryOp::GreaterThan),
531                    _ => None,
532                };
533                if let Some(negated_op) = maybe_negated {
534                    return Expression::Binary {
535                        op: negated_op,
536                        left: left.clone(),
537                        right: right.clone(),
538                    };
539                }
540            }
541
542            Expression::Unary {
543                op: UnaryOp::Not,
544                operand: Box::new(operand),
545            }
546        }
547        UnaryOp::Negate => Expression::Unary {
548            op: UnaryOp::Negate,
549            operand: Box::new(operand),
550        },
551    }
552}
553
554// ============================================================================
555// Helper Functions
556// ============================================================================
557
558/// Check if an operator is commutative (operand order doesn't matter).
559fn is_commutative(op: &BinaryOp) -> bool {
560    matches!(
561        op,
562        BinaryOp::And
563            | BinaryOp::Or
564            | BinaryOp::Equal
565            | BinaryOp::NotEqual
566            | BinaryOp::Plus
567            | BinaryOp::Multiply
568    )
569}
570
571/// Generate a comparison key for lexicographic sorting of expressions.
572fn expr_cmp_key(expr: &Expression) -> String {
573    // Use canonical serialization for stable comparison
574    canonical_serialize(expr)
575}
576
577/// Recursively serialized expression to a stable string representation
578fn canonical_serialize(expr: &Expression) -> String {
579    use std::fmt::Write;
580    let mut out = String::new();
581
582    match expr {
583        Expression::Literal(v) => write!(out, "Lit({})", v).unwrap(),
584        Expression::Variable(s) => write!(out, "Var({})", s).unwrap(),
585        Expression::QuantityLiteral { value, unit } => {
586            write!(out, "Quant({}, {:?})", value, unit).unwrap()
587        }
588        Expression::TimeLiteral(s) => write!(out, "Time({})", s).unwrap(),
589        Expression::IntervalLiteral { start, end } => {
590            write!(out, "Int({}, {})", start, end).unwrap()
591        }
592        Expression::MemberAccess { object, member } => {
593            write!(out, "Mem({}, {})", object, member).unwrap()
594        }
595        Expression::Binary { op, left, right } => write!(
596            out,
597            "Bin({:?}, {}, {})",
598            op,
599            canonical_serialize(left),
600            canonical_serialize(right)
601        )
602        .unwrap(),
603        Expression::Unary { op, operand } => {
604            write!(out, "Un({:?}, {})", op, canonical_serialize(operand)).unwrap()
605        }
606        Expression::Cast {
607            operand,
608            target_type,
609        } => write!(
610            out,
611            "Cast({}, {:?})",
612            canonical_serialize(operand),
613            target_type
614        )
615        .unwrap(),
616        Expression::Quantifier {
617            quantifier,
618            variable,
619            collection,
620            condition,
621        } => write!(
622            out,
623            "Quant({:?}, {}, {}, {})",
624            quantifier,
625            variable,
626            canonical_serialize(collection),
627            canonical_serialize(condition)
628        )
629        .unwrap(),
630        Expression::GroupBy {
631            variable,
632            collection,
633            filter,
634            key,
635            condition,
636        } => {
637            let f_str = filter
638                .as_ref()
639                .map(|f| canonical_serialize(f))
640                .unwrap_or_else(|| "None".into());
641            write!(
642                out,
643                "Group({}, {}, {}, {}, {})",
644                variable,
645                canonical_serialize(collection),
646                f_str,
647                canonical_serialize(key),
648                canonical_serialize(condition)
649            )
650            .unwrap()
651        }
652        Expression::Aggregation {
653            function,
654            collection,
655            field,
656            filter,
657        } => {
658            let f_str = filter
659                .as_ref()
660                .map(|f| canonical_serialize(f))
661                .unwrap_or_else(|| "None".into());
662            let field_str = field.as_ref().map(|s| s.as_str()).unwrap_or("None");
663            write!(
664                out,
665                "Agg({:?}, {}, {}, {})",
666                function,
667                canonical_serialize(collection),
668                field_str,
669                f_str
670            )
671            .unwrap()
672        }
673        Expression::AggregationComprehension {
674            function,
675            variable,
676            collection,
677            window,
678            predicate,
679            projection,
680            target_unit,
681        } => {
682            let w_str = window
683                .as_ref()
684                .map(|w| format!("{:?}", w))
685                .unwrap_or_else(|| "None".into());
686            let tu_str = target_unit.as_deref().unwrap_or("None");
687            write!(
688                out,
689                "AggComp({:?}, {}, {}, {}, {}, {}, {})",
690                function,
691                variable,
692                canonical_serialize(collection),
693                w_str,
694                canonical_serialize(predicate),
695                canonical_serialize(projection),
696                tu_str
697            )
698            .unwrap()
699        }
700    }
701    out
702}
703
704/// Check if expression is the literal `true`.
705fn is_true_literal(expr: &Expression) -> bool {
706    matches!(expr, Expression::Literal(v) if v.as_bool() == Some(true))
707}
708
709/// Check if expression is the literal `false`.
710fn is_false_literal(expr: &Expression) -> bool {
711    matches!(expr, Expression::Literal(v) if v.as_bool() == Some(false))
712}
713
714// ============================================================================
715// Tests
716// ============================================================================
717
718#[cfg(test)]
719mod tests {
720    use super::*;
721    use crate::policy::Quantifier;
722
723    #[test]
724    fn test_literal_normalization() {
725        let expr = Expression::literal(true);
726        let norm = NormalizedExpression::new(&expr);
727        assert_eq!(norm.to_string(), "true");
728    }
729
730    #[test]
731    fn test_variable_normalization() {
732        let expr = Expression::variable("x");
733        let norm = NormalizedExpression::new(&expr);
734        assert_eq!(norm.to_string(), "x");
735    }
736
737    #[test]
738    fn test_commutative_sorting_and() {
739        // b AND a should normalize to (a AND b)
740        let expr = Expression::binary(
741            BinaryOp::And,
742            Expression::variable("b"),
743            Expression::variable("a"),
744        );
745        let norm = NormalizedExpression::new(&expr);
746        assert_eq!(norm.to_string(), "(a AND b)");
747    }
748
749    #[test]
750    fn test_commutative_sorting_or() {
751        // z OR y should normalize to (y OR z)
752        let expr = Expression::binary(
753            BinaryOp::Or,
754            Expression::variable("z"),
755            Expression::variable("y"),
756        );
757        let norm = NormalizedExpression::new(&expr);
758        assert_eq!(norm.to_string(), "(y OR z)");
759    }
760
761    #[test]
762    fn test_identity_elimination_and_true() {
763        // true AND x → x
764        let expr = Expression::binary(
765            BinaryOp::And,
766            Expression::literal(true),
767            Expression::variable("x"),
768        );
769        let norm = NormalizedExpression::new(&expr);
770        assert_eq!(norm.to_string(), "x");
771    }
772
773    #[test]
774    fn test_identity_elimination_and_true_right() {
775        // x AND true → x
776        let expr = Expression::binary(
777            BinaryOp::And,
778            Expression::variable("x"),
779            Expression::literal(true),
780        );
781        let norm = NormalizedExpression::new(&expr);
782        assert_eq!(norm.to_string(), "x");
783    }
784
785    #[test]
786    fn test_identity_elimination_or_false() {
787        // false OR x → x
788        let expr = Expression::binary(
789            BinaryOp::Or,
790            Expression::literal(false),
791            Expression::variable("x"),
792        );
793        let norm = NormalizedExpression::new(&expr);
794        assert_eq!(norm.to_string(), "x");
795    }
796
797    #[test]
798    fn test_domination_and_false() {
799        // false AND x → false
800        let expr = Expression::binary(
801            BinaryOp::And,
802            Expression::literal(false),
803            Expression::variable("x"),
804        );
805        let norm = NormalizedExpression::new(&expr);
806        assert_eq!(norm.to_string(), "false");
807    }
808
809    #[test]
810    fn test_domination_or_true() {
811        // true OR x → true
812        let expr = Expression::binary(
813            BinaryOp::Or,
814            Expression::literal(true),
815            Expression::variable("x"),
816        );
817        let norm = NormalizedExpression::new(&expr);
818        assert_eq!(norm.to_string(), "true");
819    }
820
821    #[test]
822    fn test_idempotence_and() {
823        // a AND a → a
824        let expr = Expression::binary(
825            BinaryOp::And,
826            Expression::variable("a"),
827            Expression::variable("a"),
828        );
829        let norm = NormalizedExpression::new(&expr);
830        assert_eq!(norm.to_string(), "a");
831    }
832
833    #[test]
834    fn test_idempotence_or() {
835        // a OR a → a
836        let expr = Expression::binary(
837            BinaryOp::Or,
838            Expression::variable("a"),
839            Expression::variable("a"),
840        );
841        let norm = NormalizedExpression::new(&expr);
842        assert_eq!(norm.to_string(), "a");
843    }
844
845    #[test]
846    fn test_absorption_or() {
847        // a OR (a AND b) → a
848        let expr = Expression::binary(
849            BinaryOp::Or,
850            Expression::variable("a"),
851            Expression::binary(
852                BinaryOp::And,
853                Expression::variable("a"),
854                Expression::variable("b"),
855            ),
856        );
857        let norm = NormalizedExpression::new(&expr);
858        assert_eq!(norm.to_string(), "a");
859    }
860
861    #[test]
862    fn test_absorption_and() {
863        // a AND (a OR b) → a
864        let expr = Expression::binary(
865            BinaryOp::And,
866            Expression::variable("a"),
867            Expression::binary(
868                BinaryOp::Or,
869                Expression::variable("a"),
870                Expression::variable("b"),
871            ),
872        );
873        let norm = NormalizedExpression::new(&expr);
874        assert_eq!(norm.to_string(), "a");
875    }
876
877    #[test]
878    fn test_double_negation_elimination() {
879        // NOT NOT x → x
880        let expr = Expression::unary(
881            UnaryOp::Not,
882            Expression::unary(UnaryOp::Not, Expression::variable("x")),
883        );
884        let norm = NormalizedExpression::new(&expr);
885        assert_eq!(norm.to_string(), "x");
886    }
887
888    #[test]
889    fn test_de_morgan_equal() {
890        // NOT (a == b) → a != b
891        let expr = Expression::unary(
892            UnaryOp::Not,
893            Expression::binary(
894                BinaryOp::Equal,
895                Expression::variable("a"),
896                Expression::variable("b"),
897            ),
898        );
899        let norm = NormalizedExpression::new(&expr);
900        assert_eq!(norm.to_string(), "(a != b)");
901    }
902
903    #[test]
904    fn test_de_morgan_not_equal() {
905        // NOT (a != b) → a == b
906        let expr = Expression::unary(
907            UnaryOp::Not,
908            Expression::binary(
909                BinaryOp::NotEqual,
910                Expression::variable("a"),
911                Expression::variable("b"),
912            ),
913        );
914        let norm = NormalizedExpression::new(&expr);
915        assert_eq!(norm.to_string(), "(a == b)");
916    }
917
918    #[test]
919    fn test_de_morgan_greater_than() {
920        // NOT (a > b) → a <= b
921        let expr = Expression::unary(
922            UnaryOp::Not,
923            Expression::binary(
924                BinaryOp::GreaterThan,
925                Expression::variable("a"),
926                Expression::variable("b"),
927            ),
928        );
929        let norm = NormalizedExpression::new(&expr);
930        assert_eq!(norm.to_string(), "(a <= b)");
931    }
932
933    #[test]
934    fn test_chain_flattening_and() {
935        // (a AND b) AND c → (a AND b AND c) sorted
936        let expr = Expression::binary(
937            BinaryOp::And,
938            Expression::binary(
939                BinaryOp::And,
940                Expression::variable("c"),
941                Expression::variable("a"),
942            ),
943            Expression::variable("b"),
944        );
945        let norm = NormalizedExpression::new(&expr);
946        // Should be sorted: a AND b AND c
947        assert_eq!(norm.to_string(), "((a AND b) AND c)");
948    }
949
950    #[test]
951    fn test_chain_deduplication() {
952        // a AND b AND a → a AND b (sorted)
953        let expr = Expression::binary(
954            BinaryOp::And,
955            Expression::binary(
956                BinaryOp::And,
957                Expression::variable("a"),
958                Expression::variable("b"),
959            ),
960            Expression::variable("a"),
961        );
962        let norm = NormalizedExpression::new(&expr);
963        assert_eq!(norm.to_string(), "(a AND b)");
964    }
965
966    #[test]
967    fn test_equivalence_commutative() {
968        let a_and_b = Expression::binary(
969            BinaryOp::And,
970            Expression::variable("a"),
971            Expression::variable("b"),
972        );
973        let b_and_a = Expression::binary(
974            BinaryOp::And,
975            Expression::variable("b"),
976            Expression::variable("a"),
977        );
978        let norm1 = NormalizedExpression::new(&a_and_b);
979        let norm2 = NormalizedExpression::new(&b_and_a);
980        assert_eq!(norm1, norm2);
981    }
982
983    #[test]
984    fn test_stable_hash_deterministic() {
985        let expr = Expression::binary(
986            BinaryOp::Or,
987            Expression::variable("x"),
988            Expression::literal(false),
989        );
990        let h1 = NormalizedExpression::new(&expr).stable_hash();
991        let h2 = NormalizedExpression::new(&expr).stable_hash();
992        assert_eq!(h1, h2);
993    }
994
995    #[test]
996    fn test_nested_normalization() {
997        // (true AND (b OR a)) → (a OR b)
998        let nested = Expression::binary(
999            BinaryOp::And,
1000            Expression::literal(true),
1001            Expression::binary(
1002                BinaryOp::Or,
1003                Expression::variable("b"),
1004                Expression::variable("a"),
1005            ),
1006        );
1007        let norm = NormalizedExpression::new(&nested);
1008        assert_eq!(norm.to_string(), "(a OR b)");
1009    }
1010
1011    #[test]
1012    fn test_quantifier_normalization() {
1013        let expr = Expression::quantifier(
1014            Quantifier::ForAll,
1015            "x",
1016            Expression::variable("items"),
1017            Expression::binary(
1018                BinaryOp::And,
1019                Expression::literal(true),
1020                Expression::variable("valid"),
1021            ),
1022        );
1023        let norm = NormalizedExpression::new(&expr);
1024        // Condition should be simplified: true AND valid → valid
1025        assert!(norm.to_string().contains("valid"));
1026        assert!(!norm.to_string().contains("true"));
1027    }
1028}