[developers] subsumption packing and index accessibility filtering incompatible?
sweaglesw at sweaglesw.org
Mon Aug 6 16:29:37 CEST 2012
Here is an interesting problem that I ran across in my adventures of generation (with GG -- but of broader interest).
When packing under subsumption, we take advantage of a basic property that if R is a rule (or active edge) and X and Y are two edges with Y > X ("Y subsumes X"), and R(X) exists, then R(Y) exists and R(Y) > R(X). This enables a guarantee that anything that could be built from X can also be built (by analogy) from Y.
The problem is that there are cases where the index accessibility filter accepts X, Y, and R(X), but rejects R(Y). When X is packed in Y, we don't try to build R(X) because we assume R(Y) will be built and stand in for it, but in these circumstances that assumption is violated and we can miss results.
The crux of the issue is that a variable v can be visible on X and Y and R(X), but missing from R(Y). If v is mentioned by an EP outside the span of R(Y) (which is the same span as R(X)), then R(Y) is rejected while R(X) is (possibly) accepted.
Any solution needs to guarantee that if X and R(X) exist / pass the filter, and if X packs in Y, then (1) R(Y) exists / passes the filter and (2) R(X) packs in R(Y). Without (1) we will miss solutions and without (2) the retroactive packing freezing system will break.
Moving this to `developers' in hopes that someone has an idea,
More information about the developers