review changes

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 ->

src/lib/reasoners/adt_rel.ml

@@ -39,65 +39,52 @@ 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
      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;
   }
 
   exception Inconsistent of Ex.t
 
   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,43 +93,38 @@ 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]. *)
       assert false
 
   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
 

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 =

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 =

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

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

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,35 +146,14 @@ 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; _ } =
   match builtin with
   | 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

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