From 6743244837981031f3708fa80884fc5ebcc2d1eb Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 20 Jun 2024 14:51:02 +0200
Subject: [PATCH 1/8] Use Dolmen attribute to store well founded order

This PR used the well designed Dolmen to store a custom attribute on
constructors of ADT and ADT themself. This design has two advantages:
1. We don't need to store an extra global state for the total order
   generated in the module `Nest`.
2. We have a total order per ADT instead of a global order for all the
   ADT types.

To be more specific, we generate a bijection between ADT constructors and the interval [0, n[ where n is the number of constructors.
---
 src/lib/frontend/d_cnf.ml           | 29 +++++-----
 src/lib/reasoners/adt_rel.ml        | 80 +++++++++++++++++---------
 src/lib/reasoners/fun_sat.ml        |  3 +-
 src/lib/reasoners/satml_frontend.ml |  3 +-
 src/lib/structures/expr.ml          |  2 +-
 src/lib/structures/fpa_rounding.ml  | 10 +++-
 src/lib/structures/ty.ml            | 16 +++---
 src/lib/structures/uid.ml           | 45 ++++++++++++++-
 src/lib/structures/uid.mli          | 24 ++++++++
 src/lib/util/lists.ml               |  7 +++
 src/lib/util/lists.mli              |  6 ++
 src/lib/util/nest.ml                | 87 +++++++++++++++++------------
 src/lib/util/nest.mli               | 44 ++++++---------
 13 files changed, 236 insertions(+), 120 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 78b301fdbe..b24cd0dfc3 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 (
@@ -1326,9 +1326,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 18eb871b3f..cae6b1a801 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 3a56a50ba7..43230d58b7 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 0a3ed11f7a..aaf94087ef 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 1e9bbe92e0..4d47d8ed22 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1276,7 +1276,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 d12e38d513..b2341f3dc3 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 c00ddd47ae..018cff9503 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 a7c4743713..99a503c610 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 09e0a76759..f308db9821 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 b6ce0252d8..dee944de4a 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 df2ee3f082..15e8c30172 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 ac42686f82..ccab7bf0a8 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 47777be59e..84ba660b07 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 an appropriate total order on
+    constructors of a given ADT 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. *)

From 7ac984a373653c894447b5f6109abfca3bd5eafd Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 9 Jul 2024 15:59:55 +0200
Subject: [PATCH 2/8] review changes

---
 src/lib/frontend/d_cnf.ml          |  4 +-
 src/lib/reasoners/adt_rel.ml       | 79 ++++++++++++------------------
 src/lib/structures/fpa_rounding.ml |  5 +-
 src/lib/structures/ty.ml           |  9 ++--
 src/lib/structures/uid.ml          | 30 +++---------
 src/lib/structures/uid.mli         | 22 ++-------
 src/lib/util/nest.ml               | 32 ++----------
 src/lib/util/nest.mli              |  5 +-
 8 files changed, 54 insertions(+), 132 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index b24cd0dfc3..e7ee687e30 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -612,7 +612,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
 
   | Some (Adt { cases; _ } as adt) ->
     let uid = Uid.of_ty_cst ty_c in
-    List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate [adt];
+    Nest.attach_orders [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 =
@@ -729,7 +729,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
           assert false
     ) ([], false) tdl
   in
-  List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate rev_tdefs;
+  Nest.attach_orders rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index cae6b1a801..213c1523d1 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -39,31 +39,19 @@ module SLR = Set.Make(LR)
 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
+module TSet =
+  Set.Make
+    (struct
+      type t = Uid.t
 
-(* 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
+      (* We use a dedicated total order on the constructors to ensure
+         the termination of model generation. *)
+      let compare id1 id2 =
+        Uid.perfect_hash id1 - Uid.perfect_hash id2
+    end)
 
-      | 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
+let timer = Timers.M_Adt
 
 module Domain = struct
   (* Set of possible constructors. The explanation justifies that any value
@@ -71,7 +59,6 @@ module Domain = struct
      domain. *)
   type t = {
     constrs : TSet.t;
-    hash : Uid.hash;
     ex : Ex.t;
   }
 
@@ -79,25 +66,25 @@ module Domain = struct
 
   let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs
 
-  let[@inline always] choose { constrs; hash; _ } =
+  let[@inline always] choose { constrs; _ } =
     (* We choose the minimal element to ensure the termination of
        model generation. *)
-    TSet.min_elt constrs |> hash.of_int
+    TSet.min_elt constrs
 
-  let[@inline always] as_singleton { constrs; hash; ex; _ } =
+  let[@inline always] as_singleton { constrs; ex } =
     if TSet.cardinal constrs = 1 then
-      Some (TSet.choose constrs |> hash.of_int, ex)
+      Some (TSet.choose constrs, ex)
     else
       None
 
-  let domain ~constrs hash ex =
+  let domain ~constrs ex =
     if TSet.is_empty constrs then
       raise @@ Inconsistent ex
     else
-      { constrs; hash; ex }
+      { constrs; ex }
 
-  let[@inline always] singleton ~ex hash c =
-    { constrs = TSet.singleton (hash.Uid.to_int c); hash; ex }
+  let[@inline always] singleton ~ex c =
+    { constrs = TSet.singleton c; ex }
 
   let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
@@ -106,15 +93,14 @@ 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 (hash.to_int constr) acc
+             TSet.add constr acc
           ) TSet.empty cases
       in
       assert (not @@ TSet.is_empty constrs);
-      { constrs; hash; ex = Ex.empty }
+      { constrs; 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]. *)
@@ -122,27 +108,23 @@ 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 (pp_cstr d.hash.Uid.of_int)) ppf d.constrs;
+         iter ~sep:comma TSet.iter Uid.pp) 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 d1.hash ex
+    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 remove ~ex c d =
+    let constrs = TSet.remove c d.constrs in
+    let ex = Ex.union ex d.ex in
+    domain ~constrs ex
 
-  let for_all f { constrs; hash; _ } =
-    TSet.for_all (fun c -> f @@ hash.of_int c) constrs
+  let for_all f { constrs; _ } = TSet.for_all f constrs
 end
 
 let is_adt_ty = function
