Function to_dnf 

pub fn to_dnf(expr: &TLExpr) -> TLExpr

Convert an expression to Disjunctive Normal Form (DNF).

DNF is a disjunction of conjunctions: (A ∧ B ∧ C) ∨ (D ∧ E) ∨ ...

Warning: DNF conversion can lead to exponential blowup in expression size. For expressions with many nested operators, consider limiting the depth or using approximation techniques.

Examples

use tensorlogic_ir::{TLExpr, Term};

// (A ∨ B) ∧ C becomes (A ∧ C) ∨ (B ∧ C)
let a = TLExpr::pred("A", vec![]);
let b = TLExpr::pred("B", vec![]);
let c = TLExpr::pred("C", vec![]);
let expr = TLExpr::and(TLExpr::or(a, b), c);
let dnf = tensorlogic_ir::to_dnf(&expr);
// Result: OR(AND(A, C), AND(B, C))