diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 751abd6a4..c099923ea 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -585,11 +585,11 @@ and handle_ty_app ?(update = false) ty_c l =
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
   | Some (
-      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt
+      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ }
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
-    Nest.add_nest [adt];
+    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -607,12 +607,12 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     in
     let lbs = List.rev rev_lbs in
     let record_constr = Uid.of_dolmen cstr in
-    let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
+    let ty = Ty.trecord ~record_constr tyvl uid lbs in
     Cache.store_ty ty_c ty
 
   | Some (Adt { cases; _ } as adt) ->
-    Nest.add_nest [adt];
-    let uid = Uid.of_dolmen ty_c in
+    let uid = Uid.of_ty_cst ty_c in
+    List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate [adt];
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
     Cache.store_ty ty_c (Ty.t_adt uid tyvl);
     let rev_cs =
@@ -627,7 +627,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
                 | None -> assert false
             ) [] dstrs
           in
-          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+          (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
       ) [] cases
     in
     let body = Some (List.rev rev_cs) in
@@ -704,7 +704,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
                   | None -> assert false
               ) [] dstrs
             in
-            (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+            (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
@@ -729,14 +729,14 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
           assert false
     ) ([], false) tdl
   in
-  Nest.add_nest rev_tdefs;
+  List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
         | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
-          let uid = Uid.of_dolmen ty_c in
+          let uid = Uid.of_ty_cst ty_c in
           let ty =
             if (record || Array.length cases = 1) && not contains_adts
             then
@@ -811,10 +811,10 @@ let mk_pattern DE.{ term_descr; _ } =
       ) [] (List.rev rev_vnames) pargs
     in
     let args = List.rev rev_args in
-    Typed.Constr {name = Uid.of_dolmen cst; args}
+    Typed.Constr {name = Uid.of_term_cst cst; args}
 
   | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = Uid.of_dolmen cst; args = []}
+    Typed.Constr {name = Uid.of_term_cst cst; args = []}
 
   | Var ({ builtin = B.Base; path; _ } as t_v) ->
     (* Should the type be passed as an argument
@@ -974,7 +974,7 @@ let rec mk_expr
               | Trecord _ as ty ->
                 E.mk_record [] ty
               | Tadt _ as ty ->
-                E.mk_constr (Uid.of_dolmen tcst) [] ty
+                E.mk_constr (Uid.of_term_cst tcst) [] ty
               | ty ->
                 Fmt.failwith "unexpected type %a@." Ty.print ty
             end
@@ -1041,7 +1041,7 @@ let rec mk_expr
               cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _
             }, [x] ->
             begin
-              let builtin = Sy.IsConstr (Uid.of_dolmen cstr) in
+              let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in
               let ty_c =
                 match DT.definition adt with
                 | Some (
@@ -1344,9 +1344,8 @@ let rec mk_expr
             let ty = dty_to_ty term_ty in
             begin match ty with
               | Ty.Tadt _ ->
-                let sy = Sy.constr @@ Uid.of_dolmen tcst in
                 let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_term sy l ty
+                E.mk_constr (Uid.of_term_cst tcst) l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_record l ty
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 18eb871b3..cae6b1a80 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -36,23 +36,42 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
-module TSet = Set.Make
-    (struct
-      type t = Uid.t
-
-      (* We use a dedicated total order on the constructors to ensure
-         the termination of the model generation. *)
-      let compare = Nest.compare
-    end)
+module DE = Dolmen.Std.Expr
+module DT = Dolmen.Std.Expr.Ty
+module B = Dolmen.Std.Builtin
+module TSet = Set.Make (Int)
 
 let timer = Timers.M_Adt
 
+(* HACK: this wrapper around [Uid.get_hash] is a temporary hack
+   used by the legacy frontend only. For the legacy frontend, we generate a
+   trivial perfect hash for the type [ty], that is a hash whose the associated
+   order does not ensure the termination of the model generation. *)
+let get_hash ty =
+  match ty with
+  | Ty.Tadt (name, params) ->
+    let cases = Ty.type_body name params in
+    begin match name with
+      | Ty_cst _ ->
+        Uid.get_hash name
+
+      | Hstring _ ->
+        let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
+        let of_int = List.nth cstrs in
+        let to_int id = Option.get @@ Lists.find_index (Uid.equal id) cstrs in
+        Uid.{ to_int; of_int }
+
+      | _ -> assert false
+    end
+  | _ -> assert false
+
 module Domain = struct
   (* Set of possible constructors. The explanation justifies that any value
      assigned to the semantic value has to use a constructor lying in the
      domain. *)
   type t = {
     constrs : TSet.t;
+    hash : Uid.hash;
     ex : Ex.t;
   }
 
@@ -60,24 +79,25 @@ module Domain = struct
 
   let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs
 
-  let[@inline always] choose { constrs; _ } =
+  let[@inline always] choose { constrs; hash; _ } =
     (* We choose the minimal element to ensure the termination of
        model generation. *)
-    TSet.min_elt constrs
+    TSet.min_elt constrs |> hash.of_int
 
-  let[@inline always] as_singleton { constrs; ex } =
+  let[@inline always] as_singleton { constrs; hash; ex; _ } =
     if TSet.cardinal constrs = 1 then
-      Some (TSet.choose constrs, ex)
+      Some (TSet.choose constrs |> hash.of_int, ex)
     else
       None
 
-  let domain ~constrs ex =
+  let domain ~constrs hash ex =
     if TSet.is_empty constrs then
       raise @@ Inconsistent ex
     else
-      { constrs; ex }
+      { constrs; hash; ex }
 
-  let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex }
+  let[@inline always] singleton ~ex hash c =
+    { constrs = TSet.singleton (hash.Uid.to_int c); hash; ex }
 
   let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
