The solver must join any newly created facts on either side of the join with the stable facts of the other side. Assuming stratification, G will remain constant while TC is computed (no newly created facts) and, by definition, will have fewer facts than TC.
The inefficient second pattern appears twice in polonius, albeit in more complex forms. First, in the naive variant:
This can be fixed by computing an intermediate relation, which I'll call subset_base_cfg, that propagates subset_base facts across the control-flow graph. We can then compute the transitive closure of subset_base_cfg at each point to obtain the original subset relation, like so:
AFAICT, the optimized variant is doing something similar, although subset passes through several intermediate relations, so it's hard to tell. Speed is also probably less important there, because the subset relation is aggressively filtered. This may have changed somewhat now that we compute subset_errors, however.
When computing a transitive closure (
TC
) for a graphG
using a semi-naive datalog solver, it is more efficient to use the first rule than the second.The solver must join any newly created facts on either side of the join with the stable facts of the other side. Assuming stratification,
G
will remain constant whileTC
is computed (no newly created facts) and, by definition, will have fewer facts thanTC
.The inefficient second pattern appears twice in polonius, albeit in more complex forms. First, in the naive variant:
https://github.com/rust-lang/polonius/blob/741e6095fe50f468982d4d253e842eb7d12ed9d3/polonius-engine/src/output/naive.rs#L136-L145
This can be fixed by computing an intermediate relation, which I'll call
subset_base_cfg
, that propagatessubset_base
facts across the control-flow graph. We can then compute the transitive closure ofsubset_base_cfg
at each point to obtain the originalsubset
relation, like so:AFAICT, the optimized variant is doing something similar, although
subset
passes through several intermediate relations, so it's hard to tell. Speed is also probably less important there, because thesubset
relation is aggressively filtered. This may have changed somewhat now that we computesubset_errors
, however.