Start munging SMT printing into python.

With a mind for making this a little more modular.
Print team enumeration members
Define an uninterpreted scheduling function
Parameterise some bit widths
Prepare to distinct all slots per round.
Print match-distinct constraints.
Fix a little formatting
Fix some sorts
We may want to check satisfiability here.
Lay out some code for fetching found-schedule
Make integer printing indirect.
Fetch match schedule values after finding sat.
Add closeness constraints.

Just as before; ensure a bunch of spans are distinct.
Make Z3 optional.

This is horrible. but hey, whatever.
Pump up to a real quantity of teams etc.
Refactor sparticus
Fix an off-by-one.
Attempt to fix our goodness constraints.

Was only constraining one span it seems.
Distinguish each span, not all boundries.
Further off-by-one munging.

Had no functional effect, just replicated some constraints.