16835424474

Committed 08 Aug 2025 04:27PM UTC coverage: 84.938% (+0.003%) from 84.935%

Build # 16835424474

Build Type

Pull #4174

github

Committed by

web-flow

Commit Message

Merge 28736a3aa into a16b0e365

Pull Request Pull Request #4174: fix[scan]: don't convert filter to `cnf` just extract `and` list

Run Details

19 of 20 new or added lines in 3 files covered. (95.0%)

3 existing lines in 3 files now uncovered.

50674 of 59660 relevant lines covered (84.94%)

567699.25 hits per line

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

98.88

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

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

use itertools::Itertools;
use vortex_error::{VortexExpect, VortexResult};

use super::nnf::nnf;
use crate::traversal::{Node as _, NodeVisitor, TraversalOrder};
use crate::{BinaryVTable, ExprRef, Operator, lit, or};

/// Return an equivalent expression in Conjunctive Normal Form (CNF).
///
/// A CNF expression is a vector of vectors. The outer vector is a conjunction. The inner vectors
/// are disjunctions. Neither [Operator::And] nor [Operator::Or] may appear in the
/// disjunctions. Moreover, each disjunction in a CNF expression must be in Negative Normal Form.
///
/// # Examples
///
/// All the NNF examples also apply to CNF, for example double negation is removed entirely:
///
/// ```
/// use vortex_expr::{not, col};
/// use vortex_expr::forms::cnf::cnf;
///
/// let double_negation = not(not(col("a")));
/// let cnfed = cnf(double_negation);
/// assert_eq!(cnfed, vec![col("a")]);
/// ```
///
/// Unlike NNF, CNF, lifts conjunctions to the top-level and distributions disjunctions such that
/// there is at most one disjunction for each conjunction operand:
///
///
/// ```rust
/// use vortex_expr::{not, col, or, and};
/// use vortex_expr::forms::cnf::cnf;
///
/// assert_eq!(
///     cnf(
///         or(
///             and(col("a"), col("b")),
///             col("c"),
///         )
///     ),
///     vec![
///         or(col("a"), col("c")),
///         or(col("b"), col("c")),
///     ]
/// );
/// ```
///
pub fn cnf(expr: ExprRef) -> Vec<ExprRef> {
    if expr == lit(true) {
        // True in CNF
        return vec![];
    }
    let nnf = nnf(expr);

    let mut visitor = CNFVisitor::default();
    nnf.accept(&mut visitor).vortex_expect("cannot fail");
    visitor
        .finish()
        .into_iter()
        .filter_map(|disjunction| disjunction.into_iter().reduce(or))
        .collect_vec()
}

#[derive(Default)]
struct CNFVisitor {
    conjuncts_of_disjuncts: Vec<Vec<ExprRef>>,
}

impl CNFVisitor {
    fn finish(self) -> Vec<Vec<ExprRef>> {
        self.conjuncts_of_disjuncts
    }
}

impl NodeVisitor<'_> for CNFVisitor {
    type NodeTy = ExprRef;

    fn visit_down(&mut self, node: &ExprRef) -> VortexResult<TraversalOrder> {
        if let Some(binary_expr) = node.as_opt::<BinaryVTable>() {
            match binary_expr.op() {
                Operator::And => return Ok(TraversalOrder::Continue),
                Operator::Or => {
                    let mut visitor = CNFVisitor::default();
                    binary_expr.lhs().accept(&mut visitor)?;
                    let lhs_conjuncts = visitor.finish();

                    let mut visitor = CNFVisitor::default();
                    binary_expr.rhs().accept(&mut visitor)?;
                    let rhs_conjuncts = visitor.finish();

                    self.conjuncts_of_disjuncts
                        .extend(lhs_conjuncts.iter().flat_map(|lhs_disjunct| {
                            rhs_conjuncts.iter().map(|rhs_disjunct| {
                                let mut lhs_copy = lhs_disjunct.clone();
                                lhs_copy.extend(rhs_disjunct.iter().cloned());
                                lhs_copy
                            })
                        }));

                    return Ok(TraversalOrder::Skip);
                }
                _ => {}
            }
        }
        // Anything other than And and Or are terminals from the perspective of CNF
        self.conjuncts_of_disjuncts.push(vec![node.clone()]);
        Ok(TraversalOrder::Skip)
    }
}

#[cfg(test)]
mod tests {

