Function nnf

pub fn nnf(expr: ExprRef) -> ExprRef

Return an equivalent expression in Negative Normal Form (NNF).

In NNF, crate::NotExpr expressions may only contain terminal nodes such as Literal or GetItem. They may not contain crate::BinaryExpr, crate::NotExpr, etc.

Examples

Double negation is removed entirely:

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

let double_negation = not(not(col("a")));
let nnfed = nnf(double_negation);
assert_eq!(&nnfed, &col("a"));

Triple negation becomes single negation:

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

let triple_negation = not(not(not(col("a"))));
let nnfed = nnf(triple_negation);
assert_eq!(&nnfed, &not(col("a")));

Negation at a high-level is pushed to the leaves, likely increasing the total number nodes:

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

assert_eq!(
    &nnf(not(and(col("a"), col("b")))),
    &or(not(col("a")), not(col("b")))
);

In Vortex, NNF is extended beyond simple Boolean operators to any Boolean-valued operator:

use vortex_expr::{not, col, and, or, lt, lit, gt_eq};
use vortex_expr::forms::nnf::nnf;

assert_eq!(
    &nnf(not(and(gt_eq(col("a"), lit(3)), col("b")))),
    &or(lt(col("a"), lit(3)), not(col("b")))
);