GaloisInc / daedalus

The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
65 stars 11 forks source link

Add disjunctive slicing for sequenct nil/non-nil #313

Open simonjwinwood opened 1 year ago

simonjwinwood commented 1 year ago

Currently the slicing algorithm produces at most one slice for a looping construct, as the choice between 0 and 1 iteration must be shared across all slices (the number of loop iterations can be chosen lazily if we know the loop is non-empty). This is potentially a performance degredation as we get fewer, larger slices. One solution is to implement disjunctive slicing, where we split on whether a list is empty or not, and so slices have a sommon understanding of whether a loop is empty or not.