Skip to content

zipper_merge_dnf: empty clause is silently bottom, the algebra says top #64

Description

@MesTTo

clause_mask in experimental/zipper_algebra.rs returns ByteMask::EMPTY when a clause has no members, so an empty clause contributes nothing to the merge. As DNF algebra the empty conjunction is top (the identity of meet), which over pathsets is the everything-set and not representable as a finite trie, so PathMap cannot honor it; but honoring it silently as bottom inverts its meaning. Today Clause::FULL and the dnf! macro never produce one, so nothing is wrong in-tree; the hazard is a programmatic Clause builder that filters members down to none and silently flips from "always contributes" to "never contributes". One line settles it either way: a debug_assert!(!clause.is_empty()) in zipper_merge_dnf, or a doc sentence on Clause stating the empty clause is treated as bottom by convention.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Labels

No labels
No labels

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions