Check whether some entry `(p2, n2)` in `l2` with `p2 ⊆ p1` provides a contribution that dominates `n1.const` along every assignment satisfying `p1`'s activation. A `p2` entry contributes `n_p2.const` unconditionally (in that branch), and each `v ∈ n_p2.var` contributes at least `v.offset + 1` because `v.idx ∈ p2 ⊆ p1` guarantees `u_v ≥ 1`.
(l2: &NormLevel, p1: &[u64], c: u64)
| 581 | } |
| 582 | } |
| 583 | |
| 584 | // Comparison |
| 585 | |
| 586 | /// Check whether some entry `(p2, n2)` in `l2` with `p2 ⊆ p1` provides a |
| 587 | /// contribution that dominates `n1.const` along every assignment satisfying |
| 588 | /// `p1`'s activation. A `p2` entry contributes `n_p2.const` unconditionally |
| 589 | /// (in that branch), and each `v ∈ n_p2.var` contributes at least `v.offset + 1` |
| 590 | /// because `v.idx ∈ p2 ⊆ p1` guarantees `u_v ≥ 1`. |
| 591 | fn covers_const(l2: &NormLevel, p1: &[u64], c: u64) -> bool { |
no test coverage detected