    use vortex_expr::forms::cnf::cnf;
    use vortex_expr::{and, col, eq, gt_eq, lit, lt, not_eq, or};

    #[test]
    fn test_cnf_simple() {
        assert_eq!(
            cnf(or(or(and(col("a"), col("b")), col("c")), col("d"))),
            vec![
                or(or(col("a"), col("c")), col("d")),
                or(or(col("b"), col("c")), col("d"))
            ]
        );
    }

    #[test]
    fn test_with_lit() {
        assert_eq!(
            cnf(or(
                and(
                    gt_eq(col("earnings"), lit(50_000)),
                    not_eq(col("role"), lit("Manager"))
                ),
                col("special_flag")
            ),),
            vec![
                or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),
                or(not_eq(col("role"), lit("Manager")), col("special_flag"))
            ]
        );
    }

    #[test]
    fn test_cnf() {
        assert_eq!(
            cnf(or(
                or(
                    and(
                        gt_eq(col("earnings"), lit(50_000)),
                        not_eq(col("role"), lit("Manager"))
                    ),
                    col("special_flag")
                ),
                and(lt(col("tenure"), lit(5)), eq(col("role"), lit("Engineer"))),
            )),
            vec![
                or(
                    or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),
                    lt(col("tenure"), lit(5))
                ),
                or(
                    or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),
                    eq(col("role"), lit("Engineer"))
                ),
                or(
                    or(not_eq(col("role"), lit("Manager")), col("special_flag")),
                    lt(col("tenure"), lit(5))
                ),
                or(
                    or(not_eq(col("role"), lit("Manager")), col("special_flag")),
                    eq(col("role"), lit("Engineer"))
                )
            ]
        );
    }
}

