vortex_expr/forms/
nnf.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
use vortex_error::VortexResult;

use crate::traversal::{FoldChildren, FoldDown, FoldUp, Folder, Node as _};
use crate::{not, BinaryExpr, ExprRef, Not, Operator};

/// Return an equivalent expression in Negative Normal Form (NNF).
///
/// In NNF, [Not] expressions may only contain terminal nodes such as [Literal](crate::Literal) or
/// [Column](crate::Column). 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")))
/// );
/// ```
pub fn nnf(expr: ExprRef) -> VortexResult<ExprRef> {
    let mut visitor = NNFVisitor::default();
    Ok(expr.transform_with_context(&mut visitor, false)?.result())
}

#[derive(Default)]
struct NNFVisitor {}

impl Folder for NNFVisitor {
    type NodeTy = ExprRef;
    type Out = ExprRef;
    type Context = bool;

    fn visit_down(
        &mut self,
        node: &ExprRef,
        negating: bool,
    ) -> VortexResult<FoldDown<ExprRef, bool>> {
        let node_any = node.as_any();
        if node_any.downcast_ref::<Not>().is_some() {
            return Ok(FoldDown::Continue(!negating));
        } else if let Some(binary_expr) = node_any.downcast_ref::<BinaryExpr>() {
            match binary_expr.op() {
                Operator::And | Operator::Or => {
                    return Ok(FoldDown::Continue(negating));
                }
                _ => {}
            }
        }

        Ok(FoldDown::SkipChildren)
    }

    fn visit_up(
        &mut self,
        node: ExprRef,
        negating: bool,
        new_children: FoldChildren<ExprRef>,
    ) -> VortexResult<FoldUp<ExprRef>> {
        let node_any = node.as_any();
        let new_node = if node_any.downcast_ref::<Not>().is_some() {
            let FoldChildren::Children(mut new_children) = new_children else {
                unreachable!();
            };
            debug_assert_eq!(new_children.len(), 1);

            new_children.remove(0)
        } else if let Some(binary_expr) = node_any.downcast_ref::<BinaryExpr>() {
            if !negating {
                node
            } else {
                let new_op = match binary_expr.op() {
                    Operator::Eq => Operator::NotEq,
                    Operator::NotEq => Operator::Eq,
                    Operator::Gt => Operator::Lte,
                    Operator::Gte => Operator::Lt,
                    Operator::Lt => Operator::Gte,
                    Operator::Lte => Operator::Gt,
                    Operator::And => Operator::Or,
                    Operator::Or => Operator::And,
                };
                let (lhs, rhs) = match binary_expr.op() {
                    Operator::Or | Operator::And => {
                        let FoldChildren::Children(mut negated_children) = new_children else {
                            unreachable!();
                        };
                        debug_assert_eq!(negated_children.len(), 2);
                        let rhs = negated_children.remove(1);
                        let lhs = negated_children.remove(0);
                        (lhs, rhs)
                    }
                    _ => {
                        let FoldChildren::Skipped = new_children else {
                            unreachable!();
                        };
                        (binary_expr.lhs().clone(), binary_expr.rhs().clone())
                    }
                };
                BinaryExpr::new_expr(lhs, new_op, rhs)
            }
        } else {
            let FoldChildren::Skipped = new_children else {
                unreachable!();
            };

            if negating {
                not(node)
            } else {
                node
            }
        };
        Ok(FoldUp::Continue(new_node))
    }
}