vortex_expr/forms/
nnf.rs

1use vortex_error::{VortexExpect, VortexResult};
2
3use crate::traversal::{FoldDown, FoldUp, FolderMut, Node as _};
4use crate::{BinaryExpr, ExprRef, Not, Operator, not};
5
6/// Return an equivalent expression in Negative Normal Form (NNF).
7///
8/// In NNF, [Not] expressions may only contain terminal nodes such as [Literal](crate::Literal) or
9/// [GetItem](crate::GetItem). They *may not* contain [BinaryExpr], [Not], etc.
10///
11/// # Examples
12///
13/// Double negation is removed entirely:
14///
15/// ```
16/// use vortex_expr::{not, col};
17/// use vortex_expr::forms::nnf::nnf;
18///
19/// let double_negation = not(not(col("a")));
20/// let nnfed = nnf(double_negation);
21/// assert_eq!(&nnfed, &col("a"));
22/// ```
23///
24/// Triple negation becomes single negation:
25///
26/// ```
27/// use vortex_expr::{not, col};
28/// use vortex_expr::forms::nnf::nnf;
29///
30/// let triple_negation = not(not(not(col("a"))));
31/// let nnfed = nnf(triple_negation);
32/// assert_eq!(&nnfed, &not(col("a")));
33/// ```
34///
35/// Negation at a high-level is pushed to the leaves, likely increasing the total number nodes:
36///
37/// ```
38/// use vortex_expr::{not, col, and, or};
39/// use vortex_expr::forms::nnf::nnf;
40///
41/// assert_eq!(
42///     &nnf(not(and(col("a"), col("b")))),
43///     &or(not(col("a")), not(col("b")))
44/// );
45/// ```
46///
47/// In Vortex, NNF is extended beyond simple Boolean operators to any Boolean-valued operator:
48///
49/// ```
50/// use vortex_expr::{not, col, and, or, lt, lit, gt_eq};
51/// use vortex_expr::forms::nnf::nnf;
52///
53/// assert_eq!(
54///     &nnf(not(and(gt_eq(col("a"), lit(3)), col("b")))),
55///     &or(lt(col("a"), lit(3)), not(col("b")))
56/// );
57/// ```
58pub fn nnf(expr: ExprRef) -> ExprRef {
59    let mut visitor = NNFVisitor::default();
60
61    expr.transform_with_context(&mut visitor, false)
62        .vortex_expect("cannot fail")
63        .result()
64}
65
66#[derive(Default)]
67struct NNFVisitor {}
68
69impl FolderMut for NNFVisitor {
70    type NodeTy = ExprRef;
71    type Out = ExprRef;
72    type Context = bool;
73
74    fn visit_down(
75        &mut self,
76        node: &ExprRef,
77        negating: bool,
78    ) -> VortexResult<FoldDown<ExprRef, bool>> {
79        let node_any = node.as_any();
80        if node_any.is::<Not>() {
81            return Ok(FoldDown::Continue(!negating));
82        } else if let Some(binary_expr) = node_any.downcast_ref::<BinaryExpr>() {
83            match binary_expr.op() {
84                Operator::And | Operator::Or => {
85                    return Ok(FoldDown::Continue(negating));
86                }
87                _ => {}
88            }
89        }
90
91        Ok(FoldDown::Continue(negating))
92    }
93
94    fn visit_up(
95        &mut self,
96        node: ExprRef,
97        negating: bool,
98        mut new_children: Vec<ExprRef>,
99    ) -> VortexResult<FoldUp<ExprRef>> {
100        let node_any = node.as_any();
101
102        let new_node = if node_any.is::<Not>() {
103            debug_assert_eq!(new_children.len(), 1);
104            new_children.remove(0)
105        } else if let Some(binary_expr) = node_any.downcast_ref::<BinaryExpr>() {
106            if !negating {
107                node
108            } else {
109                let new_op = match binary_expr.op() {
110                    Operator::Eq => Operator::NotEq,
111                    Operator::NotEq => Operator::Eq,
112                    Operator::Gt => Operator::Lte,
113                    Operator::Gte => Operator::Lt,
114                    Operator::Lt => Operator::Gte,
115                    Operator::Lte => Operator::Gt,
116                    Operator::And => Operator::Or,
117                    Operator::Or => Operator::And,
118                };
119                let (lhs, rhs) = match binary_expr.op() {
120                    Operator::Or | Operator::And => {
121                        let mut negated_children = new_children;
122                        debug_assert_eq!(negated_children.len(), 2);
123                        let rhs = negated_children.remove(1);
124                        let lhs = negated_children.remove(0);
125                        (lhs, rhs)
126                    }
127                    _ => (binary_expr.lhs().clone(), binary_expr.rhs().clone()),
128                };
129                BinaryExpr::new_expr(lhs, new_op, rhs)
130            }
131        } else if negating {
132            not(node)
133        } else {
134            node
135        };
136
137        Ok(FoldUp::Continue(new_node))
138    }
139}
vortex_expr/forms/nnf.rs

vortex_expr/forms/
nnf.rs