@@ -86,14 +106,15 @@ module Domain = struct
     | Ty.Tadt (name, params) ->
       (* Return the list of all the constructors of the type of [r]. *)
       let cases = Ty.type_body name params in
+      let hash = get_hash ty in
       let constrs =
         List.fold_left
           (fun acc Ty.{ constr; _ } ->
-             TSet.add constr acc
+             TSet.add (hash.to_int constr) acc
           ) TSet.empty cases
       in
       assert (not @@ TSet.is_empty constrs);
-      { constrs; ex = Ex.empty }
+      { constrs; hash; ex = Ex.empty }
     | _ ->
       (* Only ADT values can have a domain. This case shouldn't happen since
          we check the type of semantic values in both [add] and [assume]. *)
@@ -101,23 +122,27 @@ module Domain = struct
 
   let equal d1 d2 = TSet.equal d1.constrs d2.constrs
 
+  let pp_cstr of_int ppf i =
+    Uid.pp ppf @@ of_int i
+
   let pp ppf d =
     Fmt.(braces @@
-         iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs;
+         iter ~sep:comma TSet.iter (pp_cstr d.hash.Uid.of_int)) ppf d.constrs;
     if Options.(get_verbose () || get_unsat_core ()) then
       Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
 
   let intersect ~ex d1 d2 =
     let constrs = TSet.inter d1.constrs d2.constrs in
     let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
-    domain ~constrs ex
+    domain ~constrs d1.hash ex
 
-  let remove ~ex c d =
-    let constrs = TSet.remove c d.constrs in
-    let ex = Ex.union ex d.ex in
-    domain ~constrs ex
+  let remove ~ex c { constrs; hash; ex = ex' } =
+    let constrs = TSet.remove (hash.to_int c) constrs in
+    let ex = Ex.union ex' ex in
+    domain ~constrs hash ex
 
-  let for_all f { constrs; _ } = TSet.for_all f constrs
+  let for_all f { constrs; hash; _ } =
+    TSet.for_all (fun c -> f @@ hash.of_int c) constrs
 end
 
 let is_adt_ty = function
@@ -182,10 +207,11 @@ module Domains = struct
 
   let get r t =
     match Th.embed r with
-    | Constr { c_name; _ } ->
+    | Constr { c_name; c_ty; _ } ->
       (* For sake of efficiency, we don't look in the map if the
          semantic value is a constructor. *)
-      Domain.singleton ~ex:Explanation.empty c_name
+      let hash = get_hash c_ty in
+      Domain.singleton ~ex:Explanation.empty hash c_name
     | _ ->
       try MX.find r t.domains
       with Not_found ->
@@ -410,7 +436,7 @@ let assume_distinct =
           cannot be an application of the constructor [c]. *)
 let assume_is_constr ~ex r c domains =
   let d1 = Domains.get r domains in
-  let d2 = Domain.singleton ~ex:Explanation.empty c in
+  let d2 = Domain.singleton ~ex:Explanation.empty d1.hash c in
   let nd = Domain.intersect ~ex d1 d2 in
   Domains.tighten r nd domains
 
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 3a56a50ba..43230d58b 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -1881,8 +1881,7 @@ module Make (Th : Theory.S) = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ();
-    Nest.reinit ()
+    Uf.reinit_cache ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 0a3ed11f7..aaf94087e 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1393,8 +1393,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ();
-    Nest.reinit ()
+    Uf.reinit_cache ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 871955304..80f95ce29 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1262,7 +1262,7 @@ let mk_tester cons t =
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
 let void =
