From 025ab5b10492d364bbdb4e4209f283f98e7fdcb7 Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 21:30:14 +1000 Subject: [PATCH 1/5] Add feature-gated PathMap DNF evaluator --- kernel/Cargo.toml | 3 +- kernel/src/lib.rs | 2 + kernel/src/path_dnf.rs | 205 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 209 insertions(+), 1 deletion(-) create mode 100644 kernel/src/path_dnf.rs diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index 6a42ac47..9c99e9af 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -36,4 +36,5 @@ z3 = [] no_search = [] grounding = [] specialize_io = [] -periodic_merkleize = [] \ No newline at end of file +periodic_merkleize = [] +experimental_dnf = [] diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs index b5667595..a99c3bbd 100644 --- a/kernel/src/lib.rs +++ b/kernel/src/lib.rs @@ -4,6 +4,8 @@ #![feature(stmt_expr_attributes)] #![feature(more_float_constants)] +#[cfg(feature = "experimental_dnf")] +pub mod path_dnf; pub mod space; mod sources; mod sinks; diff --git a/kernel/src/path_dnf.rs b/kernel/src/path_dnf.rs new file mode 100644 index 00000000..c9990143 --- /dev/null +++ b/kernel/src/path_dnf.rs @@ -0,0 +1,205 @@ +use pathmap::PathMap; + +/// Execution counters for a feature-gated PathMap DNF evaluation. +#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)] +pub struct DnfPathSetStats { + /// Number of disjunctive clauses supplied by the caller. + pub clauses: usize, + /// Total number of conjunctive factors across all clauses. + pub factors: usize, + /// Clauses with exactly one factor, which can be joined directly. + pub singleton_clauses: usize, + /// Clauses with at least two factors, which require meet operations. + pub multi_factor_clauses: usize, + /// Exact `PathMap::meet` operations used to materialize clause results. + pub meet_ops: usize, + /// Exact `PathMap::join` operations used to union clause results. + pub join_ops: usize, +} + +/// Result of evaluating a finite pathset expression in disjunctive normal form. +#[derive(Clone, Debug)] +pub struct DnfPathSetResult { + /// Exact pathset result of `clause0 OR clause1 OR ...`. + pub map: PathMap<()>, + /// Diagnostic counters that make the fallback work visible in tests. + pub stats: DnfPathSetStats, +} + +/// Errors for finite DNF pathset evaluation. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum DnfPathSetError { + /// An empty conjunction would denote the universal pathset, which is not a + /// finite `PathMap<()>` value. + EmptyClause { clause_index: usize }, +} + +/// Evaluates a finite pathset expression in disjunctive normal form. +/// +/// Each inner slice is a conjunction evaluated with [`PathMap::meet`]. Clause +/// results are then combined with [`PathMap::join`]. This is a guarded semantic +/// adapter for evaluating the PathMap `origin/dnf` zipper-merge idea without +/// depending on that branch's broader zipper and grafting API changes. +pub fn evaluate_pathmap_dnf( + clauses: &[&[&PathMap<()>]], +) -> Result { + let mut stats = DnfPathSetStats { + clauses: clauses.len(), + ..DnfPathSetStats::default() + }; + let mut result = PathMap::new(); + let mut has_result = false; + + for (clause_index, clause) in clauses.iter().enumerate() { + if clause.is_empty() { + return Err(DnfPathSetError::EmptyClause { clause_index }); + } + + stats.factors += clause.len(); + if clause.len() == 1 { + stats.singleton_clauses += 1; + } else { + stats.multi_factor_clauses += 1; + } + + let mut clause_map = clause[0].clone(); + for factor in &clause[1..] { + clause_map = clause_map.meet(factor); + stats.meet_ops += 1; + } + + if has_result { + result = result.join(&clause_map); + stats.join_ops += 1; + } else { + result = clause_map; + has_result = true; + } + } + + Ok(DnfPathSetResult { map: result, stats }) +} + +#[cfg(test)] +mod tests { + use super::*; + + type Paths = &'static [&'static [u8]]; + + const SMALL_TRIE_1: Paths = &[&[0, 1, 2], &[0, 1, 3]]; + const SMALL_TRIE_2: Paths = &[&[0, 1], &[0, 2], &[3], &[2, 3]]; + const SMALL_TRIE_3: Paths = &[&[0, 1, 2], &[0, 1, 3], &[0, 1, 4]]; + const EMPTY_PATHS: Paths = &[]; + + fn map(paths: Paths) -> PathMap<()> { + PathMap::from_iter(paths.iter().copied()) + } + + fn assert_same_paths(actual: &PathMap<()>, expected: &PathMap<()>, expected_paths: Paths) { + assert_eq!( + expected.val_count(), + expected_paths.len(), + "test expected list does not describe the complete expected map" + ); + + let mut remainder = actual.clone(); + for path in expected_paths { + assert!( + actual.path_exists_at(path), + "expected path {path:?} missing from actual result" + ); + assert!( + expected.path_exists_at(path), + "test expected list contains path {path:?} not present in expected map" + ); + remainder.remove_val_at(path, true); + } + + for path in SMALL_TRIE_1 + .iter() + .chain(SMALL_TRIE_2.iter()) + .chain(SMALL_TRIE_3.iter()) + { + assert_eq!( + actual.path_exists_at(path), + expected.path_exists_at(path), + "path {path:?} disagrees between actual and expected" + ); + } + assert_eq!( + remainder.val_count(), + 0, + "actual result contains extra paths" + ); + } + + #[test] + fn dnf_single_clause_matches_multiway_meet() { + let trie1 = map(SMALL_TRIE_1); + let trie2 = map(SMALL_TRIE_2); + let trie3 = map(SMALL_TRIE_3); + + let result = evaluate_pathmap_dnf(&[&[&trie1, &trie2, &trie3]]).unwrap(); + let expected = trie1.meet(&trie2).meet(&trie3); + + assert_same_paths(&result.map, &expected, EMPTY_PATHS); + assert_eq!(result.stats.clauses, 1); + assert_eq!(result.stats.factors, 3); + assert_eq!(result.stats.meet_ops, 2); + assert_eq!(result.stats.join_ops, 0); + } + + #[test] + fn dnf_singleton_clauses_match_multiway_join() { + let trie1 = map(SMALL_TRIE_1); + let trie2 = map(SMALL_TRIE_2); + let trie3 = map(SMALL_TRIE_3); + + let result = evaluate_pathmap_dnf(&[&[&trie1], &[&trie2], &[&trie3]]).unwrap(); + let expected = trie1.join(&trie2).join(&trie3); + + assert_same_paths( + &result.map, + &expected, + &[ + &[0, 1], + &[0, 1, 2], + &[0, 1, 3], + &[0, 1, 4], + &[0, 2], + &[2, 3], + &[3], + ], + ); + assert_eq!(result.stats.singleton_clauses, 3); + assert_eq!(result.stats.multi_factor_clauses, 0); + assert_eq!(result.stats.meet_ops, 0); + assert_eq!(result.stats.join_ops, 2); + } + + #[test] + fn dnf_partial_overlap_matches_distributed_reference() { + let trie1 = map(SMALL_TRIE_1); + let trie2 = map(SMALL_TRIE_2); + let trie3 = map(SMALL_TRIE_3); + + let result = evaluate_pathmap_dnf(&[&[&trie1, &trie2], &[&trie1, &trie3]]).unwrap(); + let expected = trie1.meet(&trie2.join(&trie3)); + + assert_same_paths(&result.map, &expected, SMALL_TRIE_1); + assert_eq!(result.stats.clauses, 2); + assert_eq!(result.stats.factors, 4); + assert_eq!(result.stats.meet_ops, 2); + assert_eq!(result.stats.join_ops, 1); + } + + #[test] + fn dnf_rejects_empty_clause_without_universal_pathset() { + let trie1 = map(SMALL_TRIE_1); + + assert_eq!( + evaluate_pathmap_dnf(&[&[&trie1], &[]]).unwrap_err(), + DnfPathSetError::EmptyClause { clause_index: 1 } + ); + } +} From 7a075baedc47dbab3c81d29f08d39ac8beee7f5f Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 21:31:03 +1000 Subject: [PATCH 2/5] Expose DNF materialization diagnostics --- kernel/src/path_dnf.rs | 54 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/kernel/src/path_dnf.rs b/kernel/src/path_dnf.rs index c9990143..e8a74da8 100644 --- a/kernel/src/path_dnf.rs +++ b/kernel/src/path_dnf.rs @@ -15,6 +15,20 @@ pub struct DnfPathSetStats { pub meet_ops: usize, /// Exact `PathMap::join` operations used to union clause results. pub join_ops: usize, + /// Distinct factor references observed by pointer identity. + pub distinct_factor_refs: usize, + /// Repeated factor references beyond the first occurrence. + pub repeated_factor_refs: usize, + /// Sum of input factor value counts across all clause positions. + pub factor_input_values: usize, + /// Sum of materialized clause-result value counts before final union. + pub clause_output_values: usize, + /// Clause-result values eliminated by duplicate-removing final union. + pub duplicate_clause_values: usize, + /// Largest materialized clause-result value count. + pub peak_clause_values: usize, + /// Largest materialized accumulated result value count. + pub peak_result_values: usize, } /// Result of evaluating a finite pathset expression in disjunctive normal form. @@ -49,6 +63,7 @@ pub fn evaluate_pathmap_dnf( }; let mut result = PathMap::new(); let mut has_result = false; + let mut distinct_factor_refs = Vec::new(); for (clause_index, clause) in clauses.iter().enumerate() { if clause.is_empty() { @@ -56,6 +71,17 @@ pub fn evaluate_pathmap_dnf( } stats.factors += clause.len(); + for factor in *clause { + stats.factor_input_values += factor.val_count(); + let factor_ref = std::ptr::from_ref(*factor).cast::<()>(); + if distinct_factor_refs.contains(&factor_ref) { + stats.repeated_factor_refs += 1; + } else { + distinct_factor_refs.push(factor_ref); + stats.distinct_factor_refs += 1; + } + } + if clause.len() == 1 { stats.singleton_clauses += 1; } else { @@ -67,6 +93,9 @@ pub fn evaluate_pathmap_dnf( clause_map = clause_map.meet(factor); stats.meet_ops += 1; } + let clause_values = clause_map.val_count(); + stats.clause_output_values += clause_values; + stats.peak_clause_values = stats.peak_clause_values.max(clause_values); if has_result { result = result.join(&clause_map); @@ -75,7 +104,11 @@ pub fn evaluate_pathmap_dnf( result = clause_map; has_result = true; } + stats.peak_result_values = stats.peak_result_values.max(result.val_count()); } + stats.duplicate_clause_values = stats + .clause_output_values + .saturating_sub(result.val_count()); Ok(DnfPathSetResult { map: result, stats }) } @@ -147,6 +180,13 @@ mod tests { assert_eq!(result.stats.factors, 3); assert_eq!(result.stats.meet_ops, 2); assert_eq!(result.stats.join_ops, 0); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 0); + assert_eq!(result.stats.factor_input_values, 9); + assert_eq!(result.stats.clause_output_values, 0); + assert_eq!(result.stats.duplicate_clause_values, 0); + assert_eq!(result.stats.peak_clause_values, 0); + assert_eq!(result.stats.peak_result_values, 0); } #[test] @@ -175,6 +215,13 @@ mod tests { assert_eq!(result.stats.multi_factor_clauses, 0); assert_eq!(result.stats.meet_ops, 0); assert_eq!(result.stats.join_ops, 2); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 0); + assert_eq!(result.stats.factor_input_values, 9); + assert_eq!(result.stats.clause_output_values, 9); + assert_eq!(result.stats.duplicate_clause_values, 2); + assert_eq!(result.stats.peak_clause_values, 4); + assert_eq!(result.stats.peak_result_values, 7); } #[test] @@ -191,6 +238,13 @@ mod tests { assert_eq!(result.stats.factors, 4); assert_eq!(result.stats.meet_ops, 2); assert_eq!(result.stats.join_ops, 1); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 1); + assert_eq!(result.stats.factor_input_values, 11); + assert_eq!(result.stats.clause_output_values, 2); + assert_eq!(result.stats.duplicate_clause_values, 0); + assert_eq!(result.stats.peak_clause_values, 2); + assert_eq!(result.stats.peak_result_values, 2); } #[test] From e20da83386178043fc5bc715211af6a7332b6d42 Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 21:31:08 +1000 Subject: [PATCH 3/5] Expose DNF existence shortcut --- kernel/src/path_dnf.rs | 178 ++++++++++++++++++++++++++++++++++------- 1 file changed, 148 insertions(+), 30 deletions(-) diff --git a/kernel/src/path_dnf.rs b/kernel/src/path_dnf.rs index e8a74da8..c04754ae 100644 --- a/kernel/src/path_dnf.rs +++ b/kernel/src/path_dnf.rs @@ -5,6 +5,10 @@ use pathmap::PathMap; pub struct DnfPathSetStats { /// Number of disjunctive clauses supplied by the caller. pub clauses: usize, + /// Clauses actually evaluated before completion or short-circuit. + pub clauses_evaluated: usize, + /// Clauses skipped by a short-circuiting aggregate query. + pub short_circuit_skipped_clauses: usize, /// Total number of conjunctive factors across all clauses. pub factors: usize, /// Clauses with exactly one factor, which can be joined directly. @@ -40,6 +44,17 @@ pub struct DnfPathSetResult { pub stats: DnfPathSetStats, } +/// Result of checking whether a finite DNF pathset is non-empty. +#[derive(Clone, Debug)] +pub struct DnfPathSetExistenceResult { + /// Whether at least one DNF clause produced an output path. + pub exists: bool, + /// Diagnostic counters for the short-circuiting DNF existence path. + pub stats: DnfPathSetStats, + /// Whether the final duplicate-eliminating output map was materialized. + pub final_output_materialized: bool, +} + /// Errors for finite DNF pathset evaluation. #[derive(Clone, Copy, Debug, Eq, PartialEq)] pub enum DnfPathSetError { @@ -66,36 +81,8 @@ pub fn evaluate_pathmap_dnf( let mut distinct_factor_refs = Vec::new(); for (clause_index, clause) in clauses.iter().enumerate() { - if clause.is_empty() { - return Err(DnfPathSetError::EmptyClause { clause_index }); - } - - stats.factors += clause.len(); - for factor in *clause { - stats.factor_input_values += factor.val_count(); - let factor_ref = std::ptr::from_ref(*factor).cast::<()>(); - if distinct_factor_refs.contains(&factor_ref) { - stats.repeated_factor_refs += 1; - } else { - distinct_factor_refs.push(factor_ref); - stats.distinct_factor_refs += 1; - } - } - - if clause.len() == 1 { - stats.singleton_clauses += 1; - } else { - stats.multi_factor_clauses += 1; - } - - let mut clause_map = clause[0].clone(); - for factor in &clause[1..] { - clause_map = clause_map.meet(factor); - stats.meet_ops += 1; - } - let clause_values = clause_map.val_count(); - stats.clause_output_values += clause_values; - stats.peak_clause_values = stats.peak_clause_values.max(clause_values); + let (clause_map, _) = + evaluate_clause(clause_index, clause, &mut stats, &mut distinct_factor_refs)?; if has_result { result = result.join(&clause_map); @@ -113,6 +100,102 @@ pub fn evaluate_pathmap_dnf( Ok(DnfPathSetResult { map: result, stats }) } +/// Checks whether a finite DNF pathset is non-empty without materializing the +/// final duplicate-eliminating union. +pub fn evaluate_pathmap_dnf_exists( + clauses: &[&[&PathMap<()>]], +) -> Result { + let mut stats = DnfPathSetStats { + clauses: clauses.len(), + ..DnfPathSetStats::default() + }; + let mut distinct_factor_refs = Vec::new(); + + for (clause_index, clause) in clauses.iter().enumerate() { + let (_, clause_values) = + evaluate_clause(clause_index, clause, &mut stats, &mut distinct_factor_refs)?; + + if clause_values > 0 { + stats.short_circuit_skipped_clauses = clauses.len().saturating_sub(clause_index + 1); + + return Ok(DnfPathSetExistenceResult { + exists: true, + stats, + final_output_materialized: false, + }); + } + } + + Ok(DnfPathSetExistenceResult { + exists: false, + stats, + final_output_materialized: false, + }) +} + +fn evaluate_clause( + clause_index: usize, + clause: &[&PathMap<()>], + stats: &mut DnfPathSetStats, + distinct_factor_refs: &mut Vec<*const ()>, +) -> Result<(PathMap<()>, usize), DnfPathSetError> { + if clause.is_empty() { + return Err(DnfPathSetError::EmptyClause { clause_index }); + } + + record_clause_inputs(stats, distinct_factor_refs, clause); + let clause_map = materialize_clause(clause, stats); + let clause_values = record_clause_output(stats, &clause_map); + + Ok((clause_map, clause_values)) +} + +fn record_clause_inputs( + stats: &mut DnfPathSetStats, + distinct_factor_refs: &mut Vec<*const ()>, + clause: &[&PathMap<()>], +) { + stats.clauses_evaluated += 1; + stats.factors += clause.len(); + + if clause.len() == 1 { + stats.singleton_clauses += 1; + } else { + stats.multi_factor_clauses += 1; + } + + for factor in clause { + stats.factor_input_values += factor.val_count(); + let factor_ref = std::ptr::from_ref(*factor).cast::<()>(); + if distinct_factor_refs.contains(&factor_ref) { + stats.repeated_factor_refs += 1; + } else { + distinct_factor_refs.push(factor_ref); + stats.distinct_factor_refs += 1; + } + } +} + +fn materialize_clause(clause: &[&PathMap<()>], stats: &mut DnfPathSetStats) -> PathMap<()> { + let mut clause_map = clause[0].clone(); + + for factor in &clause[1..] { + clause_map = clause_map.meet(factor); + stats.meet_ops += 1; + } + + clause_map +} + +fn record_clause_output(stats: &mut DnfPathSetStats, clause_map: &PathMap<()>) -> usize { + let clause_values = clause_map.val_count(); + + stats.clause_output_values += clause_values; + stats.peak_clause_values = stats.peak_clause_values.max(clause_values); + + clause_values +} + #[cfg(test)] mod tests { use super::*; @@ -177,6 +260,8 @@ mod tests { assert_same_paths(&result.map, &expected, EMPTY_PATHS); assert_eq!(result.stats.clauses, 1); + assert_eq!(result.stats.clauses_evaluated, 1); + assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.factors, 3); assert_eq!(result.stats.meet_ops, 2); assert_eq!(result.stats.join_ops, 0); @@ -212,6 +297,8 @@ mod tests { ], ); assert_eq!(result.stats.singleton_clauses, 3); + assert_eq!(result.stats.clauses_evaluated, 3); + assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.multi_factor_clauses, 0); assert_eq!(result.stats.meet_ops, 0); assert_eq!(result.stats.join_ops, 2); @@ -235,6 +322,8 @@ mod tests { assert_same_paths(&result.map, &expected, SMALL_TRIE_1); assert_eq!(result.stats.clauses, 2); + assert_eq!(result.stats.clauses_evaluated, 2); + assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.factors, 4); assert_eq!(result.stats.meet_ops, 2); assert_eq!(result.stats.join_ops, 1); @@ -256,4 +345,33 @@ mod tests { DnfPathSetError::EmptyClause { clause_index: 1 } ); } + + #[test] + fn dnf_exists_short_circuits_without_final_union() { + let trie1 = map(SMALL_TRIE_1); + let trie2 = map(SMALL_TRIE_2); + let trie3 = map(SMALL_TRIE_3); + + let result = + evaluate_pathmap_dnf_exists(&[&[&trie1, &trie2, &trie3], &[&trie1], &[&trie2]]) + .unwrap(); + + assert!(result.exists); + assert!(!result.final_output_materialized); + assert_eq!(result.stats.clauses, 3); + assert_eq!(result.stats.clauses_evaluated, 2); + assert_eq!(result.stats.short_circuit_skipped_clauses, 1); + assert_eq!(result.stats.factors, 4); + assert_eq!(result.stats.singleton_clauses, 1); + assert_eq!(result.stats.multi_factor_clauses, 1); + assert_eq!(result.stats.meet_ops, 2); + assert_eq!(result.stats.join_ops, 0); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 1); + assert_eq!(result.stats.factor_input_values, 11); + assert_eq!(result.stats.clause_output_values, 2); + assert_eq!(result.stats.duplicate_clause_values, 0); + assert_eq!(result.stats.peak_clause_values, 2); + assert_eq!(result.stats.peak_result_values, 0); + } } From 87bfb3b1371ba5b9c699fa5b73dba65dc805b8ab Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 21:32:11 +1000 Subject: [PATCH 4/5] Deduplicate DNF overlap assertions --- kernel/src/path_dnf.rs | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/kernel/src/path_dnf.rs b/kernel/src/path_dnf.rs index c04754ae..ec745415 100644 --- a/kernel/src/path_dnf.rs +++ b/kernel/src/path_dnf.rs @@ -249,6 +249,17 @@ mod tests { ); } + fn assert_overlap_stats(stats: DnfPathSetStats, join_ops: usize, peak_result_values: usize) { + assert_eq!(stats.join_ops, join_ops); + assert_eq!(stats.distinct_factor_refs, 3); + assert_eq!(stats.repeated_factor_refs, 1); + assert_eq!(stats.factor_input_values, 11); + assert_eq!(stats.clause_output_values, 2); + assert_eq!(stats.duplicate_clause_values, 0); + assert_eq!(stats.peak_clause_values, 2); + assert_eq!(stats.peak_result_values, peak_result_values); + } + #[test] fn dnf_single_clause_matches_multiway_meet() { let trie1 = map(SMALL_TRIE_1); @@ -326,14 +337,7 @@ mod tests { assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.factors, 4); assert_eq!(result.stats.meet_ops, 2); - assert_eq!(result.stats.join_ops, 1); - assert_eq!(result.stats.distinct_factor_refs, 3); - assert_eq!(result.stats.repeated_factor_refs, 1); - assert_eq!(result.stats.factor_input_values, 11); - assert_eq!(result.stats.clause_output_values, 2); - assert_eq!(result.stats.duplicate_clause_values, 0); - assert_eq!(result.stats.peak_clause_values, 2); - assert_eq!(result.stats.peak_result_values, 2); + assert_overlap_stats(result.stats, 1, 2); } #[test] @@ -365,13 +369,6 @@ mod tests { assert_eq!(result.stats.singleton_clauses, 1); assert_eq!(result.stats.multi_factor_clauses, 1); assert_eq!(result.stats.meet_ops, 2); - assert_eq!(result.stats.join_ops, 0); - assert_eq!(result.stats.distinct_factor_refs, 3); - assert_eq!(result.stats.repeated_factor_refs, 1); - assert_eq!(result.stats.factor_input_values, 11); - assert_eq!(result.stats.clause_output_values, 2); - assert_eq!(result.stats.duplicate_clause_values, 0); - assert_eq!(result.stats.peak_clause_values, 2); - assert_eq!(result.stats.peak_result_values, 0); + assert_overlap_stats(result.stats, 0, 0); } } From ab24e4bce603f83c4d8265c46450c34d9b5d37c9 Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 21:33:02 +1000 Subject: [PATCH 5/5] Prune empty DNF clauses --- kernel/src/path_dnf.rs | 213 ++++++++++++++++++++++++++++++----------- 1 file changed, 158 insertions(+), 55 deletions(-) diff --git a/kernel/src/path_dnf.rs b/kernel/src/path_dnf.rs index ec745415..dd7a660a 100644 --- a/kernel/src/path_dnf.rs +++ b/kernel/src/path_dnf.rs @@ -9,8 +9,13 @@ pub struct DnfPathSetStats { pub clauses_evaluated: usize, /// Clauses skipped by a short-circuiting aggregate query. pub short_circuit_skipped_clauses: usize, - /// Total number of conjunctive factors across all clauses. + /// Total number of supplied conjunctive factor positions in evaluated clauses. pub factors: usize, + /// Factor positions whose pathsets were actually inspected before a clause + /// completed or became empty. + pub factors_evaluated: usize, + /// Factor positions skipped after a conjunction became empty. + pub short_circuit_skipped_factors: usize, /// Clauses with exactly one factor, which can be joined directly. pub singleton_clauses: usize, /// Clauses with at least two factors, which require meet operations. @@ -29,6 +34,8 @@ pub struct DnfPathSetStats { pub clause_output_values: usize, /// Clause-result values eliminated by duplicate-removing final union. pub duplicate_clause_values: usize, + /// Evaluated clauses that produced an empty pathset. + pub empty_clause_results: usize, /// Largest materialized clause-result value count. pub peak_clause_values: usize, /// Largest materialized accumulated result value count. @@ -72,23 +79,23 @@ pub enum DnfPathSetError { pub fn evaluate_pathmap_dnf( clauses: &[&[&PathMap<()>]], ) -> Result { - let mut stats = DnfPathSetStats { - clauses: clauses.len(), - ..DnfPathSetStats::default() - }; + let (mut stats, mut distinct_factor_refs) = evaluator_state(clauses); let mut result = PathMap::new(); let mut has_result = false; - let mut distinct_factor_refs = Vec::new(); for (clause_index, clause) in clauses.iter().enumerate() { - let (clause_map, _) = + let clause_result = evaluate_clause(clause_index, clause, &mut stats, &mut distinct_factor_refs)?; + if clause_result.values == 0 { + continue; + } + if has_result { - result = result.join(&clause_map); + result = result.join(&clause_result.map); stats.join_ops += 1; } else { - result = clause_map; + result = clause_result.map; has_result = true; } stats.peak_result_values = stats.peak_result_values.max(result.val_count()); @@ -105,17 +112,13 @@ pub fn evaluate_pathmap_dnf( pub fn evaluate_pathmap_dnf_exists( clauses: &[&[&PathMap<()>]], ) -> Result { - let mut stats = DnfPathSetStats { - clauses: clauses.len(), - ..DnfPathSetStats::default() - }; - let mut distinct_factor_refs = Vec::new(); + let (mut stats, mut distinct_factor_refs) = evaluator_state(clauses); for (clause_index, clause) in clauses.iter().enumerate() { - let (_, clause_values) = + let clause_result = evaluate_clause(clause_index, clause, &mut stats, &mut distinct_factor_refs)?; - if clause_values > 0 { + if clause_result.values > 0 { stats.short_circuit_skipped_clauses = clauses.len().saturating_sub(clause_index + 1); return Ok(DnfPathSetExistenceResult { @@ -133,28 +136,42 @@ pub fn evaluate_pathmap_dnf_exists( }) } +fn evaluator_state(clauses: &[&[&PathMap<()>]]) -> (DnfPathSetStats, Vec<*const ()>) { + ( + DnfPathSetStats { + clauses: clauses.len(), + ..DnfPathSetStats::default() + }, + Vec::new(), + ) +} + +struct ClauseEvaluation { + map: PathMap<()>, + values: usize, +} + fn evaluate_clause( clause_index: usize, clause: &[&PathMap<()>], stats: &mut DnfPathSetStats, distinct_factor_refs: &mut Vec<*const ()>, -) -> Result<(PathMap<()>, usize), DnfPathSetError> { +) -> Result { if clause.is_empty() { return Err(DnfPathSetError::EmptyClause { clause_index }); } - record_clause_inputs(stats, distinct_factor_refs, clause); - let clause_map = materialize_clause(clause, stats); + record_clause_shape(stats, clause); + let clause_map = materialize_clause(clause, stats, distinct_factor_refs); let clause_values = record_clause_output(stats, &clause_map); - Ok((clause_map, clause_values)) + Ok(ClauseEvaluation { + map: clause_map, + values: clause_values, + }) } -fn record_clause_inputs( - stats: &mut DnfPathSetStats, - distinct_factor_refs: &mut Vec<*const ()>, - clause: &[&PathMap<()>], -) { +fn record_clause_shape(stats: &mut DnfPathSetStats, clause: &[&PathMap<()>]) { stats.clauses_evaluated += 1; stats.factors += clause.len(); @@ -163,25 +180,46 @@ fn record_clause_inputs( } else { stats.multi_factor_clauses += 1; } +} - for factor in clause { - stats.factor_input_values += factor.val_count(); - let factor_ref = std::ptr::from_ref(*factor).cast::<()>(); - if distinct_factor_refs.contains(&factor_ref) { - stats.repeated_factor_refs += 1; - } else { - distinct_factor_refs.push(factor_ref); - stats.distinct_factor_refs += 1; - } +fn record_factor_input( + stats: &mut DnfPathSetStats, + distinct_factor_refs: &mut Vec<*const ()>, + factor: &PathMap<()>, +) { + stats.factors_evaluated += 1; + stats.factor_input_values += factor.val_count(); + let factor_ref = std::ptr::from_ref(factor).cast::<()>(); + if distinct_factor_refs.contains(&factor_ref) { + stats.repeated_factor_refs += 1; + } else { + distinct_factor_refs.push(factor_ref); + stats.distinct_factor_refs += 1; } } -fn materialize_clause(clause: &[&PathMap<()>], stats: &mut DnfPathSetStats) -> PathMap<()> { +fn materialize_clause( + clause: &[&PathMap<()>], + stats: &mut DnfPathSetStats, + distinct_factor_refs: &mut Vec<*const ()>, +) -> PathMap<()> { + record_factor_input(stats, distinct_factor_refs, clause[0]); let mut clause_map = clause[0].clone(); - for factor in &clause[1..] { + if clause_map.is_empty() { + stats.short_circuit_skipped_factors += clause.len().saturating_sub(1); + return clause_map; + } + + for (factor_index, factor) in clause.iter().enumerate().skip(1) { + record_factor_input(stats, distinct_factor_refs, factor); clause_map = clause_map.meet(factor); stats.meet_ops += 1; + + if clause_map.is_empty() { + stats.short_circuit_skipped_factors += clause.len().saturating_sub(factor_index + 1); + break; + } } clause_map @@ -191,6 +229,7 @@ fn record_clause_output(stats: &mut DnfPathSetStats, clause_map: &PathMap<()>) - let clause_values = clause_map.val_count(); stats.clause_output_values += clause_values; + stats.empty_clause_results += usize::from(clause_values == 0); stats.peak_clause_values = stats.peak_clause_values.max(clause_values); clause_values @@ -249,17 +288,6 @@ mod tests { ); } - fn assert_overlap_stats(stats: DnfPathSetStats, join_ops: usize, peak_result_values: usize) { - assert_eq!(stats.join_ops, join_ops); - assert_eq!(stats.distinct_factor_refs, 3); - assert_eq!(stats.repeated_factor_refs, 1); - assert_eq!(stats.factor_input_values, 11); - assert_eq!(stats.clause_output_values, 2); - assert_eq!(stats.duplicate_clause_values, 0); - assert_eq!(stats.peak_clause_values, 2); - assert_eq!(stats.peak_result_values, peak_result_values); - } - #[test] fn dnf_single_clause_matches_multiway_meet() { let trie1 = map(SMALL_TRIE_1); @@ -274,13 +302,16 @@ mod tests { assert_eq!(result.stats.clauses_evaluated, 1); assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.factors, 3); - assert_eq!(result.stats.meet_ops, 2); + assert_eq!(result.stats.factors_evaluated, 2); + assert_eq!(result.stats.short_circuit_skipped_factors, 1); + assert_eq!(result.stats.meet_ops, 1); assert_eq!(result.stats.join_ops, 0); - assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.distinct_factor_refs, 2); assert_eq!(result.stats.repeated_factor_refs, 0); - assert_eq!(result.stats.factor_input_values, 9); + assert_eq!(result.stats.factor_input_values, 6); assert_eq!(result.stats.clause_output_values, 0); assert_eq!(result.stats.duplicate_clause_values, 0); + assert_eq!(result.stats.empty_clause_results, 1); assert_eq!(result.stats.peak_clause_values, 0); assert_eq!(result.stats.peak_result_values, 0); } @@ -311,6 +342,8 @@ mod tests { assert_eq!(result.stats.clauses_evaluated, 3); assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.multi_factor_clauses, 0); + assert_eq!(result.stats.factors_evaluated, 3); + assert_eq!(result.stats.short_circuit_skipped_factors, 0); assert_eq!(result.stats.meet_ops, 0); assert_eq!(result.stats.join_ops, 2); assert_eq!(result.stats.distinct_factor_refs, 3); @@ -318,6 +351,7 @@ mod tests { assert_eq!(result.stats.factor_input_values, 9); assert_eq!(result.stats.clause_output_values, 9); assert_eq!(result.stats.duplicate_clause_values, 2); + assert_eq!(result.stats.empty_clause_results, 0); assert_eq!(result.stats.peak_clause_values, 4); assert_eq!(result.stats.peak_result_values, 7); } @@ -336,8 +370,57 @@ mod tests { assert_eq!(result.stats.clauses_evaluated, 2); assert_eq!(result.stats.short_circuit_skipped_clauses, 0); assert_eq!(result.stats.factors, 4); + assert_eq!(result.stats.factors_evaluated, 4); + assert_eq!(result.stats.short_circuit_skipped_factors, 0); assert_eq!(result.stats.meet_ops, 2); - assert_overlap_stats(result.stats, 1, 2); + assert_eq!(result.stats.join_ops, 0); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 1); + assert_eq!(result.stats.factor_input_values, 11); + assert_eq!(result.stats.clause_output_values, 2); + assert_eq!(result.stats.duplicate_clause_values, 0); + assert_eq!(result.stats.empty_clause_results, 1); + assert_eq!(result.stats.peak_clause_values, 2); + assert_eq!(result.stats.peak_result_values, 2); + } + + #[test] + fn dnf_prunes_remaining_factors_after_empty_intermediate() { + let trie1 = map(SMALL_TRIE_1); + let trie2 = map(SMALL_TRIE_2); + let trie3 = map(SMALL_TRIE_3); + let empty = map(EMPTY_PATHS); + + let result = evaluate_pathmap_dnf(&[&[&trie1, &empty, &trie2, &trie3], &[&trie3]]).unwrap(); + + assert_same_paths(&result.map, &trie3, SMALL_TRIE_3); + assert_eq!(result.stats.clauses, 2); + assert_eq!(result.stats.clauses_evaluated, 2); + assert_eq!(result.stats.factors, 5); + assert_eq!(result.stats.factors_evaluated, 3); + assert_eq!( + ( + result.stats.short_circuit_skipped_factors, + result.stats.singleton_clauses, + result.stats.multi_factor_clauses, + result.stats.meet_ops, + result.stats.join_ops, + ), + (2, 1, 1, 1, 0) + ); + assert_eq!(result.stats.distinct_factor_refs, 3); + assert_eq!(result.stats.repeated_factor_refs, 0); + assert_eq!( + ( + result.stats.factor_input_values, + result.stats.clause_output_values, + result.stats.duplicate_clause_values, + result.stats.empty_clause_results, + result.stats.peak_clause_values, + result.stats.peak_result_values, + ), + (5, 3, 0, 1, 3, 3) + ); } #[test] @@ -366,9 +449,29 @@ mod tests { assert_eq!(result.stats.clauses_evaluated, 2); assert_eq!(result.stats.short_circuit_skipped_clauses, 1); assert_eq!(result.stats.factors, 4); - assert_eq!(result.stats.singleton_clauses, 1); - assert_eq!(result.stats.multi_factor_clauses, 1); - assert_eq!(result.stats.meet_ops, 2); - assert_overlap_stats(result.stats, 0, 0); + assert_eq!(result.stats.factors_evaluated, 3); + assert_eq!( + ( + result.stats.short_circuit_skipped_factors, + result.stats.singleton_clauses, + result.stats.multi_factor_clauses, + result.stats.meet_ops, + result.stats.join_ops, + ), + (1, 1, 1, 1, 0) + ); + assert_eq!(result.stats.distinct_factor_refs, 2); + assert_eq!(result.stats.repeated_factor_refs, 1); + assert_eq!( + ( + result.stats.factor_input_values, + result.stats.clause_output_values, + result.stats.duplicate_clause_values, + result.stats.empty_clause_results, + result.stats.peak_clause_values, + result.stats.peak_result_values, + ), + (8, 2, 0, 1, 2, 0) + ); } }