@@ -207,11 +189,10 @@ module Domains = struct
 
   let get r t =
     match Th.embed r with
-    | Constr { c_name; c_ty; _ } ->
+    | Constr { c_name; _ } ->
       (* For sake of efficiency, we don't look in the map if the
          semantic value is a constructor. *)
-      let hash = get_hash c_ty in
-      Domain.singleton ~ex:Explanation.empty hash c_name
+      Domain.singleton ~ex:Explanation.empty c_name
     | _ ->
       try MX.find r t.domains
       with Not_found ->
@@ -436,7 +417,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 d1.hash c in
+  let d2 = Domain.singleton ~ex:Explanation.empty c in
   let nd = Domain.intersect ~ex d1 d2 in
   Domains.tighten r nd domains
 
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index b2341f3dc3..754839ae8f 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -95,10 +95,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   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
-
+    | Some def -> Nest.attach_orders [def]
     | None -> assert false
   in
   let body =
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 018cff9503..39424257f8 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -536,17 +536,14 @@ let t_adt ?(body=None) s ty_vars =
 module DE = Dolmen.Std.Expr
 
 let tunit =
-  let name =
+  let () =
     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
+    | Some def -> Nest.attach_orders [def]
     | 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 ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] 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 99a503c610..0d594d0393 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -34,18 +34,6 @@ type 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
@@ -87,19 +75,15 @@ let compare u1 u2 =
   | 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 order_tag : int DStd.Tag.t = DStd.Tag.create ()
 
-let get_hash id =
+let perfect_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
+  | Term_cst id ->
+    Option.get @@ DE.Term.Const.get_tag id order_tag
+  | Hstring hs ->
+    Hstring.hash hs
+  | _ -> assert false
 
 module Set = Set.Make
     (struct
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index f308db9821..45553fcf12 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -33,19 +33,6 @@ type t = private
   | 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
@@ -54,15 +41,16 @@ val of_hstring : Hstring.t -> t
 
 val to_term_cst : t -> DE.term_cst
 
+val order_tag : int Dolmen.Std.Tag.t
+(** Tag used to attach the order of constructor. Used to
+    retrieve efficiency the order of the constructor in [to_int]. *)
+
+val perfect_hash : t -> int
 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/nest.ml b/src/lib/util/nest.ml
index ccab7bf0a8..fa80dfbc20 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -137,10 +137,6 @@ let build_graph (defs : DE.ty_def list) : Hp.t =
     ) defs;
   hp
 
-(* 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)
 
@@ -150,27 +146,6 @@ module H = struct
       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; _ } =
@@ -178,7 +153,7 @@ let ty_cst_of_cstr DE.{ builtin; _ } =
   | B.Constructor { adt; _ } -> adt
   | _ -> Fmt.failwith "expect an ADT constructor"
 
-let generate defs =
+let attach_orders 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
@@ -187,7 +162,7 @@ let generate defs =
     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;
+    DE.Term.Const.set_tag id Uid.order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -197,5 +172,4 @@ let generate defs =
            Hp.insert hp node
       ) !outgoing;
     outgoing := [];
-  done;
-  H.to_hash r
+  done
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index 84ba660b07..a466903f38 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -28,8 +28,9 @@ module DE = Dolmen.Std.Expr
     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].
+val attach_orders : DE.ty_def list -> unit
+(** [attach_orders defs] generate and attach orders on the constructors 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

From f421b437026f9ffe4d57e2552fa057bd641cef96 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 10 Jul 2024 13:06:08 +0200
Subject: [PATCH 3/8] Remove dead code

---
 src/lib/util/lists.ml  | 7 -------
 src/lib/util/lists.mli | 6 ------
 2 files changed, 13 deletions(-)

diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml
index dee944de4a..b6ce0252d8 100644
--- a/src/lib/util/lists.ml
+++ b/src/lib/util/lists.ml
@@ -82,10 +82,3 @@ 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 15e8c30172..df2ee3f082 100644
--- a/src/lib/util/lists.mli
+++ b/src/lib/util/lists.mli
@@ -67,9 +67,3 @@ 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. *)

From 39ba617ed33deb547d48d1dbebb05f8428ea4414 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 10 Jul 2024 14:47:45 +0200
Subject: [PATCH 4/8] Use polymorphic GADT for UId.t

---
 src/lib/frontend/d_cnf.ml          | 29 ++++++++++---------
 src/lib/frontend/typechecker.ml    | 24 +++++++++-------
 src/lib/reasoners/adt.ml           |  9 ++++--
 src/lib/reasoners/adt.mli          | 10 +++++--
 src/lib/reasoners/adt_rel.ml       |  4 +--
 src/lib/reasoners/records.ml       |  4 +--
 src/lib/reasoners/theory.ml        | 12 ++++----
 src/lib/structures/expr.mli        |  4 +--
 src/lib/structures/fpa_rounding.ml |  2 +-
 src/lib/structures/symbols.ml      |  8 +++---
 src/lib/structures/symbols.mli     | 12 ++++----
 src/lib/structures/ty.ml           | 19 ++++++------
 src/lib/structures/ty.mli          | 26 +++++++++--------
 src/lib/structures/typed.ml        |  2 +-
 src/lib/structures/typed.mli       |  2 +-
 src/lib/structures/uid.ml          | 46 +++++++++++++++++-------------
 src/lib/structures/uid.mli         | 42 +++++++++++++++------------
 src/lib/structures/xliteral.ml     |  2 +-
 src/lib/structures/xliteral.mli    |  2 +-
 19 files changed, 143 insertions(+), 116 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index e7ee687e30..eff26b99d0 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -106,15 +106,17 @@ module Cache = struct
     then Ty.fresh_tvar ()
     else
       match id with
-      | Some id -> Ty.text [] (Uid.of_dolmen id)
+      | Some id -> Ty.text [] (Uid.of_string id)
       | None -> Ty.fresh_empty_text ()
 