-  let cstr = Uid.of_dolmen Dolmen.Std.Expr.Term.Cstr.void in
+  let cstr = Uid.of_term_cst Dolmen.Std.Expr.Term.Cstr.void in
   mk_constr cstr [] Ty.tunit
 
 (** Substitutions *)
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index d12e38d51..b2341f3dc 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -93,8 +93,16 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
     List.map (fun c -> DStd.Path.global @@ to_smt_string c, []) cstrs
   in
   let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  let () =
+    match DStd.Expr.Ty.definition ty_cst with
+    | Some def ->
+      let name, hash = Nest.generate [def] |> List.hd in
+      Uid.set_hash name hash
+
+    | None -> assert false
+  in
   let body =
-    List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
+    List.map (fun (c, _) -> Uid.of_term_cst c, []) d_cstrs
   in
   let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index c00ddd47a..018cff950 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -536,15 +536,17 @@ let t_adt ?(body=None) s ty_vars =
 module DE = Dolmen.Std.Expr
 
 let tunit =
-  let name = Uid.of_dolmen DE.Ty.Const.unit in
-  let void = Uid.of_dolmen DE.Term.Cstr.void in
+  let name =
+    match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with
+    | Some def ->
+      let name, hash = Nest.generate [def] |> List.hd in
+      Uid.set_hash name hash;
+      name
+    | None -> assert false
+  in
+  let void = Uid.of_term_cst DE.Term.Cstr.void in
   let body = Some [void, []] in
   let ty = t_adt ~body name [] in
-  let () =
-    match DE.Ty.definition DE.Ty.Const.unit with
-    | Some def -> Nest.add_nest [def]
-    | _ -> assert false
-  in
   ty
 
 let trecord ?(sort_fields = false) ~record_constr lv name lbs =
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index a7c474371..99a503c61 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -26,23 +26,48 @@
 (**************************************************************************)
 
 module DStd = Dolmen.Std
-module DE = DStd.Expr
+module DE = Dolmen.Std.Expr
 
 type t =
   | Hstring : Hstring.t -> t
   | Dolmen : 'a DE.id -> t
+  | Term_cst : DE.term_cst -> t
+  | Ty_cst : DE.ty_cst -> t
+
+type hash = {
+  to_int : t -> int;
+  (** Return a perfect hash for the constructor. This hash is between [0]
+      and [n] where [n] is the number of constructors of the ADT. *)
+
+  of_int : int -> t;
+  (** Return the associated constructor to the integer.
+
+      @raises Invalid_argument if the integer does not correspond to
+       a constructor of this ADT. *)
+}
 
 let[@inline always] of_dolmen id = Dolmen id
+let[@inline always] of_term_cst id = Term_cst id
+let[@inline always] of_ty_cst id = Ty_cst id
 let[@inline always] of_hstring hs = Hstring hs
 let[@inline always] of_string s = of_hstring @@ Hstring.make s
 
+let[@inline always] to_term_cst id =
+  match id with
+  | Term_cst t -> t
+  | _ -> invalid_arg "to_term_cst"
+
 let hash = function
   | Hstring hs -> Hstring.hash hs
   | Dolmen id -> DE.Id.hash id
+  | Term_cst id -> DE.Id.hash id
+  | Ty_cst id -> DE.Id.hash id
 
 let pp ppf = function
   | Hstring hs -> Hstring.print ppf hs
   | Dolmen id -> DE.Id.print ppf id
+  | Term_cst id -> DE.Id.print ppf id
+  | Ty_cst id -> DE.Id.print ppf id
 
 let show = Fmt.to_to_string pp
 
@@ -50,14 +75,32 @@ let equal u1 u2 =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.equal hs1 hs2
   | Dolmen id1, Dolmen id2 -> DE.Id.equal id1 id2
+  | Term_cst id1, Term_cst id2 -> DE.Id.equal id1 id2
+  | Ty_cst id1, Ty_cst id2 -> DE.Id.equal id1 id2
   | _ -> String.equal (show u1) (show u2)
 
 let compare u1 u2 =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.compare hs1 hs2
   | Dolmen id1, Dolmen id2 -> DE.Id.compare id1 id2
+  | Term_cst id1, Term_cst id2 -> DE.Id.compare id1 id2
+  | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2
   | _ -> String.compare (show u1) (show u2)
 
