aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-10-10 17:28:05 +0200
committerMatthieu Sozeau2016-10-20 17:53:14 +0200
commitecaea9a428c052ea431ec7c392e81aaf918d5d96 (patch)
tree6ef8e9a62ded2734d307e7f917d4c310f893aa6a /kernel/cemitcodes.ml
parent3e536acf2ebcd078314dcac2a79d267c95db7bf8 (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