Function nnf

pub fn nnf(expr: ExprRef) -> VortexResult<ExprRef>

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

In NNF, Not expressions may only contain terminal nodes such as Literal or GetItem. They may not contain BinaryExpr, Not, 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).unwrap();
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).unwrap();
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")))).unwrap(),
    &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")))).unwrap(),
    &or(lt(col("a"), lit(3)), not(col("b")))
);