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"

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

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

This restriction is a bit arbitrary, but it allows us to later safely call
get_ui() on scalarset bounds. In practice, no usable model should run into this
limit.

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"

This has no immediate relevance, but we're about to make the `prefix` parameter
to Generator a more complex type than std::string. This particular call site
will need to take advantage of this to pass through richer information than a
simple string that it can pass to generate_print().

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

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

Surprisingly, this was not used at all during symmetry reduction.

Github: related to #193 "State corruption with scalarset?"

Github: related to #193 "State corruption with scalarset?"

Similar to the situation in tests/193.m, we were not descending into TypeExprIDs
which was causing some records to not have their fields reordered.

Github: related to #193 "State corruption with scalarset?"