16370663357

Committed 18 Jul 2025 12:34PM UTC coverage: 81.524% (+0.5%) from 81.031%

Build # 16370663357

Build Type

Pull #3912

github

Committed by

web-flow

Commit Message

Merge 7e052bc6b into eda1774d5

Pull Request Pull Request #3912: fix: unpack and propagate error

Run Details

14 of 16 new or added lines in 2 files covered. (87.5%)

45 existing lines in 4 files now uncovered.

42027 of 51552 relevant lines covered (81.52%)

169751.82 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

88.57

/vortex-expr/src/forms/nnf.rs

// SPDX-License-Identifier: Apache-2.0
// SPDX-FileCopyrightText: Copyright the Vortex contributors

use vortex_error::{VortexExpect, VortexResult, vortex_bail};

use crate::traversal::{FoldDown, FoldUp, FolderMut, Node as _, NodeVisitor, TraversalOrder};
use crate::{
    BinaryExpr, BinaryVTable, ExprRef, GetItemVTable, IntoExpr, LiteralVTable, NotVTable, Operator,
    not,
};

/// Return an equivalent expression in Negative Normal Form ([NNF](https://en.wikipedia.org/wiki/Negation_normal_form)).
///
/// In NNF, [crate::NotExpr] expressions may only contain terminal nodes such as [Literal](crate::LiteralExpr) or
/// [GetItem](crate::GetItemExpr). 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")))
/// );
/// ```
pub fn nnf(expr: ExprRef) -> ExprRef {
    let mut visitor = NNFVisitor::default();

    expr.transform_with_context(&mut visitor, false)
        .vortex_expect("cannot fail")
        .result()
}

/// Verifies whether the expression is in Negative Normal Form ([NNF](https://en.wikipedia.org/wiki/Negation_normal_form)).
///
/// Note that NNF isn't canonical, different expressions might be logically equivalent but different.
pub fn is_nnf(expr: &ExprRef) -> bool {
    let mut visitor = NNFValidationVisitor::default();
    expr.accept(&mut visitor).vortex_expect("never fails");
    visitor.is_nnf
}

#[derive(Default)]
struct NNFVisitor {}

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

    fn visit_down(
        &mut self,
        node: &ExprRef,
        negating: bool,
    ) -> VortexResult<FoldDown<ExprRef, bool>> {
        if node.is::<NotVTable>() {
            return Ok(FoldDown::Continue(!negating));
        }

        Ok(FoldDown::Continue(negating))
    }

    fn visit_up(
        &mut self,
        node: ExprRef,
        negating: bool,
        mut new_children: Vec<ExprRef>,
    ) -> VortexResult<FoldUp<ExprRef>> {
        let new_node = if node.is::<NotVTable>() {
            debug_assert_eq!(new_children.len(), 1);
            new_children.remove(0)
        } else if let Some(binary_expr) = node.as_opt::<BinaryVTable>() {
            if !negating {
                node.with_children(new_children)?
            } 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,
                    Operator::Add => {
                        vortex_bail!("nnf: type mismatch: cannot negate addition")
                    }
                };
                let (lhs, rhs) = match binary_expr.op() {
                    Operator::Or | Operator::And => {
                        let mut negated_children = new_children;
                        debug_assert_eq!(negated_children.len(), 2);
                        let rhs = negated_children.remove(1);
                        let lhs = negated_children.remove(0);
                        (lhs, rhs)
                    }
                    _ => (binary_expr.lhs().clone(), binary_expr.rhs().clone()),
                };
                BinaryExpr::new(lhs, new_op, rhs).into_expr()
            }
        } else if negating {
            not(node)
        } else {
            node
        };

        Ok(FoldUp::Continue(new_node))
    }
}

struct NNFValidationVisitor {
    is_nnf: bool,
}

impl Default for NNFValidationVisitor {
    fn default() -> Self {
        Self { is_nnf: true }
    }
}

impl<'a> NodeVisitor<'a> for NNFValidationVisitor {
    type NodeTy = ExprRef;

    fn visit_down(&mut self, node: &'a Self::NodeTy) -> VortexResult<TraversalOrder> {
        if let Some(not_expr) = node.as_opt::<NotVTable>() {
            let is_var =
                not_expr.child().is::<GetItemVTable>() || not_expr.child().is::<LiteralVTable>();
            self.is_nnf &= is_var;
            if !is_var {
                return Ok(TraversalOrder::Stop);
            }
        }

        Ok(TraversalOrder::Continue)
    }
}

#[cfg(test)]
mod tests {
    use rstest::rstest;

    use super::*;
    use crate::{and, col, gt_eq, lit, lt, or};

