Function cnf

pub fn cnf(expr: ExprRef) -> Vec<ExprRef> 

Return an equivalent expression in Conjunctive Normal Form (CNF).

A CNF expression is a vector of vectors. The outer vector is a conjunction. The inner vectors are disjunctions. Neither Operator::And nor Operator::Or may appear in the disjunctions. Moreover, each disjunction in a CNF expression must be in Negative Normal Form.

Examples

All the NNF examples also apply to CNF, for example double negation is removed entirely:

use vortex_expr::{not, col};
use vortex_expr::forms::cnf::cnf;

let double_negation = not(not(col("a")));
let cnfed = cnf(double_negation);
assert_eq!(cnfed, vec![col("a")]);

Unlike NNF, CNF, lifts conjunctions to the top-level and distributions disjunctions such that there is at most one disjunction for each conjunction operand:

use vortex_expr::{not, col, or, and};
use vortex_expr::forms::cnf::cnf;

assert_eq!(
    cnf(
        or(
            and(col("a"), col("b")),
            col("c"),
        )
    ),
    vec![
        or(col("a"), col("c")),
        or(col("b"), col("c")),
    ]
);