Use Dolmen attribute to store well founded order

This PR used the well designed Dolmen to store a custom attribute on
constructors of ADT. 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.

src/lib/frontend/d_cnf.ml

@@ -585,11 +585,11 @@ and handle_ty_app ?(update = false) ty_c l =
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
   | Some (
-      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt
+      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ }
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
-    Nest.add_nest [adt];
+    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -607,12 +607,12 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     in
     let lbs = List.rev rev_lbs in
     let record_constr = Uid.of_dolmen cstr in
-    let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
+    let ty = Ty.trecord ~record_constr tyvl uid lbs in
     Cache.store_ty ty_c ty
 
   | Some (Adt { cases; _ } as adt) ->
-    Nest.add_nest [adt];
-    let uid = Uid.of_dolmen ty_c in
+    let uid = Uid.of_ty_cst ty_c in
+    List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate [adt];
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
     Cache.store_ty ty_c (Ty.t_adt uid tyvl);
     let rev_cs =
@@ -627,7 +627,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
                 | None -> assert false
             ) [] dstrs
           in
-          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+          (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
       ) [] cases
     in
     let body = Some (List.rev rev_cs) in
@@ -704,7 +704,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
                   | None -> assert false
               ) [] dstrs
             in
-            (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+            (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
@@ -729,14 +729,14 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
           assert false
     ) ([], false) tdl
   in
-  Nest.add_nest rev_tdefs;
+  List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
         | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
-          let uid = Uid.of_dolmen ty_c in
+          let uid = Uid.of_ty_cst ty_c in
           let ty =
             if (record || Array.length cases = 1) && not contains_adts
             then
@@ -811,10 +811,10 @@ let mk_pattern DE.{ term_descr; _ } =
       ) [] (List.rev rev_vnames) pargs
     in
     let args = List.rev rev_args in
-    Typed.Constr {name = Uid.of_dolmen cst; args}
+    Typed.Constr {name = Uid.of_term_cst cst; args}
 
   | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = Uid.of_dolmen cst; args = []}
+    Typed.Constr {name = Uid.of_term_cst cst; args = []}
 
   | Var ({ builtin = B.Base; path; _ } as t_v) ->
     (* Should the type be passed as an argument
@@ -974,7 +974,7 @@ let rec mk_expr
               | Trecord _ as ty ->
                 E.mk_record [] ty
               | Tadt _ as ty ->
-                E.mk_constr (Uid.of_dolmen tcst) [] ty
+                E.mk_constr (Uid.of_term_cst tcst) [] ty
               | ty ->
                 Fmt.failwith "unexpected type %a@." Ty.print ty
             end
@@ -1041,7 +1041,7 @@ let rec mk_expr
               cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _
             }, [x] ->
             begin
-              let builtin = Sy.IsConstr (Uid.of_dolmen cstr) in
+              let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in
               let ty_c =
                 match DT.definition adt with
                 | Some (
@@ -1344,9 +1344,8 @@ let rec mk_expr
             let ty = dty_to_ty term_ty in
             begin match ty with
               | Ty.Tadt _ ->
-                let sy = Sy.constr @@ Uid.of_dolmen tcst in
                 let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_term sy l ty
+                E.mk_constr (Uid.of_term_cst tcst) l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_record l ty

src/lib/reasoners/adt_rel.ml

@@ -36,48 +36,68 @@ 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;
   }
 
   exception Inconsistent of Ex.t
 
   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,38 +106,43 @@ 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]. *)
       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 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
 

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 ();

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 ();

src/lib/structures/expr.ml

@@ -1262,7 +1262,7 @@ let mk_tester cons t =
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
 let void =
-  let cstr = Uid.of_dolmen Dolmen.Std.Expr.Term.Cstr.void in
+  let cstr = Uid.of_term_cst Dolmen.Std.Expr.Term.Cstr.void in
   mk_constr cstr [] Ty.tunit
 
 (** Substitutions *)

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

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 =