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,10 @@ 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 tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -627,7 +626,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_cstr cstr, List.rev rev_fields) :: accl
       ) [] cases
     in
     let body = Some (List.rev rev_cs) in
@@ -704,7 +703,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_cstr cstr, List.rev rev_fields) :: accl
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
@@ -811,10 +810,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_cstr cst; args}
 
   | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = Uid.of_dolmen cst; args = []}
+    Typed.Constr {name = Uid.of_cstr cst; args = []}
 
   | Var ({ builtin = B.Base; path; _ } as t_v) ->
     (* Should the type be passed as an argument
@@ -974,7 +973,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_cstr tcst) [] ty
               | ty ->
                 Fmt.failwith "unexpected type %a@." Ty.print ty
             end
@@ -1041,7 +1040,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_cstr cstr) in
               let ty_c =
                 match DT.definition adt with
                 | Some (
@@ -1344,9 +1343,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_cstr 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

@@ -42,7 +42,13 @@ module TSet = Set.Make
 
       (* We use a dedicated total order on the constructors to ensure
          the termination of the model generation. *)
-      let compare = Nest.compare
+      let compare id1 id2 =
+        match Uid.order id1, Uid.order id2 with
+        | Some i, Some j -> i - j
+        | None, None -> Uid.compare id1 id2
+        | _ ->
+          (* TODO: XXXXXXXXXX THIS assertion HAS TO BE REMOVED BEFORE MERGING *)
+          Fmt.failwith "id1 = %a, id2 = %a" Uid.pp id1 Uid.pp id2
     end)
 
 let timer = Timers.M_Adt

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/fpa_rounding.ml

@@ -93,8 +93,13 @@ 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 -> Nest.add_nest [def]
+    | None -> assert false
+  in
   let body =
-    List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
+    List.map (fun (c, _) -> Uid.of_cstr 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,15 @@ 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 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
+    | None -> assert false
   in
+  let name = Uid.of_dolmen DE.Ty.Const.unit in
+  let void = Uid.of_cstr DE.Term.Cstr.void in
+  let body = Some [void, []] in
+  let ty = t_adt ~body name [] in
   ty
 
 let trecord ?(sort_fields = false) ~record_constr lv name lbs =

src/lib/structures/uid.ml

@@ -25,39 +25,51 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DStd = Dolmen.Std
-module DE = DStd.Expr
+module DE = Dolmen.Std.Expr
 
 type t =
   | Hstring : Hstring.t -> t
-  | Dolmen : 'a DE.id -> t
+  | Dolmen : 'a DE.id * int option -> t
+
+let[@inline always] of_dolmen id = Dolmen (id, None)
+
+let[@inline always] of_cstr id =
+  match DE.Term.Const.get_tag id Nest.order_attr with
+  | Some i -> Dolmen (id, Some i)
+  | None ->
+    Fmt.failwith "the constructor %a has no order"
+      DE.Term.Const.print id
 
-let[@inline always] of_dolmen id = Dolmen id
 let[@inline always] of_hstring hs = Hstring hs
 let[@inline always] of_string s = of_hstring @@ Hstring.make s
 
 let hash = function
   | Hstring hs -> Hstring.hash hs
-  | Dolmen id -> DE.Id.hash id
+  | Dolmen (id, _) -> DE.Id.hash id
 
 let pp ppf = function
   | Hstring hs -> Hstring.print ppf hs
-  | Dolmen id -> DE.Id.print ppf id
+  | Dolmen (id, _) -> DE.Id.print ppf id
 
 let show = Fmt.to_to_string pp
 
 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
+  | Dolmen (id1, _), Dolmen (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
+  | Dolmen (id1, _), Dolmen (id2, _) -> DE.Id.compare id1 id2
   | _ -> String.compare (show u1) (show u2)
 
+let[@inline always] order t =
+  match t with
+  | Hstring _ -> None
+  | Dolmen (_, o) -> o
+
 module Set = Set.Make
     (struct
       type nonrec t = t

src/lib/structures/uid.mli

@@ -29,16 +29,18 @@ module DE = Dolmen.Std.Expr
 
 type t = private
   | Hstring : Hstring.t -> t
-  | Dolmen : 'a DE.id -> t
+  | Dolmen : 'a DE.id * int option -> t
 
 val of_dolmen : 'a DE.Id.t -> t
+val of_cstr : DE.term_cst -> t
 val of_string : string -> t
 val of_hstring : Hstring.t -> t
 val hash : t -> int
 val pp : t Fmt.t
 val show : t -> string
 val equal : t -> t -> bool
 val compare : t -> t -> int
+val order : t -> int option
 
 module Set : Set.S with type elt = t
 module Map : Map.S with type key = t

src/lib/util/nest.ml

@@ -21,8 +21,6 @@ module DE = DStd.Expr
 module DT = DE.Ty
 module B = Dolmen.Std.Builtin
 
-type t = Dolmen.Std.Expr.ty_def list
-
 (* A nest is the set of all the constructors of a mutually recursive definition
    of ADTs.
 
@@ -49,6 +47,8 @@ type node = {
   (* This weight is used to prioritize constructors with less destructors
      during the sorting (see [add_nest]). *)
 
+  ty : DE.ty_cst;
+
   mutable outgoing : edge;
   (* Hyperedge from a subset S in S(ty) to a subset G in G(ty) where ty is
      the type of [id]. At the beginning, we have S = S(ty) and G = G(ty).
@@ -73,6 +73,7 @@ module Hp =
         let dummy_edge : node list ref = ref [] in
         {
           id = DE.Term.Const.Int.int "0" (* dummy *);
+          ty = Obj.magic 0;
           outgoing = dummy_edge;
           in_degree = -1;
           weight = -1;
@@ -111,11 +112,12 @@ let build_graph (defs : DE.ty_def list) : Hp.t =
     (fun def ->
        match def with
        | DE.Abstract -> assert false
-       | DE.Adt { cases; _ } ->
+       | DE.Adt { cases; ty; _ } ->
          Array.iter
            (fun DE.{ cstr; dstrs; _ } ->
               let node = {
                 id = cstr;
+                ty;
                 outgoing = Hashtbl.find map def;
                 in_degree = -1; (* dummy value *)
                 weight = Array.length dstrs
@@ -139,34 +141,33 @@ 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
+let order_attr : int DStd.Tag.t = DStd.Tag.create ()
+
+module H = struct
+  include Hashtbl.Make (DE.Ty.Const)
+
+  let find t ty =
+    match find t ty with
+    | i -> i
+    | exception Not_found -> 0
+
+  let incr t ty =
+    let i = find t ty in
+    add t ty (i+1)
+end
 
 (* Sort the constructors of the nest using a sorting based on
    Kahn's algorithm. *)
 let add_nest n =
   let hp = build_graph n in
+  let orders : int 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; ty; _ } = Hp.pop_min hp in
+    let o = H.find orders ty in
+    H.incr orders ty;
+    DE.Term.Const.set_tag id order_attr o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -177,10 +178,3 @@ let add_nest n =
       ) !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

src/lib/util/nest.mli

@@ -16,8 +16,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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.
@@ -28,21 +26,10 @@ module DE = Dolmen.Std.Expr
     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
+val add_nest : Dolmen.Std.Expr.ty_def list -> 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]. *)
+val order_attr : int Dolmen.Std.Tag.t