Function to_cnf 

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

Convert an expression to Conjunctive Normal Form (CNF).

CNF is a conjunction of disjunctions: (A ∨ B ∨ C) ∧ (D ∨ E) ∧ ...

Warning: CNF 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::or(TLExpr::and(a, b), c);
let cnf = tensorlogic_ir::to_cnf(&expr);
// Result: AND(OR(A, C), OR(B, C))