+let hash_tag : hash DStd.Tag.t = DStd.Tag.create ()
+
+let set_hash id hash =
+  match id with
+  | Ty_cst ty_c ->
+    DE.Ty.Const.set_tag ty_c hash_tag hash
+  | _ -> Fmt.invalid_arg "set_hash %a" pp id
+
+let get_hash id =
+  match id with
+  | Ty_cst ty_c ->
+    Option.get @@ DE.Ty.Const.get_tag ty_c hash_tag
+  | _ -> Fmt.invalid_arg "get_hash %a" pp id
+
 module Set = Set.Make
     (struct
       type nonrec t = t
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index 09e0a7675..f308db982 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -30,15 +30,39 @@ module DE = Dolmen.Std.Expr
 type t = private
   | Hstring : Hstring.t -> t
   | Dolmen : 'a DE.id -> t
+  | Term_cst : DE.term_cst -> t
+  | Ty_cst : DE.ty_cst -> t
+
+type hash = {
+  to_int : t -> int;
+  (** Return a hash for the constructor. This hash is between [0] and [n]
+      exclusive where [n] is the number of constructors of the ADT. *)
+
+  of_int : int -> t;
+  (** Return the associated constructor to the integer.
+
+      @raises Invalid_argument if the integer does not correspond to
+       a constructor of this ADT. *)
+}
+(** Minimal perfect hash function for the constructors of an ADT. *)
 
 val of_dolmen : 'a DE.Id.t -> t
+val of_term_cst : DE.term_cst -> t
+val of_ty_cst : DE.ty_cst -> t
 val of_string : string -> t
 val of_hstring : Hstring.t -> t
+
+val to_term_cst : t -> DE.term_cst
+
 val hash : t -> int
 val pp : t Fmt.t
 val show : t -> string
 val equal : t -> t -> bool
 val compare : t -> t -> int
 
+val hash_tag : hash DE.Tags.t
+val set_hash : t -> hash -> unit
+val get_hash : t -> hash
+
 module Set : Set.S with type elt = t
 module Map : Map.S with type key = t
diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml
index b6ce0252d..dee944de4 100644
--- a/src/lib/util/lists.ml
+++ b/src/lib/util/lists.ml
@@ -82,3 +82,10 @@ let rec is_sorted cmp l =
   match l with
   | x :: y :: xs -> cmp x y <= 0 && is_sorted cmp (y :: xs)
   | [_] | [] -> true
+
+(* Copied from the Stdlib of OCaml 5.2. *)
+let find_index p =
+  let rec aux i = function
+      [] -> None
+    | a::l -> if p a then Some i else aux (i+1) l in
+  aux 0
diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli
index df2ee3f08..15e8c3017 100644
--- a/src/lib/util/lists.mli
+++ b/src/lib/util/lists.mli
@@ -67,3 +67,9 @@ val try_map : ('a -> 'b option) -> 'a list -> 'b list option
 val is_sorted : ('a -> 'a -> int) -> 'a list -> bool
 (** [is_sorted cmp l] checks that [l] is sorted for the comparison function
     [cmp]. *)
+
+val find_index : ('a -> bool) -> 'a list -> int option
+(** [find_index f l] returns [Some i], where [i] is the index of the first
+    element of the list [l] that satisfies [f x], if there is such an element.
+
+    It returns [None] if there is no such element. *)
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
index ac42686f8..ccab7bf0a 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -19,9 +19,7 @@
 module DStd = Dolmen.Std
 module DE = DStd.Expr
 module DT = DE.Ty
-module B = Dolmen.Std.Builtin
-
-type t = Dolmen.Std.Expr.ty_def list
+module B = DStd.Builtin
 
 (* A nest is the set of all the constructors of a mutually recursive definition
    of ADTs.
@@ -139,34 +137,57 @@ let build_graph (defs : DE.ty_def list) : Hp.t =
     ) defs;
   hp
 
-module H = Hashtbl.Make (Uid)
-
-(* Internal state used to store the current order. *)
-let add_cstr, find_weight, reinit =
-  let ctr = ref 0 in
-  let order : int H.t = H.create 100 in
-  let add_cstr cstr =
-    H.add order cstr !ctr;
-    incr ctr
-  and find_weight cstr =
-    try
-      H.find order cstr
-    with Not_found ->
-      Fmt.failwith "cannot find uid %a" Uid.pp cstr
-  and reinit () =
-    ctr := 0;
-    H.clear order
-  in add_cstr, find_weight, reinit
-
-(* Sort the constructors of the nest using a sorting based on
-   Kahn's algorithm. *)
-let add_nest n =
-  let hp = build_graph n in
+(* Tag used to attach the order of constructor. Used to
+   retrieve efficiency the order of the constructor in [to_int]. *)
+let order_tag : int DStd.Tag.t = DStd.Tag.create ()
+
+module H = struct
+  include Hashtbl.Make (DE.Ty.Const)
+
+  let add_cstr t (ty : DE.ty_cst) (cstr : DE.term_cst) =
+    match find t ty with
+    | len, cstrs ->
+      add t ty (len + 1, cstr :: cstrs); len
+    | exception Not_found ->
+      add t ty (1, [cstr]); 0
+
+  let to_hash t =
+    fold
+      (fun ty (_, cstrs) acc ->
+         let cstrs = Array.of_list cstrs in
+         let of_int =
+           let len = Array.length cstrs
+           in fun i ->
+             if i < 0 || i > len then
+               invalid_arg "hash"
+             else Array.unsafe_get cstrs (len-1-i) |> Uid.of_term_cst
+         in
+         let to_int cstr =
+           let d_cstr = Uid.to_term_cst cstr in
+           match DE.Term.Const.get_tag d_cstr order_tag with
+           | Some i -> i
+           | None ->
+             Fmt.failwith "the constructor %a has no order" DE.Id.print d_cstr
+         in
+         (Uid.of_ty_cst ty, Uid.{ to_int; of_int }) :: acc
+      ) t []
+end
+
+let ty_cst_of_cstr DE.{ builtin; _ } =
+  match builtin with
+  | B.Constructor { adt; _ } -> adt
+  | _ -> Fmt.failwith "expect an ADT constructor"
+
+let generate defs =
+  let hp = build_graph defs in
+  let r : (int * DE.term_cst list) H.t = H.create 17 in
   while not @@ Hp.is_empty hp do
     (* Loop invariant: the set of nodes in heap [hp] is exactly
        the set of the nodes of the graph without ingoing hyperedge. *)
-    let { id; outgoing; in_degree; _ } = Hp.pop_min hp in
-    add_cstr @@ Uid.of_dolmen id;
+    let { id; outgoing; in_degree;  _ } = Hp.pop_min hp in
+    let ty = ty_cst_of_cstr id in
+    let o = H.add_cstr r ty id in
+    DE.Term.Const.set_tag id order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -176,11 +197,5 @@ let add_nest n =
            Hp.insert hp node
       ) !outgoing;
     outgoing := [];
-  done
-
-let compare (id1 : Uid.t) (id2 : Uid.t) =
-  match id1, id2 with
-  | Dolmen _, Dolmen _ ->
-    find_weight id1 - find_weight id2
-  | _ ->
-    Uid.compare id1 id2
+  done;
+  H.to_hash r
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index 47777be59..154dff0e8 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -18,31 +18,19 @@
 
 module DE = Dolmen.Std.Expr
 
-(** The purpose of this module is to construct a total order on ADT
-    constructors to ensure the termination of model generation for
-    this theory.
-
-    By nest, we mean the set of all the constructors in a mutually
-    recursive definition of ADTs.
-
-    Before comparing constructors with [compare], the complete
-    nest to which they belong have to be added with [add_nest]. *)
-
-type t = DE.ty_def list
-(** Type of nest. *)
-
-val add_nest : t -> unit
-(** [add_nest defs] sorts and adds the nest [defs] in the current
-    internal order.
-
-    {b Note:} Assume that [defs] is a complete nest (in any order). *)
-
-val compare : Uid.t -> Uid.t -> int
-(** [compare id1 id2] compares the constructors [id1] and [id2] with
-    the order generated by [add_nest] if they are both Dolmen identifiers.
-
-    @raise Failure if the nests of the constructors [id1] and [id2] have not
-                   been added with [add_nest] before. *)
-
-val reinit : unit -> unit
-(** [reinit ()] clears all the registered constructors by [add_nest]. *)
+(** The purpose of this module is to construct appropriate total orders on ADT
+    constructors of a given type to ensure the termination of model generation
+    for this theory.
+
+    For each ADT type, we generate a minimal perfect hash function
+    for its set of constructors, that is a bijection between this set
+    on the integer between 0 and [n] exclusive, where [n] denotes the
+    number of constructors. The total order on ADT constructors is given by
+    the hash function. *)
+
+val generate : DE.ty_def list -> (Uid.t * Uid.hash) list
+(** [generate defs] generate minimal perfect hashes for each ADT of [defs].
+
+    {b Note:} assume that [defs] is a list of definitions of a complete nest
+    (in any order). By nest, we mean the set of all the constructors in a
+    mutually recursive definition of ADTs. *)