[generic] Automatic casting with Z3

[Brian Sniffen]

I've published the autocaster used for Wretched Hive and
others. It's probably not a great match for ten days---subtle
characters, only one run---but if you have many runs, algebraicly
described characters, and a lot of casting decisions to make
quickly, this might be of use:

    https://github.com/briansniffen/autocaster

It assumes you're getting your apps in a csv file, as from Google
Forms.  It uses the Z3 model checker / optimizing SMT solver to find a
good solution quickly, and an optimal solution eventually.