More formally handle endianness swaps between Z3 and XLS

XLS holds its data in big-endian sort of format, where Bits::Get(0) will return the MSb. Z3 holds data in little-endian format.

This has caused me tremendous headaches; if we defined a more formal way of translating values between the two contexts, that'd probably save me a lot of headaches.