Function cnf

pub fn cnf(expr: ExprRef) -> VortexResult<Vec<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).unwrap();
assert_eq!(cnfed, vec![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(
            or(
                and(col("a"), col("b")),
                col("c")
            ),
            col("d")
        )
    ).unwrap(),
    vec![
        vec![col("a"), col("c"), col("d")],
        vec![col("b"), col("c"), col("d")]
    ]
);

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

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

Vortex extends the CNF definition to any Boolean-valued expression, even ones with non-Boolean parameters:

use vortex_expr::{not, col, or, and, gt_eq, lit, not_eq, lt, eq};
use vortex_expr::forms::cnf::cnf;
use itertools::Itertools;

assert_eq!(
    cnf(
        or(
            and(
                gt_eq(col("earnings"), lit(50_000)),
                not_eq(col("role"), lit("Manager"))
            ),
            col("special_flag")
        ),
    ).unwrap(),
    vec![
        vec![
            gt_eq(col("earnings"), lit(50_000)),
            col("special_flag")
        ],
        vec![
            not_eq(col("role"), lit("Manager")),
            col("special_flag")
        ]
    ]
);

use vortex_expr::{not, col, or, and, gt_eq, lit, not_eq, lt, eq};
use vortex_expr::forms::cnf::cnf;
use itertools::Itertools;

assert_eq!(
    cnf(
        or(
            or(
                and(
                    gt_eq(col("earnings"), lit(50_000)),
                    not_eq(col("role"), lit("Manager"))
                ),
                col("special_flag")
            ),
            and(
                lt(col("tenure"), lit(5)),
                eq(col("role"), lit("Engineer"))
            ),
        )
    ).unwrap(),
    vec![
        vec![
            gt_eq(col("earnings"), lit(50_000)),
            col("special_flag"),
            lt(col("tenure"), lit(5)),
        ],
        vec![
            gt_eq(col("earnings"), lit(50_000)),
            col("special_flag"),
            eq(col("role"), lit("Engineer")),
        ],
        vec![
            not_eq(col("role"), lit("Manager")),
            col("special_flag"),
            lt(col("tenure"), lit(5)),
        ],
        vec![
            not_eq(col("role"), lit("Manager")),
            col("special_flag"),
            eq(col("role"), lit("Engineer")),
        ],
    ]
);