1	// SPDX-License-Identifier: Apache-2.0
2	// SPDX-FileCopyrightText: Copyright the Vortex contributors
3
4	use itertools::Itertools;
5	use vortex_error::{VortexExpect, VortexResult};
6
7	use super::nnf::nnf;
8	use crate::traversal::{Node as _, NodeVisitor, TraversalOrder};
9	use crate::{BinaryVTable, ExprRef, Operator, lit, or};
10
11	/// Return an equivalent expression in Conjunctive Normal Form (CNF).
12	///
13	/// A CNF expression is a vector of vectors. The outer vector is a conjunction. The inner vectors
14	/// are disjunctions. Neither [Operator::And] nor [Operator::Or] may appear in the
15	/// disjunctions. Moreover, each disjunction in a CNF expression must be in Negative Normal Form.
16	///
17	/// # Examples
18	///
19	/// All the NNF examples also apply to CNF, for example double negation is removed entirely:
20	///
21	/// ```
22	/// use vortex_expr::{not, col};
23	/// use vortex_expr::forms::cnf::cnf;
24	///
25	/// let double_negation = not(not(col("a")));
26	/// let cnfed = cnf(double_negation);
27	/// assert_eq!(cnfed, vec![col("a")]);
28	/// ```
29	///
30	/// Unlike NNF, CNF, lifts conjunctions to the top-level and distributions disjunctions such that
31	/// there is at most one disjunction for each conjunction operand:
32	///
33	///
34	/// ```rust
35	/// use vortex_expr::{not, col, or, and};
36	/// use vortex_expr::forms::cnf::cnf;
37	///
38	/// assert_eq!(
39	/// cnf(
40	/// or(
41	/// and(col("a"), col("b")),
42	/// col("c"),
43	/// )
44	/// ),
45	/// vec![
46	/// or(col("a"), col("c")),
47	/// or(col("b"), col("c")),
48	/// ]
49	/// );
50	/// ```
51	///
52	pub fn cnf(expr: ExprRef) -> Vec<ExprRef> {	66✔
53	if expr == lit(true) {	66✔
54	// True in CNF
UNCOV 55	return vec![];	×
56	}	66✔
57	let nnf = nnf(expr);	66✔
58
59	let mut visitor = CNFVisitor::default();	66✔
60	nnf.accept(&mut visitor).vortex_expect("cannot fail");	66✔
61	visitor	66✔
62	.finish()	66✔
63	.into_iter()	66✔
64	.filter_map(\|disjunction\| disjunction.into_iter().reduce(or))	176✔
65	.collect_vec()	66✔
66	}	66✔
67
68	#[derive(Default)]
69	struct CNFVisitor {
70	conjuncts_of_disjuncts: Vec<Vec<ExprRef>>,
71	}
72
73	impl CNFVisitor {
74	fn finish(self) -> Vec<Vec<ExprRef>> {	286✔
75	self.conjuncts_of_disjuncts	286✔
76	}	286✔
77	}
78
79	impl NodeVisitor<'_> for CNFVisitor {
80	type NodeTy = ExprRef;
81
82	fn visit_down(&mut self, node: &ExprRef) -> VortexResult<TraversalOrder> {	462✔
83	if let Some(binary_expr) = node.as_opt::<BinaryVTable>() {	462✔
84	match binary_expr.op() {	330✔
85	Operator::And => return Ok(TraversalOrder::Continue),	88✔
86	Operator::Or => {
87	let mut visitor = CNFVisitor::default();	110✔
88	binary_expr.lhs().accept(&mut visitor)?;	110✔
89	let lhs_conjuncts = visitor.finish();	110✔
90
91	let mut visitor = CNFVisitor::default();	110✔
92	binary_expr.rhs().accept(&mut visitor)?;	110✔
93	let rhs_conjuncts = visitor.finish();	110✔
94
95	self.conjuncts_of_disjuncts	110✔
96	.extend(lhs_conjuncts.iter().flat_map(\|lhs_disjunct\| {	220✔
97	rhs_conjuncts.iter().map(\|rhs_disjunct\| {	264✔
98	let mut lhs_copy = lhs_disjunct.clone();	264✔
99	lhs_copy.extend(rhs_disjunct.iter().cloned());	264✔
100	lhs_copy	264✔
101	})	264✔
102	}));	220✔
103
104	return Ok(TraversalOrder::Skip);	110✔
105	}
106	_ => {}	132✔
107	}
108	}	132✔
109	// Anything other than And and Or are terminals from the perspective of CNF
110	self.conjuncts_of_disjuncts.push(vec![node.clone()]);	264✔
111	Ok(TraversalOrder::Skip)	264✔
112	}	462✔
113	}
114
115	#[cfg(test)]
116	mod tests {
117
118	use vortex_expr::forms::cnf::cnf;
119	use vortex_expr::{and, col, eq, gt_eq, lit, lt, not_eq, or};
120
121	#[test]
122	fn test_cnf_simple() {	1✔
123	assert_eq!(	1✔
124	cnf(or(or(and(col("a"), col("b")), col("c")), col("d"))),	1✔
125	vec![	1✔
126	or(or(col("a"), col("c")), col("d")),	1✔
127	or(or(col("b"), col("c")), col("d"))	1✔
128	]
129	);
130	}	1✔
131
132	#[test]
133	fn test_with_lit() {	1✔
134	assert_eq!(	1✔
135	cnf(or(	1✔
136	and(	1✔
137	gt_eq(col("earnings"), lit(50_000)),	1✔
138	not_eq(col("role"), lit("Manager"))	1✔
139	),	1✔
140	col("special_flag")	1✔
141	),),	1✔
142	vec![	1✔
143	or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),	1✔
144	or(not_eq(col("role"), lit("Manager")), col("special_flag"))	1✔
145	]
146	);
147	}	1✔
148
149	#[test]
150	fn test_cnf() {	1✔
151	assert_eq!(	1✔
152	cnf(or(	1✔
153	or(	1✔
154	and(	1✔
155	gt_eq(col("earnings"), lit(50_000)),	1✔
156	not_eq(col("role"), lit("Manager"))	1✔
157	),	1✔
158	col("special_flag")	1✔
159	),	1✔
160	and(lt(col("tenure"), lit(5)), eq(col("role"), lit("Engineer"))),	1✔
161	)),	1✔
162	vec![	1✔
163	or(	1✔
164	or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),	1✔
165	lt(col("tenure"), lit(5))	1✔
166	),
167	or(	1✔
168	or(gt_eq(col("earnings"), lit(50_000)), col("special_flag")),	1✔
169	eq(col("role"), lit("Engineer"))	1✔
170	),	1✔
171	or(	1✔
172	or(not_eq(col("role"), lit("Manager")), col("special_flag")),	1✔
173	lt(col("tenure"), lit(5))	1✔
174	),	1✔
175	or(	1✔
176	or(not_eq(col("role"), lit("Manager")), col("special_flag")),	1✔
177	eq(col("role"), lit("Engineer"))	1✔
178	)	1✔
179	]
180	);
181	}	1✔
182	}

vortex-data / vortex / 16835424474

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