Add SMT encoding with sets as uninterpreted constants and functions as arrays

[rodrigo7491]

Initial evaluation of the arrays encoding indicates that SMT arrays provide significant performance gains when encoding TLA+ functions, but can cause a slowdown when compared to the oopsla19 encoding when encoding TLA+ sets. In light of this, we should add a new funArrays encoding, in which SMT arrays are used solely to encoded TLA+ functions.

Having two competing array encodings is intended to be a temporary situation, with the encoding shown to be more efficient by large scale evaluation intended to be kept and the other encoding intended to be removed.