exhaustive scalarsets

[Smattr]

It occurred to me that it should be possible for the checker to identify when symmetry reduction results in an upper range of a scalarset type being unnecessary. For example, the user may define a scalarset(10) but the checker may find that in practice any value above 5 is always symmetric to one less. Hence, the user could have just defined a scalarset(6).

Extending this idea, it should be possible for the checker to take an "infinite" scalarset and find a "useful" upper bound to it. Subsequent to having this idea, I read David Dill's "A Retrospective on Murϕ" and realised he had already had this idea. It does not look like this was ever implemented in a Murphi variant, but it certainly seems like a worthwhile goal for Rumur.

[Smattr]

This notion is actually referred to as "data saturation" in C􏰈 Norris Ip and David L􏰈 Dill's "Better Verification Through Symmetry".