This PR implements the model generation for ADT. The model generation is
done by the casesplit mechanism in `Adt_rel`.

- If `--enable-adts-cs` is present, we do casesplits by choosing a
  delayed destructor as before after asserting.

- If there is no more delayed constructors, we look for a domain which
  contains a tightenable constructor (that is a constructor without
  payload) and we choose the domain as small as possible as it does in
  the `Enum` theory.

- If we are in model generation, we can also choose constructors with
  payload (but we still choose first constructors without payload).

- The termination of the model generation is ensured by a topological
  sorting during the parsing of the ADTs declarations.

Alt-Ergo answers `unsat` for this test on both `v2.5.4` and `next`
instead of producing a wrong model. `Z3` answers `unsat` too but
`cvc 5` answers `unknown`.