Use Dolmen attribute to store well founded order

src/lib/frontend/d_cnf.ml

@@ -101,20 +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_dolmen id)
+      match name with
+      | Some n -> Ty.text [] (Uid.of_string n)
       | None -> Ty.fresh_empty_text ()
 
-  let update_ty_store ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~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 () in
+  let update_ty_store_ret ?(is_var = true) ?name id =
+    let ty = fresh_ty ~is_var ~name () in
     store_ty id ty;
     ty
 
@@ -125,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
@@ -585,19 +586,21 @@ 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. *)
-    Nest.add_nest [adt];
+    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 =
       Array.fold_left (
         fun acc c ->
           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,13 +609,13 @@ 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 ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs 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
 
   | Some (Adt { cases; _ } as adt) ->
-    Nest.add_nest [adt];
-    let uid = Uid.of_dolmen 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 =
@@ -623,11 +626,11 @@ 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
-          (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
@@ -638,7 +641,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 +681,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,11 +703,11 @@ 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
-            (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,18 +732,19 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
           assert false
     ) ([], false) tdl
   in
-  Nest.add_nest rev_tdefs;
+  Nest.attach_orders 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 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 +797,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
         | _ ->
@@ -811,10 +815,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 +978,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
@@ -1019,9 +1023,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
@@ -1041,7 +1045,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 +1330,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/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

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]. *)
 

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
 

src/lib/reasoners/adt_rel.ml

@@ -36,13 +36,19 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
-module TSet = Set.Make
+module DE = Dolmen.Std.Expr
+module DT = Dolmen.Std.Expr.Ty
+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 the model generation. *)
-      let compare = Nest.compare
+         the termination of model generation. *)
+      let compare id1 id2 =
+        Nest.perfect_hash id1 - Nest.perfect_hash id2
     end)
 
 let timer = Timers.M_Adt
@@ -77,7 +83,8 @@ module Domain = struct
     else
       { constrs; ex }
 
-  let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex }
+  let[@inline always] singleton ~ex c =
+    { constrs = TSet.singleton c; ex }
 
   let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
@@ -609,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

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

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