DNF reference evaluator, differentially sealed against PathMap's zipper_merge_dnf#95
Open
MesTTo wants to merge 1 commit into
Open
DNF reference evaluator, differentially sealed against PathMap's zipper_merge_dnf#95MesTTo wants to merge 1 commit into
MesTTo wants to merge 1 commit into
Conversation
One coherent feature-gated module in place of the four-PR refactor chain: evaluate/exists/count over union-of-meets, every step delegating to public PathMap algebra ops (meet, join, val_count, is_empty), with the instrumentation counters. The count path is the same duplicate-eliminating union as the full evaluation, only without returning the map: as the reference it stays the simplest correct thing, so the unmeasured disjoint-fragment fast path, its overlap checks, and the unreachable overflow error are gone, as is the constant-false final_output_materialized on the exists result. The `experimental_dnf` feature now forwards `pathmap/zipper_alg`, and the tests differentially seal PathMap's fused zipper_merge_dnf against this reference: the meet, join, and mixed shapes plus 60 deterministic random DNFs agree exactly. One real divergence is pinned rather than hidden: an empty clause is an error here (empty conjunction = TOP, unrepresentable) but an empty contribution (BOTTOM) in the fused engine; one convention should win before either is load-bearing.
MesTTo
force-pushed
the
pr/mork-pathset-dnf-evaluator
branch
from
025ab5b to
8399af5
Compare
MesTTo
changed the title
This was referenced Jul 4, 2026
Closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A feature-gated DNF reference evaluator over PathMap pathsets:
evaluate_pathmap_dnf/..._exists/..._countover union-of-meets, every step delegating to public PathMap algebra ops (meet,join,val_count,is_empty), with instrumentation counters. Gated behindexperimental_dnf, which now also forwardspathmap/zipper_alg.Its purpose is to be the differential oracle for PathMap's fused
zipper_merge_dnf(the DNF zipper-merge that landed in PathMap): the tests seal the fused engine against this reference on the meet, join, and mixed shapes plus 60 deterministic random DNFs — all agree exactly. One real divergence is pinned rather than hidden: an empty clause is an error here (empty conjunction = ⊤, unrepresentable as a finite pathset) but an empty contribution (⊥) in the fused engine. One convention should win before either becomes load-bearing; flagging it for a decision.This consolidates what was previously split across #96 (diagnostics/exists), #97 (pruning), #98 (exact count) — those were serialized rewrites of the same function bodies, not separable concerns, so they are folded here and trimmed: the count path is the same duplicate-eliminating union without returning the map (the unmeasured disjoint-fragment fast path, its O(k²) overlap checks, and the unreachable overflow error are gone), and the constant
final_output_materializedon the exists result is dropped.