+  let show (type a) (id : a DE.id) = Fmt.to_to_string DE.Id.print id
+
   let update_ty_store ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
+    let ty = fresh_ty ~is_var ~id:(show id) () in
     store_ty id ty
 
   let update_ty_store_ret ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
+    let ty = fresh_ty ~is_var ~id:(show id) () in
     store_ty id ty;
     ty
 
@@ -597,7 +599,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
           match c with
           | Some (DE.{ id_ty; _ } as id) ->
             let pty = dty_to_ty id_ty in
-            (Uid.of_dolmen id, pty) :: acc
+            (Uid.of_term_cst id, pty) :: acc
           | _ ->
             Fmt.failwith
               "Unexpected null label for some field of the record type %a"
@@ -606,7 +608,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
       ) [] dstrs
     in
     let lbs = List.rev rev_lbs in
-    let record_constr = Uid.of_dolmen cstr in
+    let record_constr = Uid.of_term_cst cstr in
     let ty = Ty.trecord ~record_constr tyvl uid lbs in
     Cache.store_ty ty_c ty
 
@@ -623,7 +625,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
               fun acc tc_o ->
                 match tc_o with
                 | Some (DE.{ id_ty; _ } as field) ->
-                  (Uid.of_dolmen field, dty_to_ty id_ty) :: acc
+                  (Uid.of_term_cst field, dty_to_ty id_ty) :: acc
                 | None -> assert false
             ) [] dstrs
           in
@@ -638,7 +640,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let ty_params = []
     (* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *)
     in
-    let ty = Ty.text ty_params (Uid.of_dolmen ty_c) in
+    let ty = Ty.text ty_params (Uid.of_ty_cst ty_c) in
     Cache.store_ty ty_c ty
 
 (** Handles term declaration by storing the eventual present type variables
@@ -678,7 +680,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             match c with
             | Some (DE.{ id_ty; _ } as id) ->
               let pty = dty_to_ty id_ty in
-              (Uid.of_dolmen id, pty) :: acc
+              (Uid.of_term_cst id, pty) :: acc
             | _ ->
               Fmt.failwith
                 "Unexpected null label for some field of the record type %a"
@@ -700,7 +702,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
                 fun acc tc_o ->
                   match tc_o with
                   | Some (DE.{ id_ty; _ } as id) ->
-                    (Uid.of_dolmen id, dty_to_ty id_ty) :: acc
+                    (Uid.of_term_cst id, dty_to_ty id_ty) :: acc
                   | None -> assert false
               ) [] dstrs
             in
@@ -737,10 +739,11 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
         | 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_ty_cst ty_c in
+          let record_constr = Uid.of_term_cst cases.(0).cstr in
           let ty =
             if (record || Array.length cases = 1) && not contains_adts
             then
-              Ty.trecord ~record_constr:uid tyvl uid []
+              Ty.trecord ~record_constr tyvl uid []
             else
               Ty.t_adt uid tyvl
           in
@@ -793,7 +796,7 @@ let mk_pattern DE.{ term_descr; _ } =
           Array.fold_left (
             fun acc v ->
               match v with
-              | Some dstr -> Uid.of_dolmen dstr :: acc
+              | Some dstr -> Uid.of_term_cst dstr :: acc
               | _ -> assert false
           ) [] dstrs
         | _ ->
@@ -1019,9 +1022,9 @@ let rec mk_expr
                     let sy =
                       match Cache.find_ty adt with
                       | Trecord _ ->
-                        Sy.Op (Sy.Access (Uid.of_dolmen destr))
+                        Sy.Op (Sy.Access (Uid.of_term_cst destr))
                       | Tadt _ ->
-                        Sy.destruct (Uid.of_dolmen destr)
+                        Sy.destruct (Uid.of_term_cst destr)
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 3c8f971e5f..fddbe43b5b 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -190,12 +190,12 @@ module Types = struct
     let rec check_duplicates s = function
       | [] -> ()
       | (lb, _) :: l ->
-        if Uid.Set.mem lb s then
+        if Uid.Term_set.mem lb s then
           Errors.typing_error
             (DuplicateLabel (Hstring.make @@ Uid.show lb)) loc;
-        check_duplicates (Uid.Set.add lb s) l
+        check_duplicates (Uid.Term_set.add lb s) l
     in
-    check_duplicates Uid.Set.empty lbs;
+    check_duplicates Uid.Term_set.empty lbs;
     match ty with
     | Ty.Trecord { Ty.lbs = l; _ } ->
       if List.length lbs <> List.length l then
@@ -586,32 +586,34 @@ let check_no_duplicates =
 let filter_patterns pats ty_body _loc =
   let cases =
     List.fold_left
-      (fun s {Ty.constr=c; _} -> Uid.Set.add c s) Uid.Set.empty ty_body
+      (fun s {Ty.constr=c; _} -> Uid.Term_set.add c s)
+      Uid.Term_set.empty ty_body
   in
   let missing, filtered_pats, dead =
     List.fold_left
       (fun (miss, filtered_pats, dead) ((p, _) as u) ->
          match p with
          | Constr { name; _ } ->
-           assert (Uid.Set.mem name cases); (* pattern is well typed *)
-           if Uid.Set.mem name miss then (* not encountered yet *)
-             Uid.Set.remove name miss, u :: filtered_pats, dead
+           assert (Uid.Term_set.mem name cases); (* pattern is well typed *)
+           if Uid.Term_set.mem name miss then (* not encountered yet *)
+             Uid.Term_set.remove name miss, u :: filtered_pats, dead
            else (* case already seen --> dead pattern *)
              miss, pats, p :: dead
          | Var _ ->
-           if Uid.Set.is_empty miss then
+           if Uid.Term_set.is_empty miss then
              (* match already exhaussive -> dead case *)
              miss, filtered_pats, p :: dead
            else (* covers all remaining cases, miss becomes empty *)
-             Uid.Set.empty, u :: filtered_pats, dead
+             Uid.Term_set.empty, u :: filtered_pats, dead
       )(cases, [], []) pats
   in
   missing, List.rev filtered_pats, dead
 
 let check_pattern_matching missing dead loc =
