diff options
| author | Matthieu Sozeau | 2016-10-10 17:28:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:53:14 +0200 |
| commit | ecaea9a428c052ea431ec7c392e81aaf918d5d96 (patch) | |
| tree | 6ef8e9a62ded2734d307e7f917d4c310f893aa6a /kernel/cemitcodes.ml | |
| parent | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (diff) | |
Fix minimization to be insensitive to redundant arcs.
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions
