Use the Dolmen identifiers for constructors and ADT names

[Halbaroth]

We don't manage correctly incremental type declarations. For instance the following input is accepted by the SMT-LIB standard:

(set-logic ALL)
(push 1)
(declare-datatype t
  ((c1 (d1 Int)) (c2)))
(pop 1)
(declare-datatype t
  ((c2 (d1 Int)) (c1)))
(declare-const x t)
(declare-const y t)
(assert ((_ is c1) x))
(assert ((_ is c1) y))
(assert (distinct x y))
(check-sat)

(Notice that we switch the constructors c1 and c2 in our second declaration of the type t). AE answers unknown on next but it answers unsat if we remove the first declaration of t.

This PR fixes the issue for the new frontend only. So we got unsat with --frontend dolmen but we still got unknown with --frontend legacy.

The solution consists in using the unique identifiers produced by Dolmen for the constructors, destructors and names of ADTs. To reduce as much as possible the amount of modification done in the legacy typechecker, I wrapped Dolmen's identifiers in a new module Uid. This module agrees with Hstring if we use the constructors of_string or of_hstring and it uses Dolmen's identifiers if we use the constructor of_dolmen. Of course, we'll get rid of this module as soon as we remove the legacy frontend.

I didn't use a unique identifier for the constructor of builtin enumeration types. This case will be fixed after removing the legacy frontend.

This PR is supposed to be merged before #1093

[Halbaroth]

The PR is ready for a second pass. I think we should test the legacy frontend with fpa on Marvin before merging it.

[Halbaroth]

I rebase this PR on #1117 to remove some polymorphic comparisons again ;)

[Halbaroth]

No regression with the following combinations:

• frontend legacy on ae-format
• frontend legacy on ae-format-fpa with --enable-theories fpa
• frontend dolmen on ae-format
• frontend dolmen on ae-format-fpa with --enable-theories fpa

So this PR is ready for I hope a last check ;)