-  if not (Uid.Set.is_empty missing) then begin
+  if not (Uid.Term_set.is_empty missing) then begin
     let missing =
-      List.map (fun m -> Hstring.make @@ Uid.show m) (Uid.Set.elements missing)
+      List.map (fun m -> Hstring.make @@ Uid.show m)
+        (Uid.Term_set.elements missing)
     in
     Errors.typing_error (MatchNotExhaustive missing) loc end;
   if dead != [] then
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 834ea2ce31..8ce4dad0ac 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -28,12 +28,17 @@
 module Sy = Symbols
 module E  = Expr
 
+
 type 'a abstract =
-  | Constr of { c_name : Uid.t ; c_ty : Ty.t ; c_args : (Uid.t * 'a) list }
+  | Constr of {
+      c_name : Uid.term_cst;
+      c_ty : Ty.t;
+      c_args : (Uid.term_cst * 'a) list
+    }
   (* [Cons { c_name; c_ty; c_args }] reprensents the application of the
      constructor [c_name] of the ADT [ty] with the arguments [c_args]. *)
 
-  | Select of { d_name : Uid.t ; d_ty : Ty.t ; d_arg : 'a }
+  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
   (* [Select { d_name; d_ty; d_arg }] represents the destructor [d_name] of
      the ADT [d_ty] on the ADT value [d_arg]. *)
 
diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli
index b90e978db4..81d7267b5d 100644
--- a/src/lib/reasoners/adt.mli
+++ b/src/lib/reasoners/adt.mli
@@ -26,9 +26,13 @@
 (**************************************************************************)
 
 type 'a abstract =
-  | Constr of
-      { c_name : Uid.t ; c_ty : Ty.t ; c_args : (Uid.t * 'a) list }
-  | Select of { d_name : Uid.t ; d_ty : Ty.t ; d_arg : 'a }
+  | Constr of {
+      c_name : Uid.term_cst;
+      c_ty : Ty.t;
+      c_args : (Uid.term_cst * 'a) list
+    }
+
+  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
 
   | Alien of 'a
 
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 213c1523d1..37f47af9fb 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -43,7 +43,7 @@ module B = Dolmen.Std.Builtin
 module TSet =
   Set.Make
     (struct
-      type t = Uid.t
+      type t = Uid.term_cst
 
       (* We use a dedicated total order on the constructors to ensure
          the termination of model generation. *)
@@ -616,7 +616,7 @@ let constr_of_destr ty d =
 
   | _ -> assert false
 
-exception Found of X.r * Uid.t
+exception Found of X.r * Uid.term_cst
 
 let can_split env n =
   let m = Options.get_max_split () in
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index e5d354e2a7..350d42420c 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -29,8 +29,8 @@ module E = Expr
 module Sy = Symbols
 
 type 'a abstract =
-  | Record of (Uid.t * 'a abstract) list * Ty.t
-  | Access of Uid.t * 'a abstract * Ty.t
+  | Record of (Uid.term_cst * 'a abstract) list * Ty.t
+  | Access of Uid.term_cst * 'a abstract * Ty.t
   | Other of 'a * Ty.t
 
 module type ALIEN = sig
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index c490ed23a8..0c4351e053 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -160,25 +160,25 @@ module Main_Default : S = struct
            | Tvar _ -> assert false
 
            | Text (_, hs) | Trecord { name = hs; _ } when
-               Uid.Map.mem hs mp -> mp
+               Uid.Ty_map.mem hs mp -> mp
 
            | Text (l, hs) ->
              let l = List.map (fun _ -> Ty.fresh_tvar()) l in
-             Uid.Map.add hs (Text(l, hs)) mp
+             Uid.Ty_map.add hs (Text(l, hs)) mp
 
            | Trecord { name; _ } ->
              (* cannot do better for records ? *)
-             Uid.Map.add name ty mp
+             Uid.Ty_map.add name ty mp
 
            | Tadt (hs, _) ->
              (* cannot do better for ADT ? *)
-             Uid.Map.add hs ty mp
-        )sty Uid.Map.empty
+             Uid.Ty_map.add hs ty mp
+        )sty Uid.Ty_map.empty
 
     let print_types_decls ?(header=true) types =
       let open Ty in
       print_dbg ~flushed:false ~header "@[<v 2>(* types decls: *)@ ";
-      Uid.Map.iter
+      Uid.Ty_map.iter
         (fun _ ty ->
            match ty with
            | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> ()
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index a63ff116a1..87d4458f85 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -280,8 +280,8 @@ val mk_ite : t -> t -> t -> t
 
 (** smart constructor for datatypes. *)
 
-val mk_constr : Uid.t -> t list -> Ty.t -> t
-val mk_tester : Uid.t -> t -> t
+val mk_constr : Uid.term_cst -> t list -> Ty.t -> t
+val mk_tester : Uid.term_cst -> t -> t
 val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index 754839ae8f..01a957f29f 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -101,7 +101,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let body =
     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
+  let ty = Ty.t_adt ~body:(Some body) (Uid.of_ty_cst ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 7c99a2c0be..4f8671c09c 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -27,7 +27,7 @@
 
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.t (* ADT tester *)
+  | IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +35,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.t | Record
-  | Constr of Uid.t (* enums, adts *)
-  | Destruct of Uid.t
+  | Access of Uid.term_cst | Record
+  | Constr of Uid.term_cst (* enums, adts *)
+  | Destruct of Uid.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index bcf0af48a8..322a3a9354 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -27,7 +27,7 @@
 
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.t (* ADT tester *)
+  | IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +35,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.t | Record
-  | Constr of Uid.t (* enums, adts *)
-  | Destruct of Uid.t
+  | Access of Uid.term_cst | Record
+  | Constr of Uid.term_cst (* enums, adts *)
+  | Destruct of Uid.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
@@ -163,8 +163,8 @@ val var : Var.t -> t
 val int : string -> t
 val bitv : string -> t
 val real : string -> t
-val constr : Uid.t -> t
-val destruct : Uid.t -> t
+val constr : Uid.term_cst -> t
+val destruct : Uid.term_cst -> t
 val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound
 val mk_in : bound -> bound -> t
 val mk_maps_to : Var.t -> t
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 39424257f8..ecd46eb50d 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -31,17 +31,18 @@ type t =
   | Tbool
   | Tvar of tvar
   | Tbitv of int
-  | Text of t list * Uid.t
+  | Text of t list * Uid.ty_cst
   | Tfarray of t * t
-  | Tadt of Uid.t * t list
+  | Tadt of Uid.ty_cst * t list
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
+
 and trecord = {
   mutable args : t list;
-  name : Uid.t;
-  mutable lbs :  (Uid.t * t) list;
-  record_constr : Uid.t; (* for ADTs that become records. default is "{" *)
+  name : Uid.ty_cst;
+  mutable lbs :  (Uid.term_cst * t) list;
+  record_constr : Uid.term_cst; (* for ADTs that become records. default is "{" *)
 }
 
 module Smtlib = struct
@@ -67,8 +68,8 @@ exception TypeClash of t*t
 exception Shorten of t
 
 type adt_constr =
-  { constr : Uid.t ;
-    destrs : (Uid.t * t) list }
+  { constr : Uid.term_cst ;
+    destrs : (Uid.term_cst * t) list }
 
 type type_body = adt_constr list
 
@@ -405,7 +406,7 @@ and fresh_list lty subst =
 
 module Decls = struct
 
-  module MH = Uid.Map
+  module MH = Uid.Ty_map
 
   module MTY = Map.Make(struct
       type ty = t
@@ -510,7 +511,7 @@ let fresh_empty_text =
       let path = DStd.Path.global @@ Fmt.str "'_c%d" !cpt in
       DStd.Expr.Ty.Const.mk path 0
     in
-    text [] (Uid.of_dolmen id)
+    text [] (Uid.of_ty_cst id)
 
 let t_adt ?(body=None) s ty_vars =
   let ty = Tadt (s, ty_vars) in
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 43b7b8ddd9..d636faff99 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -42,7 +42,7 @@ type t =
   (** Type variables *)
   | Tbitv of int
   (** Bitvectors of a given length *)
-  | Text of t list * Uid.t
+  | Text of t list * Uid.ty_cst
   (** Abstract types applied to arguments. [Text (args, s)] is
       the application of the abstract type constructor [s] to
       arguments [args]. *)
@@ -51,7 +51,7 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.t * t list
+  | Tadt of Uid.ty_cst * t list
   (** Application of algebraic data types. [Tadt (a, params)] denotes
       the application of the polymorphic datatype [a] to the types parameters
       [params].
@@ -77,22 +77,22 @@ and tvar = {
 and trecord = {
   mutable args : t list;
   (** Arguments passed to the record constructor *)
-  name : Uid.t;
+  name : Uid.ty_cst;
   (** Name of the record type *)
-  mutable lbs :  (Uid.t * t) list;
+  mutable lbs :  (Uid.term_cst * t) list;
   (** List of fields of the record. Each field has a name,
       and an associated type. *)
-  record_constr : Uid.t;
+  record_constr : Uid.term_cst;
   (** record constructor. Useful is case it's a specialization of an
       algeberaic datatype. Default value is "\{__[name]" *)
 }
 (** Record types. *)
 
 type adt_constr =
-  { constr : Uid.t ;
+  { constr : Uid.term_cst ;
     (** constructor of an ADT type *)
 
-    destrs : (Uid.t * t) list
+    destrs : (Uid.term_cst * t) list
     (** the list of destructors associated with the constructor and
         their respective types *)
   }
@@ -109,12 +109,12 @@ module Set : Set.S with type elt = t
 (** Sets of types *)
 
 
-val assoc_destrs : Uid.t -> adt_constr list -> (Uid.t * t) list
+val assoc_destrs : Uid.term_cst -> adt_constr list -> (Uid.term_cst * t) list
 (** [assoc_destrs cons cases] returns the list of destructors associated with
     the constructor [cons] in the ADT defined by [cases].
     @raises Not_found if the constructor is not in the given list. *)
 
-val type_body : Uid.t -> t list -> type_body
+val type_body : Uid.ty_cst -> t list -> type_body
 
 (** {2 Type inspection} *)
 
@@ -160,12 +160,13 @@ val fresh_tvar : unit -> t
 val fresh_empty_text : unit -> t
 (** Return a fesh abstract type. *)
 
-val text : t list -> Uid.t -> t
+val text : t list -> Uid.ty_cst -> t
 (** Apply the abstract type constructor to the list of type arguments
     given. *)
 
 val t_adt :
-  ?body:((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
+  ?body:((Uid.term_cst * (Uid.term_cst * t) list) list) option ->
+  Uid.ty_cst -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
     its destructors with their respective types. If [body] is none,
@@ -175,7 +176,8 @@ val t_adt :
 
 val trecord :
   ?sort_fields:bool ->
-  record_constr:Uid.t -> t list -> Uid.t -> (Uid.t * t) list -> t
+  record_constr:Uid.term_cst ->
+  t list -> Uid.ty_cst -> (Uid.term_cst * t) list -> t
 (** Create a record type. [trecord args name lbs] creates a record
     type with name [name], arguments [args] and fields [lbs].
 
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index 7c495adce1..0c4fa051ef 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -52,7 +52,7 @@ type oplogic =
 
 (** type of pattern in match construct of ADTs *)
 type pattern =
-  | Constr of { name : Uid.t ; args : (Var.t * Uid.t * Ty.t) list}
+  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
   (** A pattern case which is a constructor. [name] is the name of
       constructor. [args] contains the variables bound by this pattern
       with their correponsing destructors and types *)
diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli
index b051c45cf3..281afdab27 100644
--- a/src/lib/structures/typed.mli
+++ b/src/lib/structures/typed.mli
@@ -72,7 +72,7 @@ type oplogic =
 (** Logic operators. *)
 
 type pattern =
-  | Constr of { name : Uid.t ; args : (Var.t * Uid.t * Ty.t) list}
+  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
   | Var of Var.t
 
 
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index 0d594d0393..a651606d1d 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -28,15 +28,19 @@
 module DStd = Dolmen.Std
 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 _ t =
+  | Hstring : Hstring.t -> 'a t
+  | Term_cst : DE.term_cst -> DE.term_cst t
+  | Ty_cst : DE.ty_cst -> DE.ty_cst t
+  | Ty_var : DE.ty_var -> DE.ty_var t
+
+type term_cst = DE.term_cst t
+type ty_cst = DE.ty_cst t
+type ty_var = DE.ty_var t
 
-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_ty_var id = Ty_var id
 let[@inline always] of_hstring hs = Hstring hs
 let[@inline always] of_string s = of_hstring @@ Hstring.make s
 
@@ -45,34 +49,36 @@ let[@inline always] to_term_cst id =
   | Term_cst t -> t
   | _ -> invalid_arg "to_term_cst"
 
-let hash = function
+let hash (type a) (u : a t) =
+  match u with
   | 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
+  | Ty_var id -> DE.Id.hash id
 
-let pp ppf = function
+let pp (type a) ppf (u : a t) =
+  match u with
   | 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
+  | Ty_var id -> DE.Id.print ppf id
 
-let show = Fmt.to_to_string pp
+let show (type a) (u : a t) = Fmt.to_to_string pp u
 
-let equal u1 u2 =
+let equal (type a b) (u1 : a t) (u2 : b t) =
   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
+  | Ty_var id1, Ty_var id2 -> DE.Id.equal id1 id2
   | _ -> String.equal (show u1) (show u2)
 
-let compare u1 u2 =
+let compare (type a b) (u1 : a t) (u2 : b t) =
   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
+  | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2
   | _ -> String.compare (show u1) (show u2)
 
 let order_tag : int DStd.Tag.t = DStd.Tag.create ()
@@ -83,16 +89,16 @@ let perfect_hash id =
     Option.get @@ DE.Term.Const.get_tag id order_tag
   | Hstring hs ->
     Hstring.hash hs
-  | _ -> assert false
+  | _ -> .
 
-module Set = Set.Make
+module Term_set = Set.Make
     (struct
-      type nonrec t = t
+      type nonrec t = term_cst
       let compare = compare
     end)
 
-module Map = Map.Make
+module Ty_map = Map.Make
     (struct
-      type nonrec t = t
+      type nonrec t = ty_cst
       let compare = compare
     end)
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index 45553fcf12..7d4a64d191 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -27,30 +27,34 @@
 
 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 _ t = private
+  | Hstring : Hstring.t -> 'a t
+  | Term_cst : DE.term_cst -> DE.term_cst t
+  | Ty_cst : DE.ty_cst -> DE.ty_cst t
+  | Ty_var : DE.ty_var -> DE.ty_var t
 
-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
+type term_cst = DE.term_cst t
+type ty_cst = DE.ty_cst t
+type ty_var = DE.ty_var t
 
-val to_term_cst : t -> DE.term_cst
+val of_term_cst : DE.term_cst -> term_cst
+val of_ty_cst : DE.ty_cst -> ty_cst
+val of_ty_var : DE.ty_var -> ty_var
+val of_string : string -> 'a t
+val of_hstring : Hstring.t -> 'a t
+
+val to_term_cst : term_cst -> DE.term_cst
 
 val order_tag : int Dolmen.Std.Tag.t
 (** Tag used to attach the order of constructor. Used to
     retrieve efficiency the order of the constructor in [to_int]. *)
 
-val perfect_hash : t -> int
-val hash : t -> int
-val pp : t Fmt.t
-val show : t -> string
-val equal : t -> t -> bool
-val compare : t -> t -> int
+val perfect_hash : term_cst -> int
+val hash : 'a t -> int
+val pp : 'a t Fmt.t
+val show : 'a t -> string
+val equal : 'a t -> 'a t -> bool
+val compare : 'a t -> 'a t -> int
 
-module Set : Set.S with type elt = t
-module Map : Map.S with type key = t
+module Term_set : Set.S with type elt = term_cst
+module Ty_map : Map.S with type key = ty_cst
diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml
index 5862e5b685..d7f016445b 100644
--- a/src/lib/structures/xliteral.ml
+++ b/src/lib/structures/xliteral.ml
@@ -27,7 +27,7 @@
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.t (* ADT tester *)
+    IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view =
diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli
index 7f83f90b20..bd60c345a4 100644
--- a/src/lib/structures/xliteral.mli
+++ b/src/lib/structures/xliteral.mli
@@ -27,7 +27,7 @@
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.t (* ADT tester *)
+    IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view = (*private*)

From 30e71411e192fbdd8728bc22f378ec6d77e11a8d Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 10 Jul 2024 14:51:40 +0200
Subject: [PATCH 5/8] Do not expose the order tag

---
 src/lib/reasoners/adt_rel.ml |  2 +-
 src/lib/structures/uid.ml    | 10 ----------
 src/lib/structures/uid.mli   |  5 -----
 src/lib/util/nest.ml         | 14 +++++++++++++-
 src/lib/util/nest.mli        |  2 ++
 5 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 37f47af9fb..ff30c40264 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -48,7 +48,7 @@ module TSet =
       (* We use a dedicated total order on the constructors to ensure
          the termination of model generation. *)
       let compare id1 id2 =
-        Uid.perfect_hash id1 - Uid.perfect_hash id2
+        Nest.perfect_hash id1 - Nest.perfect_hash id2
     end)
 
 let timer = Timers.M_Adt
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index a651606d1d..cbd2fa3ae6 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -81,16 +81,6 @@ let compare (type a b) (u1 : a t) (u2 : b t) =
   | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2
   | _ -> String.compare (show u1) (show u2)
 
-let order_tag : int DStd.Tag.t = DStd.Tag.create ()
-
-let perfect_hash id =
-  match id with
-  | Term_cst id ->
-    Option.get @@ DE.Term.Const.get_tag id order_tag
-  | Hstring hs ->
-    Hstring.hash hs
-  | _ -> .
-
 module Term_set = Set.Make
     (struct
       type nonrec t = term_cst
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index 7d4a64d191..e500dfcb48 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -45,11 +45,6 @@ val of_hstring : Hstring.t -> 'a t
 
 val to_term_cst : term_cst -> DE.term_cst
 
-val order_tag : int Dolmen.Std.Tag.t
-(** Tag used to attach the order of constructor. Used to
-    retrieve efficiency the order of the constructor in [to_int]. *)
-
-val perfect_hash : term_cst -> int
 val hash : 'a t -> int
 val pp : 'a t Fmt.t
 val show : 'a t -> string
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
index fa80dfbc20..b0cbf951c6 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -153,6 +153,10 @@ let ty_cst_of_cstr DE.{ builtin; _ } =
   | B.Constructor { adt; _ } -> adt
   | _ -> Fmt.failwith "expect an ADT constructor"
 
+(** 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 ()
+
 let attach_orders defs =
   let hp = build_graph defs in
   let r : (int * DE.term_cst list) H.t = H.create 17 in
@@ -162,7 +166,7 @@ let attach_orders defs =
     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 Uid.order_tag o;
+    DE.Term.Const.set_tag id order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -173,3 +177,11 @@ let attach_orders defs =
       ) !outgoing;
     outgoing := [];
   done
+
+let perfect_hash id =
+  match (id : _ Uid.t) with
+  | Term_cst id ->
+    Option.get @@ DE.Term.Const.get_tag id order_tag
+  | Hstring hs ->
+    Hstring.hash hs
+  | _ -> .
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index a466903f38..998a7c2558 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -35,3 +35,5 @@ val attach_orders : DE.ty_def list -> unit
     {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. *)
+
+val perfect_hash : Uid.term_cst -> int

From 02d9834cc9ccd267482597c7768bf2eedcaaa6e4 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 10 Jul 2024 15:40:35 +0200
Subject: [PATCH 6/8] Add an assertion in `of_term_cst`

---
 src/lib/frontend/d_cnf.ml  | 24 ++++++++++++------------
 src/lib/structures/uid.ml  | 26 ++++++++++++++++++++------
 src/lib/structures/uid.mli |  5 +++--
 src/lib/util/nest.ml       | 17 ++++++++++-------
 src/lib/util/nest.mli      |  5 +++++
 5 files changed, 50 insertions(+), 27 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index eff26b99d0..3f000139bd 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -101,22 +101,20 @@ module Cache = struct
   let find_ty id =
     HT.find ae_ty_ht (Id id)
 
-  let fresh_ty ?(is_var = true) ?id () =
+  let fresh_ty ?(is_var = true) ?(name = None) () =
     if is_var
     then Ty.fresh_tvar ()
     else
-      match id with
-      | Some id -> Ty.text [] (Uid.of_string id)
+      match name with
+      | Some n -> Ty.text [] (Uid.of_string n)
       | None -> Ty.fresh_empty_text ()
 
-  let show (type a) (id : a DE.id) = Fmt.to_to_string DE.Id.print id
-
-  let update_ty_store ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id:(show id) () in
+  let update_ty_store ?(is_var = true) ?name id =
+    let ty = fresh_ty ~is_var ~name () in
     store_ty id ty
 
-  let update_ty_store_ret ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id:(show id) () in
+  let update_ty_store_ret ?(is_var = true) ?name id =
+    let ty = fresh_ty ~is_var ~name () in
     store_ty id ty;
     ty
 
@@ -127,7 +125,8 @@ module Cache = struct
       update_ty_store_ret ~is_var id
 
   let store_tyv ?(is_var = true) t_v =
-    update_ty_store ~is_var t_v
+    let name = get_basename t_v.DE.path in
+    update_ty_store ~is_var ~name t_v
 
   let store_tyvl ?(is_var = true) (tyvl: DE.ty_var list) =
     List.iter (store_tyv ~is_var) tyvl
@@ -587,10 +586,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; _ } |]; _ }
+      (Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt)
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
+    Nest.attach_orders [adt];
     let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
@@ -613,8 +613,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     Cache.store_ty ty_c ty
 
   | Some (Adt { cases; _ } as adt) ->
-    let uid = Uid.of_ty_cst ty_c in
     Nest.attach_orders [adt];
+    let uid = Uid.of_ty_cst ty_c in
     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 =
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index cbd2fa3ae6..c2647eb638 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -38,17 +38,31 @@ type term_cst = DE.term_cst t
 type ty_cst = DE.ty_cst t
 type ty_var = DE.ty_var t
 
-let[@inline always] of_term_cst id = Term_cst id
+let order_tag : int DStd.Tag.t = DStd.Tag.create ()
+
+let has_order id =
+  let is_cstr DE.{ builtin; _ } =
+    match builtin with
+    | DStd.Builtin.Constructor _ -> true
+    | _ -> false
+  in
+  let has_attached_order id =
+    DE.Term.Const.get_tag id order_tag |> Option.is_some
+  in
+  (not (is_cstr id)) || has_attached_order id
+
+let[@inline always] of_term_cst id =
+  (* This assertion ensures that the API of the [Nest] module have been
+     correctly used, that is [Nest.attach_orders] have been called on
+     the nest of [id] if [id] is a constructor of ADT. *)
+  if not @@ has_order id then Fmt.failwith "not order on %a" DE.Id.print id;
+  Term_cst id
+
 let[@inline always] of_ty_cst id = Ty_cst id
 let[@inline always] of_ty_var id = Ty_var 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 (type a) (u : a t) =
   match u with
   | Hstring hs -> Hstring.hash hs
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index e500dfcb48..11d6570ed4 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -43,13 +43,14 @@ val of_ty_var : DE.ty_var -> ty_var
 val of_string : string -> 'a t
 val of_hstring : Hstring.t -> 'a t
 
-val to_term_cst : term_cst -> DE.term_cst
-
 val hash : 'a t -> int
 val pp : 'a t Fmt.t
 val show : 'a t -> string
 val equal : 'a t -> 'a t -> bool
 val compare : 'a t -> 'a t -> int
 
+val order_tag : int Dolmen.Std.Tag.t
+(** Tag used to attach the order of constructor. *)
+
 module Term_set : Set.S with type elt = term_cst
 module Ty_map : Map.S with type key = ty_cst
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
index b0cbf951c6..d497553ea1 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -153,10 +153,6 @@ let ty_cst_of_cstr DE.{ builtin; _ } =
   | B.Constructor { adt; _ } -> adt
   | _ -> Fmt.failwith "expect an ADT constructor"
 
-(** 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 ()
-
 let attach_orders defs =
   let hp = build_graph defs in
   let r : (int * DE.term_cst list) H.t = H.create 17 in
@@ -166,7 +162,7 @@ let attach_orders defs =
     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;
+    DE.Term.Const.set_tag id Uid.order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -180,8 +176,15 @@ let attach_orders defs =
 
 let perfect_hash id =
   match (id : _ Uid.t) with
-  | Term_cst id ->
-    Option.get @@ DE.Term.Const.get_tag id order_tag
+  | Term_cst ({ builtin = B.Constructor _; _ } as id) ->
+    begin match DE.Term.Const.get_tag id Uid.order_tag with
+      | Some h -> h
+      | None ->
+        (* Cannot occur as we eliminate this case in the smart constructor
+           [Uid.of_term_cst]. *)
+        assert false
+    end
+  | Term_cst _ -> invalid_arg "Nest.perfect_hash"
   | Hstring hs ->
     Hstring.hash hs
   | _ -> .
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index 998a7c2558..d8b30d8624 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -37,3 +37,8 @@ val attach_orders : DE.ty_def list -> unit
     mutually recursive definition of ADTs. *)
 
 val perfect_hash : Uid.term_cst -> int
+(** [perfect_hash u] returns an integer between [0] and [n] exclusive where
+    [u] is a constructor and [n] is the number of constructors of the ADT of
+    [u].
+
+    @raise Invalid_arg if [u] is not a constructor. *)

From 8951c2b2cb6333c20fb3d76bb65e0d6c6e0ab4ec Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 10 Jul 2024 16:27:54 +0200
Subject: [PATCH 7/8] linter

---
 src/lib/frontend/d_cnf.ml | 3 ++-
 src/lib/structures/ty.ml  | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 3f000139bd..3a8ba5cfd2 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -586,7 +586,8 @@ 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; _ } |]; _ } as adt)
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index ecd46eb50d..1887d3b750 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -42,7 +42,8 @@ and trecord = {
   mutable args : t list;
   name : Uid.ty_cst;
   mutable lbs :  (Uid.term_cst * t) list;
-  record_constr : Uid.term_cst; (* for ADTs that become records. default is "{" *)
+  record_constr : Uid.term_cst;
+  (* for ADTs that become records. default is "{" *)
 }
 
 module Smtlib = struct

From 2b11a43785935f65019ca2ffe307a6c32b6b4377 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 11 Jul 2024 10:16:57 +0200
Subject: [PATCH 8/8] review changes 2

---
 src/lib/frontend/d_cnf.ml          | 19 ++++++-------------
 src/lib/structures/fpa_rounding.ml |  8 ++------
 src/lib/structures/uid.ml          |  5 +++--
 3 files changed, 11 insertions(+), 21 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 3a8ba5cfd2..3fe1c22d5b 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -101,20 +101,13 @@ module Cache = struct
   let find_ty id =
     HT.find ae_ty_ht (Id id)
 
-  let fresh_ty ?(is_var = true) ?(name = None) () =
+  let fresh_ty ?(is_var = true) () =
     if is_var
     then Ty.fresh_tvar ()
-    else
-      match name with
-      | Some n -> Ty.text [] (Uid.of_string n)
-      | None -> Ty.fresh_empty_text ()
-
-  let update_ty_store ?(is_var = true) ?name id =
-    let ty = fresh_ty ~is_var ~name () in
-    store_ty id ty
+    else Ty.fresh_empty_text ()
 
-  let update_ty_store_ret ?(is_var = true) ?name id =
-    let ty = fresh_ty ~is_var ~name () in
+  let update_ty_store_ret ?(is_var = true) id =
+    let ty = fresh_ty ~is_var () in
     store_ty id ty;
     ty
 
@@ -125,8 +118,8 @@ module Cache = struct
       update_ty_store_ret ~is_var id
 
   let store_tyv ?(is_var = true) t_v =
-    let name = get_basename t_v.DE.path in
-    update_ty_store ~is_var ~name t_v
+    let ty = fresh_ty ~is_var () in
+    store_ty t_v ty
 
   let store_tyvl ?(is_var = true) (tyvl: DE.ty_var list) =
     List.iter (store_tyv ~is_var) tyvl
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index 01a957f29f..238351e99e 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -92,12 +92,8 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let cstrs =
     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 -> Nest.attach_orders [def]
-    | None -> assert false
-  in
+  let def, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  Nest.attach_orders [def];
   let body =
     List.map (fun (c, _) -> Uid.of_term_cst c, []) d_cstrs
   in
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index c2647eb638..ecb4990eac 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -40,7 +40,7 @@ type ty_var = DE.ty_var t
 
 let order_tag : int DStd.Tag.t = DStd.Tag.create ()
 
-let has_order id =
+let has_order_if_cstr id =
   let is_cstr DE.{ builtin; _ } =
     match builtin with
     | DStd.Builtin.Constructor _ -> true
@@ -55,7 +55,8 @@ let[@inline always] of_term_cst id =
   (* This assertion ensures that the API of the [Nest] module have been
      correctly used, that is [Nest.attach_orders] have been called on
      the nest of [id] if [id] is a constructor of ADT. *)
-  if not @@ has_order id then Fmt.failwith "not order on %a" DE.Id.print id;
+  if not @@ has_order_if_cstr id then
+    Fmt.invalid_arg "not order on %a" DE.Id.print id;
   Term_cst id
 
 let[@inline always] of_ty_cst id = Ty_cst id