Github: related to #194 "clearer CEX output with scalarsets"

This is the final change that brings diff counterexample traces (the default)
inline with the user's expectations. Traces should now correctly suppress
printing of elements that have not changed and preserve elements that have
changed. The effect can be seen on tests/scalarset-cex.m.

Github: related to #194 "clearer CEX output with scalarsets"

Another baby step towards having the current handle and previous handle evolve
independently.

Github: related to #194 "clearer CEX output with scalarsets"

This is more preparation to generate independent handles when traversing a
scalarset-indexed array. The relative offset for a given array element in the
previous state is not the same as the relative offset in the current state,
because the previous and current states may have different schedules for the
index type.

E.g. given a scalarset(4), the original type contains {0, 1, 2, 3}. The schedule
of this type in the previous state might be the permutation {2, 3, 1, 0} while
the schedule in the current state might be {3, 2, 0, 1}. So when retrieving the
0th element of the array, this is actually at the 2nd element in the current
state and the 3rd element in the previous state.

Github: related to #194 "clearer CEX output with scalarsets"

This is necessary to handle scalarset-indexed arrays correctly. When comparing
to the previous value, the handle needs to be independent because it is mapped
through a different schedule.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Prior to this commit, we were diffing scalarset values during printing against
their raw representation, rather than their permuted value. Depending on your
perspective, this is either wrong or inaccurate. It would result in scalarset
fields in a diff counterexample trace (the default) sometimes being incorrectly
suppressed and sometimes being incorrectly shown.

Note that there is more work to be done here, as this does not address the
equivalent for scalarset indexed arrays.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

This sort of works, but it looks very confusing in a diff mode counterexample
trace (the default) because it tries to compare to previous values of the array
elements also using the schedule from the *successor* state rather than the
schedule from the *previous* state.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

We still need to implement the same for array indices.

Github: related to #194 "clearer CEX output with scalarsets"

This moves the canonicalisation functions earlier because this is now also where
schedule reading and writing functions are emitted. We will soon need to call
these from within startstates, rules, etc. if the input model prints scalarset
values.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

This is the equivalent change we did previously for heuristic canonicalisation,
but now for the exhaustive logic.

Github: related to #194 "clearer CEX output with scalarsets"

This code is implementing Heap's algorithm for generating all permutations of a
given range. The parameter that we previously called "schedule" is what is known
as "c" or the "stack" in the pedagogical description of the algorithm. Renaming
it helps avoid confusion, now that we're introducing something else called
"schedule" that is a concept of our own invention.

Github: related to #194 "clearer CEX output with scalarsets"

This is the data we need to later reconstruct the chosen scalarset permutation.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Without counterexample traces enabled, the only reason you need a schedule is
printing the value of a scalarset variable during a `put` statement. Without
such put statements, we don't need the schedules at all and can save memory.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Upcoming changes using the value of SYMMETRY_REDUCTION to construct an array's
bounds. Clang seems fine with this, but GCC does not consider a static const
constant enough to be involved in a bounds calculation.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

We will soon want to call this from other places when generating output.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

Previously such arrays were unrolled at code generation time. This was
suboptimal for large arrays (e.g. an array with an index type of `0 .. 10000`
would generate a huge amount of code to print it). However, the main motivation
for this change is that we would like to print scalarsets using more friendly
identifiers. This requires us to emit printing as a loop, because the order of
the elements is not known at code generation time.

Github: related to #194 "clearer CEX output with scalarsets"

To support printing arrays without unrolling, we will need to handle offsets
that use a loop counter.

Github: related to #194 "clearer CEX output with scalarsets"

Github: related to #194 "clearer CEX output with scalarsets"

This is a step towards allowing us to emit printing of an array type as a loop
instead of unrolling the array at code generation time.

Github: related to #194 "clearer CEX output with scalarsets"