    #[rstest]
    #[case(
        and(not(and(lit(true), lit(true))), and(lit(true), lit(true))),
        and(or(not(lit(true)), not(lit(true))), and(lit(true), lit(true)),)
    )]
    #[case(not(not(col("a"))), col("a"))]
    #[case(not(not(not(col("a")))), not(col("a")))]
    #[case(not(and(col("a"), col("b"))), or(not(col("a")), not(col("b"))))]
    #[case(
        not(and(gt_eq(col("a"), lit(3)), col("b"))),
        or(lt(col("a"), lit(3)), not(col("b")))
    )]
    fn basic_nnf_test(#[case] input: ExprRef, #[case] expected: ExprRef) {
        let output = nnf(input.clone());

        assert_eq!(
            &output, &expected,
            "\nOriginal expr: {input}]\nRewritten expr: {output}\nexpected expr:{expected}"
        );
        assert!(is_nnf(&output));
    }
}

1	// SPDX-License-Identifier: Apache-2.0
2	// SPDX-FileCopyrightText: Copyright the Vortex contributors
3
4	use vortex_error::{VortexExpect, VortexResult, vortex_bail};
5
6	use crate::traversal::{FoldDown, FoldUp, FolderMut, Node as _, NodeVisitor, TraversalOrder};
7	use crate::{
8	BinaryExpr, BinaryVTable, ExprRef, GetItemVTable, IntoExpr, LiteralVTable, NotVTable, Operator,
9	not,
10	};
11
12	/// Return an equivalent expression in Negative Normal Form ([NNF](https://en.wikipedia.org/wiki/Negation_normal_form)).
13	///
14	/// In NNF, [crate::NotExpr] expressions may only contain terminal nodes such as [Literal](crate::LiteralExpr) or
15	/// [GetItem](crate::GetItemExpr). They may not contain [crate::BinaryExpr], [crate::NotExpr], etc.
16	///
17	/// # Examples
18	///
19	/// Double negation is removed entirely:
20	///
21	/// ```
22	/// use vortex_expr::{not, col};
23	/// use vortex_expr::forms::nnf::nnf;
24	///
25	/// let double_negation = not(not(col("a")));
26	/// let nnfed = nnf(double_negation);
27	/// assert_eq!(&nnfed, &col("a"));
28	/// ```
29	///
30	/// Triple negation becomes single negation:
31	///
32	/// ```
33	/// use vortex_expr::{not, col};
34	/// use vortex_expr::forms::nnf::nnf;
35	///
36	/// let triple_negation = not(not(not(col("a"))));
37	/// let nnfed = nnf(triple_negation);
38	/// assert_eq!(&nnfed, &not(col("a")));
39	/// ```
40	///
41	/// Negation at a high-level is pushed to the leaves, likely increasing the total number nodes:
42	///
43	/// ```
44	/// use vortex_expr::{not, col, and, or};
45	/// use vortex_expr::forms::nnf::nnf;
46	///
47	/// assert_eq!(
48	/// &nnf(not(and(col("a"), col("b")))),
49	/// &or(not(col("a")), not(col("b")))
50	/// );
51	/// ```
52	///
53	/// In Vortex, NNF is extended beyond simple Boolean operators to any Boolean-valued operator:
54	///
55	/// ```
56	/// use vortex_expr::{not, col, and, or, lt, lit, gt_eq};
57	/// use vortex_expr::forms::nnf::nnf;
58	///
59	/// assert_eq!(
60	/// &nnf(not(and(gt_eq(col("a"), lit(3)), col("b")))),
61	/// &or(lt(col("a"), lit(3)), not(col("b")))
62	/// );
63	/// ```
64	pub fn nnf(expr: ExprRef) -> ExprRef {	33,013✔
65	let mut visitor = NNFVisitor::default();	33,013✔
66
67	expr.transform_with_context(&mut visitor, false)	33,013✔
68	.vortex_expect("cannot fail")	33,013✔
69	.result()	33,013✔
70	}	33,013✔
71
72	/// Verifies whether the expression is in Negative Normal Form ([NNF](https://en.wikipedia.org/wiki/Negation_normal_form)).
73	///
74	/// Note that NNF isn't canonical, different expressions might be logically equivalent but different.
75	pub fn is_nnf(expr: &ExprRef) -> bool {	5✔
76	let mut visitor = NNFValidationVisitor::default();	5✔
77	expr.accept(&mut visitor).vortex_expect("never fails");	5✔
78	visitor.is_nnf	5✔
79	}	5✔
80
81	#[derive(Default)]
82	struct NNFVisitor {}
83
84	impl FolderMut for NNFVisitor {
85	type NodeTy = ExprRef;
86	type Out = ExprRef;
87	type Context = bool;
88
89	fn visit_down(	149,422✔
90	&mut self,	149,422✔
91	node: &ExprRef,	149,422✔
92	negating: bool,	149,422✔
93	) -> VortexResult<FoldDown<ExprRef, bool>> {	149,422✔
94	if node.is::<NotVTable>() {	149,422✔
95	return Ok(FoldDown::Continue(!negating));	8✔
96	}	149,414✔
97
98	Ok(FoldDown::Continue(negating))	149,414✔
99	}	149,422✔
100
101	fn visit_up(	149,422✔
102	&mut self,	149,422✔
103	node: ExprRef,	149,422✔
104	negating: bool,	149,422✔
105	mut new_children: Vec<ExprRef>,	149,422✔
106	) -> VortexResult<FoldUp<ExprRef>> {	149,422✔
107	let new_node = if node.is::<NotVTable>() {	149,422✔
108	debug_assert_eq!(new_children.len(), 1);	8✔
109	new_children.remove(0)	8✔
110	} else if let Some(binary_expr) = node.as_opt::<BinaryVTable>() {	149,414✔
111	if !negating {	12,054✔
112	node.with_children(new_children)?	12,050✔
113	} else {
114	let new_op = match binary_expr.op() {	4✔
UNCOV 115	Operator::Eq => Operator::NotEq,	×
UNCOV 116	Operator::NotEq => Operator::Eq,	×
UNCOV 117	Operator::Gt => Operator::Lte,	×
118	Operator::Gte => Operator::Lt,	1✔
UNCOV 119	Operator::Lt => Operator::Gte,	×
UNCOV 120	Operator::Lte => Operator::Gt,	×
121	Operator::And => Operator::Or,	3✔
UNCOV 122	Operator::Or => Operator::And,	×
123	Operator::Add => {
UNCOV 124	vortex_bail!("nnf: type mismatch: cannot negate addition")	×
125	}
126	};
127	let (lhs, rhs) = match binary_expr.op() {	4✔
128	Operator::Or \| Operator::And => {
129	let mut negated_children = new_children;	3✔
130	debug_assert_eq!(negated_children.len(), 2);	3✔
131	let rhs = negated_children.remove(1);	3✔
132	let lhs = negated_children.remove(0);	3✔
133	(lhs, rhs)	3✔
134	}
135	_ => (binary_expr.lhs().clone(), binary_expr.rhs().clone()),	1✔
136	};
137	BinaryExpr::new(lhs, new_op, rhs).into_expr()	4✔
138	}
139	} else if negating {	137,360✔
140	not(node)	13✔
141	} else {
142	node	137,347✔
143	};
144
145	Ok(FoldUp::Continue(new_node))	149,422✔
146	}	149,422✔
147	}
148
149	struct NNFValidationVisitor {
150	is_nnf: bool,
151	}
152
153	impl Default for NNFValidationVisitor {
154	fn default() -> Self {	5✔
155	Self { is_nnf: true }	5✔
156	}	5✔
157	}
158
159	impl<'a> NodeVisitor<'a> for NNFValidationVisitor {
160	type NodeTy = ExprRef;
161
162	fn visit_down(&mut self, node: &'a Self::NodeTy) -> VortexResult<TraversalOrder> {	29✔
163	if let Some(not_expr) = node.as_opt::<NotVTable>() {	29✔
164	let is_var =	6✔
165	not_expr.child().is::<GetItemVTable>() \|\| not_expr.child().is::<LiteralVTable>();	6✔
166	self.is_nnf &= is_var;	6✔
167	if !is_var {	6✔
UNCOV 168	return Ok(TraversalOrder::Stop);	×
169	}	6✔
170	}	23✔
171
172	Ok(TraversalOrder::Continue)	29✔
173	}	29✔
174	}
175
176	#[cfg(test)]
177	mod tests {
178	use rstest::rstest;
179
180	use super::*;
181	use crate::{and, col, gt_eq, lit, lt, or};
182
183	#[rstest]
184	#[case(
185	and(not(and(lit(true), lit(true))), and(lit(true), lit(true))),
186	and(or(not(lit(true)), not(lit(true))), and(lit(true), lit(true)),)
187	)]
188	#[case(not(not(col("a"))), col("a"))]
189	#[case(not(not(not(col("a")))), not(col("a")))]
190	#[case(not(and(col("a"), col("b"))), or(not(col("a")), not(col("b"))))]
191	#[case(
192	not(and(gt_eq(col("a"), lit(3)), col("b"))),
193	or(lt(col("a"), lit(3)), not(col("b")))
194	)]
195	fn basic_nnf_test(#[case] input: ExprRef, #[case] expected: ExprRef) {
196	let output = nnf(input.clone());
197
198	assert_eq!(
199	&output, &expected,
200	"\nOriginal expr: {input}]\nRewritten expr: {output}\nexpected expr:{expected}"
201	);
202	assert!(is_nnf(&output));
203	}
204	}

vortex-data / vortex / 16370663357

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous