From 9bb31c450760af694637259e170af57f89640ad8 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 12 Apr 2024 14:30:36 +0200
Subject: [PATCH 1/7] Merge `Enum` Theory into `ADT` Theory

After refactoring both `Enum` and `ADT` theories, they shared most of
their implementation.
---
 src/lib/dune                       |   2 +-
 src/lib/frontend/d_cnf.ml          |  92 +++++---------
 src/lib/frontend/typechecker.ml    |  52 ++++----
 src/lib/reasoners/adt.ml           |   4 +-
 src/lib/reasoners/adt_rel.ml       |  70 +++++++++--
 src/lib/reasoners/enum.ml          | 189 -----------------------------
 src/lib/reasoners/enum.mli         |  38 ------
 src/lib/reasoners/enum_rel.mli     |  28 -----
 src/lib/reasoners/relation.ml      |  59 +++------
 src/lib/reasoners/shostak.ml       |  96 ++++-----------
 src/lib/reasoners/shostak.mli      |   3 -
 src/lib/reasoners/theory.ml        |  20 +--
 src/lib/structures/expr.ml         |   8 --
 src/lib/structures/fpa_rounding.ml |  15 ++-
 src/lib/structures/ty.ml           |  67 +++++-----
 src/lib/structures/ty.mli          |  14 +--
 16 files changed, 202 insertions(+), 555 deletions(-)
 delete mode 100644 src/lib/reasoners/enum.ml
 delete mode 100644 src/lib/reasoners/enum.mli
 delete mode 100644 src/lib/reasoners/enum_rel.mli

diff --git a/src/lib/dune b/src/lib/dune
index aef40ae5a6..786ffcf6b8 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -48,7 +48,7 @@
     Cnf D_cnf D_loop D_state_option Input Frontend Parsed_interface Typechecker
     Models
     ; reasoners
-    Ac Arith Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel
+    Ac Arith Arrays_rel Bitv Ccx Shostak Relation
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index fe1fff77c8..dcf6d87c90 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -546,8 +546,8 @@ and handle_ty_app ?(update = false) ty_c l =
         apply_ty_substs tysubsts tv
       )
 
-    | Tadt (hs, tyl) ->
-      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl)
+    | Tadt (hs, tyl, enum) ->
+      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl, enum)
 
     | Trecord ({ args; lbs; _ } as rcrd) ->
       Trecord {
@@ -565,7 +565,7 @@ and handle_ty_app ?(update = false) ty_c l =
   (* Recover the initial versions of the types and apply them on the provided
      type arguments stored in [tyl]. *)
   match Cache.find_ty ty_c with
-  | Tadt (hs, _) -> Tadt (hs, tyl)
+  | Tadt (hs, _, enum) -> Tadt (hs, tyl, enum)
 
   | Trecord { args; _ } as ty ->
     let tysubsts =
@@ -578,7 +578,6 @@ and handle_ty_app ?(update = false) ty_c l =
     in
     apply_ty_substs tysubsts ty
 
-  | Tsum _ as ty -> ty
   | Text (_, s) -> Text (tyl, s)
   | _ -> assert false
 
@@ -611,48 +610,30 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
     Cache.store_ty ty_c ty
 
-  | Some ((Adt { cases; _ } as adt)) ->
+  | Some (Adt { cases; _ } as adt) ->
     Nest.add_nest [adt];
     let uid = Uid.of_dolmen 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, is_enum =
       Array.fold_left (
         fun (accl, is_enum) DE.{ cstr; dstrs; _ } ->
-          let is_enum =
-            if is_enum
-            then
-              if Array.length dstrs = 0
-              then true
-              else (
-                let ty = Ty.t_adt uid tyvl in
-                Cache.store_ty ty_c ty;
-                false
-              )
-            else false
-          in
+          let is_enum = is_enum && Array.length dstrs = 0 in
           let rev_fields =
             Array.fold_left (
               fun acc tc_o ->
                 match tc_o with
-                | Some (DE.{ id_ty; _ } as id) ->
-                  (Uid.of_dolmen id, dty_to_ty id_ty) :: acc
+                | Some (DE.{ id_ty; _ } as field) ->
+                  (Uid.of_dolmen field, dty_to_ty id_ty) :: acc
                 | None -> assert false
             ) [] dstrs
           in
           (Uid.of_dolmen cstr, List.rev rev_fields) :: accl, is_enum
       ) ([], true) cases
     in
-    if is_enum
-    then
-      let cstrs =
-        List.map (fun s -> fst s) (List.rev rev_cs)
-      in
-      let ty = Ty.tsum uid cstrs in
-      Cache.store_ty ty_c ty
-    else
-      let body = Some (List.rev rev_cs) in
-      let ty = Ty.t_adt ~body uid tyvl in
-      Cache.store_ty ty_c ty
+    let body = Some (List.rev rev_cs) in
+    let ty = Ty.t_adt ~enum:is_enum ~body uid tyvl in
+    Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
     let ty_params = []
@@ -711,7 +692,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       Cache.store_ty ty_c ty
 
-    | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
+    | Tadt (hs, tyl, false), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->
@@ -728,8 +709,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
-      let args = tyl in
-      let ty = Ty.t_adt ~body hs args in
+      let ty = Ty.t_adt ~body hs tyl in
       Cache.store_ty ty_c ty
 
     | _ -> assert false
@@ -756,33 +736,23 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       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 cns, is_enum =
-            Array.fold_right (
-              fun DE.{ dstrs; cstr; _ } (nacc, is_enum) ->
-                Uid.of_dolmen cstr :: nacc,
-                Array.length dstrs = 0 && is_enum
-            ) cases ([], true)
+          let is_enum =
+            Array.fold_left (
+              fun is_enum DE.{ dstrs; _ } ->
+                is_enum && Array.length dstrs = 0
+            ) true cases
           in
+          let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
           let uid = Uid.of_dolmen ty_c in
-          if is_enum
-          then (
-            let ty = Ty.tsum uid cns in
-            Cache.store_ty ty_c ty;
-            (* If it's an enum we don't need the second iteration. *)
-            acc
-          )
-          else (
-            let ty =
-              if (record || Array.length cases = 1) && not contains_adts
-              then
-                Ty.trecord ~record_constr:uid tyvl uid []
-              else Ty.t_adt uid tyvl
-            in
-            Cache.store_ty ty_c ty;
-            (ty, Some adt) :: acc
-          )
+          let ty =
+            if (record || Array.length cases = 1) && not contains_adts
+            then
+              Ty.trecord ~record_constr:uid tyvl uid []
+            else Ty.t_adt ~enum:is_enum uid tyvl
+          in
+          Cache.store_ty ty_c ty;
+          (ty, Some adt) :: acc
+
         | Abstract ->
           assert false (* unreachable in the second iteration *)
     ) [] (List.rev rev_tdefs)
@@ -1082,9 +1052,7 @@ let rec mk_expr
               match Cache.find_ty ty_c with
               | Ty.Tadt _ ->
                 E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
-              | Ty.Tsum _ as ty ->
-                let cstr = E.mk_constr (Uid.of_dolmen cstr) [] ty in
-                E.mk_eq ~iff:false (aux_mk_expr x) cstr
+
               | Ty.Trecord _ ->
                 (* The typechecker allows only testers whose the
                    two arguments have the same type. Thus, we can always
@@ -1375,7 +1343,7 @@ let rec mk_expr
           | B.Constructor _, _ ->
             let ty = dty_to_ty term_ty in
             begin match ty with
-              | Ty.Tadt (_, _) ->
+              | 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
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 7056b933da..3bb0f2c5cb 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -69,12 +69,12 @@ module Types = struct
     match ty with
     | Ty.Text (lty', s)
     | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty') ->
+    | Ty.Tadt (s,lty',false) ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
-    | Ty.Tsum (s, _) ->
-      if List.length lty <> 0 then
+    | Ty.Tadt (s,lty',true) ->
+      if List.length lty <> 0 || List.length lty' <> 0 then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       []
     | _ -> assert false
@@ -145,13 +145,6 @@ module Types = struct
     | Abstract ->
       let ty = Ty.text ty_vars (Uid.of_string id) in
       ty, { env with to_ty = MString.add id ty env.to_ty }
-    | Enum lc ->
-      if not (Lists.is_empty ty_vars) then
-        Errors.typing_error (PolymorphicEnum id) loc;
-      let ty =
-        Ty.tsum (Uid.of_string id) (List.map Uid.of_string lc)
-      in
-      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
         List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in
@@ -171,6 +164,10 @@ module Types = struct
             from_labels =
               List.fold_left
                 (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs }
+    | Enum l ->
+      let body = List.map (fun constr -> Uid.of_string constr, []) l in
+      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
+      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Algebraic l ->
       let l = (* convert ppure_type to Ty.t in l *)
         List.map (fun (constr, l) ->
@@ -276,7 +273,9 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tsum (_, cstrs) ->
+    | Ty.Tadt (name, [], true) ->
+      let Adt cases = Ty.type_body name [] in
+      let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
         (fun m c ->
            match Fpa_rounding.translate_smt_rounding_mode
@@ -300,9 +299,12 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tsum (_, cstrs) ->
-      List.find (Uid.equal n) cstrs
-    | _ -> assert false
+    | Ty.Tadt (name, [], true) ->
+      let Adt cases = Ty.type_body name [] in
+      let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
+      List.find (fun c -> String.equal n @@ Uid.show c) cstrs
+    | _ ->
+      assert false
 
   let add_fpa_builtins env =
     let (->.) args result = { args; result } in
@@ -327,9 +329,9 @@ module Env = struct
     let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in
     let tname = Fpa_rounding.fpa_rounding_mode_ae_type_name in
     let float32 = float (int "24") (int "149") in
-    let float32d = float32 (mode (Uid.of_string nte)) in
+    let float32d = float32 (mode nte) in
     let float64 = float (int "53") (int "1074") in
-    let float64d = float64 (mode (Uid.of_string nte)) in
+    let float64d = float64 (mode nte) in
     let op n op profile =
       MString.add n @@ `Term (Symbols.Op op, profile, Other)
     in
@@ -1001,14 +1003,11 @@ let rec type_term ?(call_from_type_form=false) env f =
       let e = type_term env e in
       let ty = Ty.shorten e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
-          begin match Ty.type_body name params with
-            | Ty.Adt cases -> cases
-          end
+        | Ty.Tadt (name, params, _) ->
+          let Ty.Adt cases = Ty.type_body name params in
+          cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr; destrs = lbs}]
-        | Ty.Tsum (_,l) ->
-          List.map (fun e -> {Ty.constr = e; destrs = []}) l
         | _ -> Errors.typing_error (ShouldBeADT ty) loc
       in
       let pats =
@@ -1412,15 +1411,12 @@ and type_form ?(in_theory=false) env f =
       let e = type_term env e in
       let ty = e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
-          begin match Ty.type_body name params with
-            | Ty.Adt cases -> cases
-          end
+        | Ty.Tadt (name, params, _) ->
+          let Ty.Adt cases = Ty.type_body name params in
+          cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr ; destrs = lbs}]
 
-        | Ty.Tsum (_,l) ->
-          List.map (fun e -> {Ty.constr = e ; destrs = []}) l
         | _ ->
           Errors.typing_error (ShouldBeADT ty) f.pp_loc
       in
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index f6091d907d..34cfc922f8 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -54,7 +54,7 @@ let constr_of_destr ty dest =
       ~module_name:"Adt" ~function_name:"constr_of_destr"
       "ty = %a" Ty.print ty;
   match ty with
-  | Ty.Tadt (s, params) ->
+  | Ty.Tadt (s, params, _) ->
     begin
       let Ty.Adt cases = Ty.type_body s params in
       try
@@ -173,7 +173,7 @@ module Shostak (X : ALIEN) = struct
     in
     let xs = List.rev sx in
     match f, xs, ty with
-    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
+    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) ->
       let Ty.Adt cases = Ty.type_body name params in
       let case_hs =
         try Ty.assoc_destrs hs cases with Not_found -> assert false
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index af7d51914e..a15f656ecc 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -83,7 +83,7 @@ module Domain = struct
 
   let unknown ty =
     match ty with
-    | Ty.Tadt (name, params) ->
+    | Ty.Tadt (name, params, _) ->
       (* Return the list of all the constructors of the type of [r]. *)
       let Adt body = Ty.type_body name params in
       let constrs =
@@ -133,6 +133,9 @@ module Domains = struct
 
         We don't store domains for constructors and selectors. *)
 
+    enums: SX.t;
+    (** Set of tracked representatives of enum type. *)
+
     changed : SX.t;
     (** Representatives whose domain has changed since the last flush
         in [propagation]. *)
@@ -147,14 +150,20 @@ module Domains = struct
         )
       ppf t.domains
 
-  let empty = { domains = MX.empty; changed = SX.empty }
+  let empty = { domains = MX.empty; enums = SX.empty; changed = SX.empty }
 
   let filter_ty = is_adt_ty
 
+  let is_enum r =
+    match X.type_info r with
+    | Ty.Tadt (_, [], true) -> true
+    | _ -> false
+
   let internal_update r nd t =
     let domains = MX.add r nd t.domains in
+    let enums = if is_enum r then SX.add r t.enums else t.enums in
     let changed = SX.add r t.changed in
-    { domains; changed }
+    { domains; enums; changed }
 
   let get r t =
     match Th.embed r with
@@ -170,9 +179,9 @@ module Domains = struct
   let add r t =
     match Th.embed r with
     | Alien _ when not (MX.mem r t.domains) ->
-      (* We have to add a default domain if the key `r` isn't in map in order
-          to be sure that the case-split mechanism will attempt to choose a
-          value for it. *)
+      (* We have to add a default domain if the key `r` is not in map in order
+         to be sure that the case split mechanism will attempt to choose a
+         value for it. *)
       let nd = Domain.unknown (X.type_info r) in
       internal_update r nd t
     | Alien _ | Constr _ | Select _ -> t
@@ -192,8 +201,9 @@ module Domains = struct
 
   let remove r t =
     let domains = MX.remove r t.domains in
+    let enums = SX.remove r t.enums in
     let changed = SX.remove r t.changed in
-    { domains ; changed }
+    { domains; enums; changed }
 
   exception Inconsistent = Domain.Inconsistent
 
@@ -227,6 +237,8 @@ module Domains = struct
     acc, { t with changed = SX.empty }
 
   let fold f t = MX.fold f t.domains
+
+  let fold_enums f t = SX.fold f t.enums
 end
 
 let calc_destructor d e uf =
@@ -342,7 +354,7 @@ let assume_th_elt t th_elt _ =
 (* Update the domains of the semantic values [r1] and [r2] according to the
    disequality [r1 <> r2].
 
-   This function alone isn't sufficient to produce a complete decision
+   This function alone is not sufficient to produce a complete decision
    procedure for the ADT theory. For instance, let's assume we have three
    semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's
    clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough
@@ -428,7 +440,7 @@ let assume_literals la uf domains =
          let rr1, ex1 = Uf.find_r uf r1 in
          let rr2, ex2 = Uf.find_r uf r2 in
          (* The explanation [ex] explains why [r1] and [r2] are distinct,
-            which isn't sufficient to justify why [rr1] and [rr2] are
+            which is not sufficient to justify why [rr1] and [rr2] are
             distinct. *)
          let ex = Ex.union ex1 @@ Ex.union ex2 ex in
          (* Needed for models generation because fresh terms are not added with
@@ -465,7 +477,7 @@ let build_constr_eq r c =
   match Th.embed r with
   | Alien r ->
     begin match X.type_info r with
-      | Ty.Tadt (name, params) as ty ->
+      | Ty.Tadt (name, params, _) as ty ->
         let Ty.Adt body = Ty.type_body name params in
         let ds =
           try Ty.assoc_destrs c body with Not_found -> assert false
@@ -566,7 +578,7 @@ let two = Numbers.Q.from_int 2
 (* TODO: we should compute this reverse map in `Ty` and store it there. *)
 let constr_of_destr ty d =
   match ty with
-  | Ty.Tadt (name, params) ->
+  | Ty.Tadt (name, params, _) ->
     begin
       let Ty.Adt cases = Ty.type_body name params in
       try
@@ -584,6 +596,11 @@ let constr_of_destr ty d =
 
 exception Found of X.r * Uid.t
 
+let can_split env n =
+  let m = Options.get_max_split () in
+  Numbers.Q.(compare (mult n env.size_splits) m) <= 0
+  || Numbers.Q.sign m < 0
+
 let (let*) = Option.bind
 
 (* Do a cases-plit by choosing a semantic value [r] and constructor [c]
@@ -622,6 +639,32 @@ let pick_best ds =
   in
   Some (r, c)
 
+let pick_enum ds uf =
+  Domains.fold_enums
+    (fun r best ->
+       let rr, _ = Uf.find_r uf r in
+       let d = Domains.get r ds in
+       let cd = Domain.cardinal d in
+       match Th.embed rr, best with
+       | Constr _, _ -> best
+       | _, Some (n, _, _) when n <= cd -> best
+       | _ ->
+         let c = Domain.choose d in
+         Some (cd, r, c)
+    ) ds None
+
+let split_enum env uf =
+  let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
+  let* n, r, c = pick_enum ds uf in
+  let n = Numbers.Q.from_int n in
+  if can_split env n then
+    let _, cons = Option.get @@ build_constr_eq r c in
+    let nr, ctx = X.make cons in
+    assert (Lists.is_empty ctx);
+    Some (LR.mkv_eq r nr)
+  else
+    None
+
 let split_best_domain ~for_model uf =
   if not for_model then
     None
@@ -640,7 +683,10 @@ let split_best_domain ~for_model uf =
 let next_case_split ~for_model env uf =
   match split_delayed_destructor env with
   | Some _ as r -> r
-  | None -> split_best_domain ~for_model uf
+  | None ->
+    match split_enum env uf with
+    | Some _ as r -> r
+    | None -> split_best_domain ~for_model uf
 
 let case_split env uf ~for_model =
   if Options.get_disable_adts () then
diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml
deleted file mode 100644
index 5b1bc45dcd..0000000000
--- a/src/lib/reasoners/enum.ml
+++ /dev/null
@@ -1,189 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-2024 --- OCamlPro SAS                           *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-module Sy = Symbols
-module E  = Expr
-
-type 'a abstract =
-  | Cons of Uid.t * Ty.t
-  (* [Cons(hs, ty)] represents a constructor of an enum type of type [ty]. *)
-
-  | Alien of 'a
-  (* [Alien r] represents a uninterpreted enum semantic value. *)
-
-module type ALIEN = sig
-  include Sig.X
-  val embed : r abstract -> r
-  val extract : r -> (r abstract) option
-end
-
-module Shostak (X : ALIEN) = struct
-
-  type t = X.r abstract
-  type r = X.r
-
-  let name = "Sum"
-
-  let timer = Timers.M_Sum
-
-  let is_mine_symb sy ty =
-    match sy, ty with
-    | Sy.Op (Sy.Constr _), Ty.Tsum _ -> true
-    | _ -> false
-
-  let fully_interpreted _ = true
-
-  let type_info = function
-    | Cons (_, ty) -> ty
-    | Alien x -> X.type_info x
-
-  let color _ = assert false
-
-
-  (*BISECT-IGNORE-BEGIN*)
-  module Debug = struct
-    open Printer
-
-    let print fmt = function
-      | Cons (hs,_) -> Format.fprintf fmt "%a" Uid.pp hs
-      | Alien x -> Format.fprintf fmt "%a" X.print x
-
-    let solve_bis a b =
-      if Options.get_debug_sum () then
-        print_dbg
-          ~module_name:"Enum" ~function_name:"solve"
-          "@[<v 2>we solve %a = %a@ " X.print a X.print b
-
-    let solve_bis_result res =
-      if Options.get_debug_sum () then
-        match res with
-        | [p,v] ->
-          print_dbg ~header:false
-            "we get: %a |-> %a@]" X.print p X.print v
-        | []    ->
-          print_dbg ~header:false
-            "the equation is trivial"
-        | _ -> assert false
-
-    let solve_bis_unsolvable () =
-      if Options.get_debug_sum () then
-        print_dbg
-          "the equation is unsolvable@]"
-
-  end
-  (*BISECT-IGNORE-END*)
-
-  let print = Debug.print
-
-  let embed r =
-    match X.extract r with
-    | Some c -> c
-    | None -> Alien r
-
-  let is_mine = function
-    | Alien r -> r
-    | Cons _ as c -> X.embed c
-
-  let compare_mine c1 c2 =
-    match c1 , c2 with
-    | Cons (h1,ty1) , Cons (h2,ty2)  ->
-      let n = Uid.compare h1 h2 in
-      if n <> 0 then n else Ty.compare ty1 ty2
-    | Alien r1, Alien r2 -> X.str_cmp r1 r2
-    | Alien _ , Cons _   -> 1
-    | Cons _  , Alien _  -> -1
-
-  let compare x y = compare_mine (embed x) (embed y)
-
-  let equal s1 s2 = match s1, s2 with
-    | Cons (h1,ty1) , Cons (h2,ty2)  -> Uid.equal h1 h2 && Ty.equal ty1 ty2
-    | Alien r1, Alien r2 -> X.equal r1 r2
-    | Alien _ , Cons _  | Cons _  , Alien _  -> false
-
-  let hash = function
-    | Cons (h, ty) -> Uid.hash h + 19 * Ty.hash ty
-    | Alien r -> X.hash r
-
-  let leaves _ = []
-
-  let is_constant _ = true
-
-  let subst p v c =
-    let cr = is_mine c in
-    if X.equal p cr then v
-    else
-      match c with
-      | Cons _ -> cr
-      | Alien r -> X.subst p v r
-
-  let make t = match E.term_view t with
-    | { E.f = Sy.Op (Sy.Constr hs); xs = []; ty; _ } ->
-      is_mine (Cons(hs,ty)), []
-    | _ ->
-      Printer.print_err
-        "Enum theory only expect constructors with no arguments; got %a."
-        E.print t;
-      assert false
-
-  let solve a b =
-    match embed a, embed b with
-    | Cons(c1,_) , Cons(c2,_) when Uid.equal c1 c2 -> []
-    | Cons(_,_) , Cons(_,_) -> raise Util.Unsolvable
-    | Cons _     , Alien r2   -> [r2,a]
-    | Alien r1   , Cons _     -> [r1,b]
-    | Alien _    , Alien _    ->
-      if X.str_cmp a b > 0 then [a,b] else [b,a]
-
-  let solve_bis a b =
-    Debug.solve_bis a b;
-    try
-      let res = solve a b in
-      Debug.solve_bis_result res;
-      res
-    with Util.Unsolvable ->
-      Debug.solve_bis_unsolvable ();
-      raise Util.Unsolvable
-
-  let abstract_selectors v acc = is_mine v, acc
-
-  let term_extract _ = None, false
-
-  let solve r1 r2 pb =
-    Sig.{pb with sbt = List.rev_append (solve_bis r1 r2) pb.sbt}
-
-  let assign_value _ _ _ =
-    (* As the models of this theory are finite, the case-split
-       mechanism can and does exhaust all the possible values.
-       Thus we don't need to guess new values here. *)
-    None
-
-  let to_model_term r =
-    match embed r with
-    | Cons (hs, ty) ->
-      Some (E.mk_term Sy.(Op (Constr hs)) [] ty)
-    | Alien a -> X.to_model_term a
-end
diff --git a/src/lib/reasoners/enum.mli b/src/lib/reasoners/enum.mli
deleted file mode 100644
index 2a685909f7..0000000000
--- a/src/lib/reasoners/enum.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-2024 --- OCamlPro SAS                           *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-(*type 'a abstract*)
-type 'a abstract = Cons of Uid.t * Ty.t |  Alien of 'a
-
-module type ALIEN = sig
-  include Sig.X
-  val embed : r abstract -> r
-  val extract : r -> (r abstract) option
-end
-
-module Shostak
-    (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract
diff --git a/src/lib/reasoners/enum_rel.mli b/src/lib/reasoners/enum_rel.mli
deleted file mode 100644
index 71cfa717c7..0000000000
--- a/src/lib/reasoners/enum_rel.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-2024 --- OCamlPro SAS                           *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-include Sig_rel.RELATION
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index bfdad703d6..12971f1ce4 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -37,11 +37,9 @@ module Rel3 : Sig_rel.RELATION = Bitv_rel
 
 module Rel4 : Sig_rel.RELATION = Arrays_rel
 
-module Rel5 : Sig_rel.RELATION = Enum_rel
+module Rel5 : Sig_rel.RELATION = Adt_rel
 
-module Rel6 : Sig_rel.RELATION = Adt_rel
-
-module Rel7 : Sig_rel.RELATION = Ite_rel
+module Rel6 : Sig_rel.RELATION = Ite_rel
 
 (* This value is unused. *)
 let timer = Timers.M_None
@@ -53,7 +51,6 @@ type t = {
   r4: Rel4.t;
   r5: Rel5.t;
   r6: Rel6.t;
-  r7: Rel7.t;
 }
 
 let empty uf =
@@ -63,8 +60,7 @@ let empty uf =
   let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in
   let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in
   let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in
-  let r7, doms7 = Rel7.empty (Uf.set_domains uf doms6) in
-  {r1; r2; r3; r4; r5; r6; r7}, doms7
+  {r1; r2; r3; r4; r5; r6}, doms6
 
 let (|@|) l1 l2 =
   if l1 == [] then l2
@@ -97,14 +93,10 @@ let assume env uf sa =
     Timers.with_timer Rel6.timer Timers.F_assume @@ fun () ->
     Rel6.assume env.r6 (Uf.set_domains uf doms5) sa
   in
-  let env7, doms7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) =
-    Timers.with_timer Rel7.timer Timers.F_assume @@ fun () ->
-    Rel7.assume env.r7 (Uf.set_domains uf doms6) sa
-  in
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7},
-  doms7,
-  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7;
-     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6},
+  doms6,
+  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6;
+     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 }
    : _ Sig_rel.result)
 
 let assume_th_elt env th_elt dep =
@@ -115,8 +107,7 @@ let assume_th_elt env th_elt dep =
   let env4 = Rel4.assume_th_elt env.r4 th_elt dep in
   let env5 = Rel5.assume_th_elt env.r5 th_elt dep in
   let env6 = Rel6.assume_th_elt env.r6 th_elt dep in
-  let env7 = Rel7.assume_th_elt env.r7 th_elt dep in
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}
 
 let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a
     k =
@@ -132,8 +123,7 @@ let query env uf a =
   try_query (module Rel3) env.r3 uf a @@ fun () ->
   try_query (module Rel4) env.r4 uf a @@ fun () ->
   try_query (module Rel5) env.r5 uf a @@ fun () ->
-  try_query (module Rel6) env.r6 uf a @@ fun () ->
-  try_query (module Rel7) env.r7 uf a @@ fun () -> None
+  try_query (module Rel6) env.r6 uf a @@ fun () -> None
 
 let case_split env uf ~for_model =
   Options.exec_thread_yield ();
@@ -143,8 +133,7 @@ let case_split env uf ~for_model =
   let seq4 = Rel4.case_split env.r4 uf ~for_model in
   let seq5 = Rel5.case_split env.r5 uf ~for_model in
   let seq6 = Rel6.case_split env.r6 uf ~for_model in
-  let seq7 = Rel7.case_split env.r7 uf ~for_model in
-  let splits = [seq1; seq2; seq3; seq4; seq5; seq6; seq7] in
+  let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in
   let splits = List.fold_left (|@|) [] splits in
   List.fast_sort
     (fun (_ ,_ , sz1) (_ ,_ , sz2) ->
@@ -181,8 +170,7 @@ let add env uf r t =
   let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in
   let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in
   let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in
-  let r7, doms7, eqs7 =Rel7.add env.r7 (Uf.set_domains uf doms6) r t in
-  {r1;r2;r3;r4;r5;r6;r7;},doms7,eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6|@|eqs7
+  {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6
 
 
 let instantiate ~do_syntactic_matching t_match env uf selector =
@@ -199,22 +187,13 @@ let instantiate ~do_syntactic_matching t_match env uf selector =
     Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in
   let r6, l6 =
     Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in
-  let r7, l7 =
-    Rel7.instantiate ~do_syntactic_matching t_match env.r7 uf selector in
-  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6; r7=r7},
-  l7 |@| l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
+  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6},
+  l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
 
 let new_terms env =
-  let t1 = Rel1.new_terms env.r1 in
-  let t2 = Rel2.new_terms env.r2 in
-  let t3 = Rel3.new_terms env.r3 in
-  let t4 = Rel4.new_terms env.r4 in
-  let t5 = Rel5.new_terms env.r5 in
-  let t6 = Rel6.new_terms env.r6 in
-  let t7 = Rel7.new_terms env.r7 in
-  Expr.Set.union t1
-    (Expr.Set.union t2
-       (Expr.Set.union t3
-          (Expr.Set.union t4
-             (Expr.Set.union t5
-                (Expr.Set.union t6 t7)) )))
+  Rel1.new_terms env.r1
+  |> Expr.Set.union @@ Rel2.new_terms env.r2
+  |> Expr.Set.union @@ Rel3.new_terms env.r3
+  |> Expr.Set.union @@ Rel4.new_terms env.r4
+  |> Expr.Set.union @@ Rel5.new_terms env.r5
+  |> Expr.Set.union @@ Rel6.new_terms env.r6
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 898070ff53..0c38e426d3 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -43,11 +43,8 @@ module rec CX : sig
   val extract3 : r -> BITV.t option
   val embed3 : BITV.t -> r
 
-  val extract4 : r -> ENUM.t option
-  val embed4 : ENUM.t -> r
-
-  val extract5 : r -> ADT.t option
-  val embed5 : ADT.t -> r
+  val extract4 : r -> ADT.t option
+  val embed4 : ADT.t -> r
 
 end =
 struct
@@ -58,7 +55,6 @@ struct
     | Arith of ARITH.t
     | Records of RECORDS.t
     | Bitv of BITV.t
-    | Enum of ENUM.t
     | Adt of ADT.t
 
   type r = {v : rview ; id : int}
@@ -74,7 +70,6 @@ struct
         | Arith t -> fprintf fmt "%a" ARITH.print t
         | Records t -> fprintf fmt "%a" RECORDS.print t
         | Bitv t -> fprintf fmt "%a" BITV.print t
-        | Enum t -> fprintf fmt "%a" ENUM.print t
         | Adt t -> fprintf fmt "%a" ADT.print t
         | Term t -> fprintf fmt "%a" Expr.print t
         | Ac t -> fprintf fmt "%a" AC.print t
@@ -87,8 +82,6 @@ struct
           fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t
         | Bitv t ->
           fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t
-        | Enum t ->
-          fprintf fmt "Enum(%s):[%a]" ENUM.name ENUM.print t
         | Adt t ->
           fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t
         | Term t ->
@@ -170,7 +163,6 @@ struct
         | Arith x -> 1 + 10 * ARITH.hash x
         | Records x -> 2 + 10 * RECORDS.hash x
         | Bitv x -> 3 + 10 * BITV.hash x
-        | Enum x -> 5 + 10 * ENUM.hash x
         | Adt x -> 6 + 10 * ADT.hash x
         | Ac ac -> 9 + 10 * AC.hash ac
         | Term t -> 8 + 10 * Expr.hash t
@@ -182,7 +174,6 @@ struct
       | Arith x, Arith y -> ARITH.equal x y
       | Records x, Records y -> RECORDS.equal x y
       | Bitv x, Bitv y -> BITV.equal x y
-      | Enum x, Enum y -> ENUM.equal x y
       | Adt x, Adt y -> ADT.equal x y
       | Term x, Term y -> Expr.equal x y
       | Ac x, Ac y -> AC.equal x y
@@ -209,8 +200,7 @@ struct
   let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)}
   let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)}
   let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)}
-  let embed4 x = hcons {v = Enum x; id = -1000 (* dummy *)}
-  let embed5 x = hcons {v = Adt x; id = -1000 (* dummy *)}
+  let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)}
 
   let ac_embed ({ Sig.l; _ } as t) =
     match l with
@@ -227,8 +217,7 @@ struct
   let extract1 = function { v=Arith r; _ } -> Some r | _ -> None
   let extract2 = function { v=Records r; _ } -> Some r | _ -> None
   let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None
-  let extract4 = function { v=Enum r; _ } -> Some r | _ -> None
-  let extract5 = function { v=Adt r; _ } -> Some r | _ -> None
+  let extract4 = function { v=Adt r; _ } -> Some r | _ -> None
 
   let ac_extract = function
     | { v = Ac t; _ }   -> Some t
@@ -239,7 +228,6 @@ struct
     | Arith _ -> ARITH.term_extract r
     | Records _ -> RECORDS.term_extract r
     | Bitv _ -> BITV.term_extract r
-    | Enum _ -> ENUM.term_extract r
     | Adt _ -> ADT.term_extract r
     | Ac _ -> None, false (* SYLVAIN : TODO *)
     | Term t -> Some t, true
@@ -250,7 +238,6 @@ struct
       | Arith _ -> ARITH.to_model_term r
       | Records _ -> RECORDS.to_model_term r
       | Bitv _ -> BITV.to_model_term r
-      | Enum _ -> ENUM.to_model_term r
       | Adt _ -> ADT.to_model_term r
       | Term t when Expr.is_model_term t -> Some t
       | Ac _ | Term _ -> None
@@ -266,7 +253,6 @@ struct
     | { v = Arith t; _ } -> ARITH.type_info t
     | { v = Records t; _ } -> RECORDS.type_info t
     | { v = Bitv t; _ } -> BITV.type_info t
-    | { v = Enum t; _ } -> ENUM.type_info t
     | { v = Adt t; _ } -> ADT.type_info t
     | { v = Ac x; _ } -> AC.type_info x
     | { v = Term t; _ } -> Expr.type_info t
@@ -279,8 +265,7 @@ struct
     | Arith _ -> -3
     | Records _ -> -4
     | Bitv _ -> -5
-    | Enum _ -> -7
-    | Adt _ -> -8
+    | Adt _ -> -7
 
   let compare_tag a b = theory_num a - theory_num b
 
@@ -291,7 +276,6 @@ struct
       | Arith _, Arith _ -> ARITH.compare a b
       | Records _, Records _ -> RECORDS.compare a b
       | Bitv _, Bitv _ -> BITV.compare a b
-      | Enum _, Enum _ -> ENUM.compare a b
       | Adt _, Adt _ -> ADT.compare a b
       | Term x, Term y -> Expr.compare x y
       | Ac x, Ac y -> AC.compare x y
@@ -308,7 +292,7 @@ struct
        | Records x -> RECORDS.hash x
        | Bitv x -> BITV.hash x
        | Arrays x -> ARRAYS.hash x
-       | Enum x -> ENUM.hash x
+       | Adt x -> ADT.hash x
 
    ***)
 
@@ -336,7 +320,6 @@ struct
     | Arith t -> ARITH.leaves t
     | Records t -> RECORDS.leaves t
     | Bitv t -> BITV.leaves t
-    | Enum t -> ENUM.leaves t
     | Adt t -> ADT.leaves t
     | Ac t -> r :: (AC.leaves t)
     | Term _ -> [r]
@@ -346,7 +329,6 @@ struct
     | Arith t -> ARITH.is_constant t
     | Records t -> RECORDS.is_constant t
     | Bitv t -> BITV.is_constant t
-    | Enum t -> ENUM.is_constant t
     | Adt t -> ADT.is_constant t
     | Term t ->
       begin
@@ -364,7 +346,6 @@ struct
       | Arith t -> ARITH.subst p v t
       | Records t -> RECORDS.subst p v t
       | Bitv t -> BITV.subst p v t
-      | Enum t -> ENUM.subst p v t
       | Adt t -> ADT.subst p v t
       | Ac t -> if equal p r then v else AC.subst p v t
       | Term _ -> if equal p r then v else r
@@ -376,35 +357,30 @@ struct
       ARITH.is_mine_symb sb ty,
       not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ENUM.is_mine_symb sb ty,
       not_restricted && ADT.is_mine_symb sb ty,
       AC.is_mine_symb sb ty
     with
-    | true  , false , false, false, false, false ->
+    | true, false, false, false, false ->
       Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
       ARITH.make t
 
-    | false , true  , false, false, false, false ->
+    | false, true, false, false, false ->
       Timers.with_timer Timers.M_Records Timers.F_make @@ fun () ->
       RECORDS.make t
 
-    | false , false , true  , false, false, false ->
+    | false, false, true, false, false ->
       Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () ->
       BITV.make t
 
-    | false , false , false , true , false, false ->
-      Timers.with_timer Timers.M_Sum Timers.F_make @@ fun () ->
-      ENUM.make t
-
-    | false , false , false , false, true , false ->
+    | false, false, false, true, false ->
       Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () ->
       ADT.make t
 
-    | false , false , false , false, false, true  ->
+    | false, false, false, false, true  ->
       Timers.with_timer Timers.M_AC Timers.F_make @@ fun () ->
       AC.make t
 
-    | false , false , false , false, false, false ->
+    | false, false, false, false, false ->
       term_embed t, []
 
     | _ -> assert false
@@ -415,23 +391,20 @@ struct
       ARITH.is_mine_symb sb ty,
       not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ENUM.is_mine_symb sb ty,
       not_restricted && ADT.is_mine_symb sb ty,
       AC.is_mine_symb sb ty
     with
-    | true  , false , false, false, false, false ->
+    | true, false, false, false, false ->
       ARITH.fully_interpreted sb
-    | false , true  , false, false, false, false ->
+    | false, true, false, false, false ->
       RECORDS.fully_interpreted sb
-    | false , false , true  , false, false, false ->
+    | false, false, true, false, false ->
       BITV.fully_interpreted sb
-    | false , false , false , true , false, false ->
-      ENUM.fully_interpreted sb
-    | false , false , false , false, true, false ->
+    | false, false, false, true, false ->
       ADT.fully_interpreted sb
-    | false , false , false , false, false, true  ->
+    | false, false, false, false, true  ->
       AC.fully_interpreted sb
-    | false , false , false , false, false, false ->
+    | false, false, false, false, false ->
       false
     | _ -> assert false
 
@@ -440,7 +413,6 @@ struct
     not (Options.get_restricted ()) &&
     (RECORDS.is_mine_symb sb ty ||
      BITV.is_mine_symb sb ty ||
-     ENUM.is_mine_symb sb ty ||
      ADT.is_mine_symb sb ty)
 
   let is_a_leaf r = match r.v with
@@ -457,19 +429,16 @@ struct
         ARITH.is_mine_symb ac.Sig.h ty,
         RECORDS.is_mine_symb ac.Sig.h ty,
         BITV.is_mine_symb ac.Sig.h ty,
-        ENUM.is_mine_symb ac.Sig.h ty,
         ADT.is_mine_symb ac.Sig.h ty,
         AC.is_mine_symb ac.Sig.h ty with
       (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *)
-      | true , false, false, false, false, false ->
+      | true, false, false, false, false ->
         ARITH.color ac
-      | false , true  , false, false, false, false ->
+      | false, true, false, false, false ->
         RECORDS.color ac
-      | false , false , true  , false, false, false ->
+      | false, false, true, false, false ->
         BITV.color ac
-      | false , false , false , true , false, false ->
-        ENUM.color ac
-      | false , false , false , false, true, false ->
+      | false, false, false, true, false ->
         ADT.color ac
       | _  -> ac_embed ac
 
@@ -479,7 +448,6 @@ struct
     | Arith a -> ARITH.abstract_selectors a acc
     | Records a -> RECORDS.abstract_selectors a acc
     | Bitv a -> BITV.abstract_selectors a acc
-    | Enum a -> ENUM.abstract_selectors a acc
     | Adt a -> ADT.abstract_selectors a acc
     | Term _ -> a, acc
     | Ac a -> AC.abstract_selectors a acc
@@ -568,10 +536,6 @@ struct
             Timers.with_timer BITV.timer Timers.F_solve @@ fun () ->
             BITV.solve ra rb pb
 
-          | Ty.Tsum _          ->
-            Timers.with_timer ENUM.timer Timers.F_solve @@ fun () ->
-            ENUM.solve ra rb pb
-
           (*| Ty.Tunit           -> pb *)
 
           | Ty.Tadt _ when not (Options.get_disable_adts()) ->
@@ -623,7 +587,6 @@ struct
             Some (Expr.fresh_name (Expr.type_info t), false)
         end
 
-      | _, Ty.Tsum _    -> ENUM.assign_value r distincts eq
       | _, Ty.Tadt _    when not (Options.get_disable_adts()) ->
         ADT.assign_value r distincts eq
 
@@ -700,24 +663,14 @@ and BITV : Sig.SHOSTAK
       let embed = embed3
     end)
 
-and ENUM : Sig.SHOSTAK
-  with type r = CX.r
-   and type t = CX.r Enum.abstract =
-  Enum.Shostak
-    (struct
-      include CX
-      let extract = extract4
-      let embed = embed4
-    end)
-
 and ADT : Sig.SHOSTAK
   with type r = CX.r
    and type t = CX.r Adt.abstract =
   Adt.Shostak
     (struct
       include CX
-      let extract = extract5
-      let embed = embed5
+      let extract = extract4
+      let embed = embed4
     end)
 
 (* Its signature is not Sig.SHOSTAK because it does not provide a solver *)
@@ -758,7 +711,6 @@ end
 module Arith = ARITH
 module Records = RECORDS
 module Bitv = BITV
-module Enum = ENUM
 module Adt = ADT
 module Polynome = TARITH
 module Ac = AC
diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli
index 88226887a4..0067e7df9d 100644
--- a/src/lib/reasoners/shostak.mli
+++ b/src/lib/reasoners/shostak.mli
@@ -44,9 +44,6 @@ module Records : Sig.SHOSTAK
 module Bitv : Sig.SHOSTAK
   with type r = Combine.r and type t = Combine.r Bitv.abstract
 
-module Enum : Sig.SHOSTAK
-  with type r = Combine.r and type t = Combine.r Enum.abstract
-
 module Adt : Sig.SHOSTAK
   with type r = Combine.r and type t = Combine.r Adt.abstract
 
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 7b51a8fc6a..9c8e098b28 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -159,21 +159,18 @@ module Main_Default : S = struct
            | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> mp
            | Tvar _ -> assert false
 
-           | Text (_, hs) | Tsum (hs, _) | Trecord { name = hs; _ } when
+           | Text (_, hs) | Trecord { name = hs; _ } when
                Uid.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
 
-           | Tsum (hs, _) ->
-             Uid.Map.add hs ty mp
-
            | Trecord { name; _ } ->
              (* cannot do better for records ? *)
              Uid.Map.add name ty mp
 
-           | Tadt (hs, _) ->
+           | Tadt (hs, _, _) ->
              (* cannot do better for ADT ? *)
              Uid.Map.add hs ty mp
         )sty Uid.Map.empty
@@ -187,19 +184,6 @@ module Main_Default : S = struct
            | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> ()
            | Tvar _ -> assert false
            | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty
-           | Tsum (_, l) ->
-             print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty;
-             begin match l with
-               | [] -> assert false
-               | e::l ->
-                 let print fmt e =
-                   Format.fprintf fmt " | %a" Uid.pp e
-                 in
-                 print_dbg ~flushed:false ~header:false "%a@ %a@ "
-                   Uid.pp e
-                   (pp_list_no_space print) l;
-             end
-
            | Trecord { Ty.lbs; _ } ->
              print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty;
              begin match lbs with
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 9993f4d043..b7ae778090 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -2617,7 +2617,6 @@ let mk_match e cases =
     match ty with
     | Ty.Tadt _ -> (fun hs -> Sy.destruct hs)
     | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs))
-    | Ty.Tsum _ -> (fun _hs -> assert false) (* no destructors for Tsum *)
     | _ -> assert false
   in
   let mker =
@@ -2629,13 +2628,6 @@ let mk_match e cases =
     | Ty.Trecord _ ->
       (fun _e _name -> assert false) (* no need to test for records *)
 
-    | Ty.Tsum _ ->
-      (fun e n -> (* testers are equalities for Tsum *)
-         let constr =
-           mk_term (Sy.constr n) [] (type_info e)
-         in
-         mk_eq ~iff:false e constr)
-
     | _ -> assert false
   in
   let res = compile_match mk_destr mker e cases e in
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index c94442bc15..bb59c2c9e5 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -75,7 +75,7 @@ let string_of_rounding_mode = to_smt_string
 
 let hstring_smt_reprs =
   List.map
-    (fun c -> Hs.make (to_smt_string c))
+    (fun c -> to_smt_string c, [])
     cstrs
 
 let hstring_ae_reprs =
@@ -92,18 +92,21 @@ 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 _, cstrs = DE.Term.define_adt ty_cst [] cstrs in
-  DE.Ty.apply ty_cst [], cstrs,
-  Ty.Tsum (Uid.of_dolmen ty_cst, List.map (fun (c, _) -> Uid.of_dolmen c) cstrs)
+  let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  let body =
+    List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
+  in
+  let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
   let table = Hashtbl.create 5 in
   List.iter2 (
-    fun key bnd ->
+    fun (key, _) bnd ->
       Hashtbl.add table key bnd
   ) hstring_smt_reprs cstrs;
   fun key ->
-    try Hashtbl.find table key with
+    try Hashtbl.find table (Hstring.view key) with
     | Not_found ->
       Fmt.failwith
         "Error while searching for SMT2 FPA value %a."
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index e1e9621c46..3afbd598b2 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -34,8 +34,7 @@ type t =
   | Tbitv of int
   | Text of t list * Uid.t
   | Tfarray of t * t
-  | Tsum of Uid.t * Uid.t list
-  | Tadt of Uid.t * t list
+  | Tadt of Uid.t * t list * bool
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
@@ -55,10 +54,10 @@ module Smtlib = struct
     | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n
     | Tfarray (a_t, r_t) ->
       Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t
-    | Text ([], name) | Tsum (name, _)
-    | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name
+    | Text ([], name)
+    | Trecord { args = []; name; _ } | Tadt (name, [], _) -> Uid.pp ppf name
     | Text (args, name)
-    | Trecord { args; name; _ } | Tadt (name, args) ->
+    | Trecord { args; name; _ } | Tadt (name, args, _) ->
       Fmt.(pf ppf "(@[%a %a@])" Uid.pp name (list ~sep:sp pp) args)
     | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
     | Tvar { value = Some t; _ } -> pp ppf t
@@ -122,8 +121,6 @@ let print_generic body_of =
         fprintf fmt "%a <ext>%a" print_list l Uid.pp s
       | Tfarray (t1, t2) ->
         fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2
-      | Tsum(s, _) ->
-        fprintf fmt "<sum>%a" Uid.pp s
       | Trecord { args = lv; name = n; lbs = lbls; _ } ->
         begin
           fprintf fmt "%a <record>%a" print_list lv Uid.pp n;
@@ -139,7 +136,7 @@ let print_generic body_of =
             fprintf fmt "}"
           end
         end
-      | Tadt (n, lv) ->
+      | Tadt (n, lv, _) ->
         fprintf fmt "%a <adt>%a" print_list lv Uid.pp n;
         begin match body_of with
           | None -> ()
@@ -222,13 +219,13 @@ let rec shorten ty =
     r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs;
     ty
 
-  | Tadt (n, args) ->
+  | Tadt (n, args, enum) ->
     let args' = List.map shorten args in
     shorten_body n args;
     (* should not rebuild the type if no changes are made *)
-    Tadt (n, args')
+    Tadt (n, args', enum)
 
-  | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty
+  | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
 
 and shorten_body _ _ =
   ()
@@ -248,9 +245,6 @@ let rec compare t1 t2 =
     if c<>0 then c
     else compare ta2 tb2
   | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1
-  | Tsum(s1, _), Tsum(s2, _) ->
-    Uid.compare s1 s2
-  | Tsum _, _ -> -1 | _ , Tsum _ -> 1
   | Trecord { args = a1; name = s1; lbs = l1; _ },
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
     let c = Uid.compare s1 s2 in
@@ -261,7 +255,7 @@ let rec compare t1 t2 =
         compare_list l1 l2
   | Trecord _, _ -> -1 | _ , Trecord _ -> 1
 
-  | Tadt (s1, pars1), Tadt (s2, pars2) ->
+  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
     let c = Uid.compare s1 s2 in
     if c <> 0 then c
     else compare_list pars1 pars2
@@ -300,7 +294,6 @@ let rec equal t1 t2 =
      with Invalid_argument _ -> false)
   | Tfarray (ta1, ta2), Tfarray (tb1, tb2) ->
     equal ta1 tb1 && equal ta2 tb2
-  | Tsum (s1, _), Tsum (s2, _) -> Uid.equal s1 s2
   | Trecord { args = a1; name = s1; lbs = l1; _ },
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
     begin
@@ -314,7 +307,7 @@ let rec equal t1 t2 =
   | Tint, Tint | Treal, Treal | Tbool, Tbool | Tunit, Tunit -> true
   | Tbitv n1, Tbitv n2 -> n1 =n2
 
-  | Tadt (s1, pars1), Tadt (s2, pars2) ->
+  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
     begin
       try Uid.equal s1 s2 && List.for_all2 equal pars1 pars2
       with Invalid_argument _ -> false
@@ -343,10 +336,9 @@ let rec matching s pat t =
     let s = List.fold_left2 matching s r1.args r2.args in
     List.fold_left2
       (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs
-  | Tsum (s1, _), Tsum (s2, _) when Uid.equal s1 s2 -> s
   | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s
   | Tbitv n , Tbitv m when n=m -> s
-  | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 ->
+  | Tadt(n1, args1, _), Tadt(n2, args2, _) when Uid.equal n1 n2 ->
     List.fold_left2 matching s args1 args2
   | _ , _ ->
     raise (TypeClash(pat,t))
@@ -376,12 +368,12 @@ let apply_subst =
                   name = r.name;
                   lbs = lbs}
 
-    | Tadt(name, params)
+    | Tadt(name, params, enum)
       [@ocaml.ppwarning "TODO: detect when there are no changes "]
       ->
-      Tadt (name, List.map (apply_subst s) params)
+      Tadt (name, List.map (apply_subst s) params, enum)
 
-    | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty
+    | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
   in
   fun s ty -> if M.is_empty s then ty else apply_subst s ty
 
@@ -410,9 +402,9 @@ let rec fresh ty subst =
            (x, ty)::lbs, subst) lbs ([], subst)
     in
     Trecord {r with  args = args; name = n; lbs = lbs}, subst
-  | Tadt(s,args) ->
+  | Tadt(s, args, enum) ->
     let args, subst = fresh_list args subst in
-    Tadt (s,args), subst
+    Tadt (s, args, enum), subst
   | t -> t, subst
 
 and fresh_list lty subst =
@@ -537,10 +529,8 @@ let fresh_empty_text =
     in
     text [] (Uid.of_dolmen id)
 
-let tsum s lc = Tsum (s, lc)
-
-let t_adt ?(body=None) s ty_vars =
-  let ty = Tadt (s, ty_vars) in
+let t_adt ?(enum=false) ?(body=None) s ty_vars =
+  let ty = Tadt (s, ty_vars, enum) in
   begin match body with
     | None -> ()
     | Some [] -> assert false
@@ -585,9 +575,9 @@ let rec hash t =
         (abs h) lbs
     in
     abs h
-  | Tsum (s, _) -> abs (Uid.hash s) (*we do not hash constructors*)
 
-  | Tadt (s, args) ->
+  | Tadt (s, args, _) ->
+    (* We do not hash constructors. *)
     let h =
       List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args
     in
@@ -600,8 +590,8 @@ let occurs { v = n; _ } t =
     | Tvar { v = m; _ } -> n=m
     | Text(l,_) -> List.exists occursrec l
     | Tfarray (t1,t2) -> occursrec t1 || occursrec t2
-    | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args
-    | Tsum _ | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
+    | Trecord { args ; _ } | Tadt (_, args, _) -> List.exists occursrec args
+    | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
   in occursrec t
 
 (*** destructive unification ***)
@@ -622,11 +612,10 @@ let rec unify t1 t2 =
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2
   | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name ->
     List.iter2 unify r1.args r2.args
-  | Tsum(s1, _) , Tsum(s2, _) when Uid.equal s1 s2 -> ()
   | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> ()
   | Tbitv n , Tbitv m when m=n -> ()
 
-  | Tadt(n1, p1), Tadt (n2, p2) when Uid.equal n1 n2 ->
+  | Tadt(n1, p1, _), Tadt (n2, p2, _) when Uid.equal n1 n2 ->
     List.iter2 unify p1 p2
 
   | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] ->
@@ -669,11 +658,11 @@ let vty_of t =
     | Trecord { args; lbs; _ } ->
       let acc = List.fold_left vty_of_rec acc args in
       List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs
-    | Tadt(_, args) ->
+    | Tadt(_, args, _) ->
       List.fold_left vty_of_rec acc args
 
     | Tvar { value = Some _ ; _ }
-    | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) ->
+    | Tint | Treal | Tbool | Tunit | Tbitv _ ->
       acc
   in
   vty_of_rec Svty.empty t
@@ -682,7 +671,7 @@ let vty_of t =
   [@ocaml.ppwarning "TODO: detect when there are no changes "]
 let rec monomorphize ty =
   match ty with
-  | Tint | Treal | Tbool | Tunit   | Tbitv _  | Tsum _ -> ty
+  | Tint | Treal | Tbool | Tunit   | Tbitv _  -> ty
   | Text (tyl,hs) -> Text (List.map monomorphize tyl, hs)
   | Trecord ({ args = tylv; name = n; lbs = tylb; _ } as r) ->
     let m_tylv = List.map monomorphize tylv in
@@ -694,8 +683,8 @@ let rec monomorphize ty =
   | Tvar {v=v; value=None} -> text [] (Uid.of_string ("'_c"^(string_of_int v)))
   | Tvar ({ value = Some ty1; _ } as r) ->
     Tvar { r with value = Some (monomorphize ty1)}
-  | Tadt(name, params) ->
-    Tadt(name, List.map monomorphize params)
+  | Tadt(name, params, enum) ->
+    Tadt(name, List.map monomorphize params, enum)
 
 let print_subst fmt sbt =
   M.iter (fun n ty -> Format.fprintf fmt "%d -> %a" n print ty) sbt;
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 5003566a66..01770e0723 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -48,16 +48,15 @@ type t =
   (** Abstract types applied to arguments. [Text (args, s)] is
       the application of the abstract type constructor [s] to
       arguments [args]. *)
+
   | Tfarray of t * t
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
-  | Tsum of Uid.t * Uid.t list
-  (** Enumeration, with its name, and the list of its constructors. *)
 
-  | Tadt of Uid.t * t list
-  (** Application of algebraic data types. [Tadt (a, params)] denotes
+  | Tadt of Uid.t * t list * bool
+  (** Application of algebraic data types. [Tadt (a, params, enum)] denotes
       the application of the polymorphic datatype [a] to the types parameters
-      [params].
+      [params]. The flag [enum] determines if the ADT is an enum.
 
       For instance the type of integer lists can be represented by the
       value [Tadt (Hstring.make "list", [Tint])] where the identifier "list"
@@ -169,11 +168,8 @@ val text : t list -> Uid.t -> t
 (** Apply the abstract type constructor to the list of type arguments
     given. *)
 
-val tsum : Uid.t -> Uid.t list -> t
-(** Create an enumeration type. [tsum name enums] creates an enumeration
-    named [name], with constructors [enums]. *)
-
 val t_adt :
+  ?enum:bool ->
   ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of

From 7045bb6b4e03521f4f0dc018c0ab2b60aa3ca989 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Mon, 3 Jun 2024 15:32:17 +0200
Subject: [PATCH 2/7] Attempt to fix regressions

---
 src/lib/frontend/d_cnf.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index dcf6d87c90..fd8d2bc6ad 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -692,7 +692,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       Cache.store_ty ty_c ty
 
-    | Tadt (hs, tyl, false), Some (Adt { cases; ty = ty_c; _ }) ->
+    | Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->

From 226fda18dad3a90ed112009e195a2a4baa933fe5 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 11:24:14 +0200
Subject: [PATCH 3/7] poetry

---
 src/lib/frontend/typechecker.ml | 6 +++---
 src/lib/reasoners/adt_rel.ml    | 6 +++++-
 src/lib/structures/ty.mli       | 9 ++++++---
 3 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 3bb0f2c5cb..aeecef0508 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -302,7 +302,7 @@ module Env = struct
     | Ty.Tadt (name, [], true) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
-      List.find (fun c -> String.equal n @@ Uid.show c) cstrs
+      List.find (Uid.equal n) cstrs
     | _ ->
       assert false
 
@@ -329,9 +329,9 @@ module Env = struct
     let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in
     let tname = Fpa_rounding.fpa_rounding_mode_ae_type_name in
     let float32 = float (int "24") (int "149") in
-    let float32d = float32 (mode nte) in
+    let float32d = float32 (mode (Uid.of_string nte)) in
     let float64 = float (int "53") (int "1074") in
-    let float64d = float64 (mode nte) in
+    let float64d = float64 (mode (Uid.of_string nte)) in
     let op n op profile =
       MString.add n @@ `Term (Symbols.Op op, profile, Other)
     in
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index a15f656ecc..d2f02ebcdf 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -660,6 +660,10 @@ let split_enum env uf =
   if can_split env n then
     let _, cons = Option.get @@ build_constr_eq r c in
     let nr, ctx = X.make cons in
+    (* In the current implementation of `X.make`, we produce
+       a nonempty context only for interpreted semantic values
+       of the `Arith` and `Records` theories. The semantic
+       values `cons` never involves such values. *)
     assert (Lists.is_empty ctx);
     Some (LR.mkv_eq r nr)
   else
@@ -672,11 +676,11 @@ let split_best_domain ~for_model uf =
     let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
     let* r, c = pick_best ds in
     let _, cons = Option.get @@ build_constr_eq r c in
+    let nr, ctx = X.make cons in
     (* In the current implementation of `X.make`, we produce
        a nonempty context only for interpreted semantic values
        of the `Arith` and `Records` theories. The semantic
        values `cons` never involves such values. *)
-    let nr, ctx = X.make cons in
     assert (Lists.is_empty ctx);
     Some (LR.mkv_eq r nr)
 
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 01770e0723..d71753441d 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -59,8 +59,8 @@ type t =
       [params]. The flag [enum] determines if the ADT is an enum.
 
       For instance the type of integer lists can be represented by the
-      value [Tadt (Hstring.make "list", [Tint])] where the identifier "list"
-      denotes a polymorphic ADT defined by the user with [t_adt]. *)
+      value [Tadt (Hstring.make "list", [Tint], false)] where the identifier
+      {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
   | Trecord of trecord
   (** Record type. *)
@@ -176,7 +176,10 @@ val t_adt :
     its destructors with their respective types. If [body] is none,
     then no definition will be registered for this type. The second
     argument is the name of the type. The third one provides its list
-    of arguments. *)
+    of arguments.
+
+    The flag [enum] is used to annotate ADT whose all the constructors have no
+    payload. *)
 
 val trecord :
   ?sort_fields:bool ->

From 1bc685a1f7be38bf7f8f201c5a43568e8fa10b82 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 13:24:30 +0200
Subject: [PATCH 4/7] Restore the check for polymorphism in enum type

---
 src/lib/frontend/typechecker.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index aeecef0508..0f8500d46e 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -145,6 +145,12 @@ module Types = struct
     | Abstract ->
       let ty = Ty.text ty_vars (Uid.of_string id) in
       ty, { env with to_ty = MString.add id ty env.to_ty }
+    | Enum l ->
+      if not (Lists.is_empty ty_vars) then
+        Errors.typing_error (PolymorphicEnum id) loc;
+      let body = List.map (fun constr -> Uid.of_string constr, []) l in
+      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
+      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
         List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in
@@ -164,10 +170,6 @@ module Types = struct
             from_labels =
               List.fold_left
                 (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs }
-    | Enum l ->
-      let body = List.map (fun constr -> Uid.of_string constr, []) l in
-      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
-      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Algebraic l ->
       let l = (* convert ppure_type to Ty.t in l *)
         List.map (fun (constr, l) ->

From 36d143d6a8a514ac7af4bd95b4e174dea46430ef Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 13:52:46 +0200
Subject: [PATCH 5/7] Use a polymorphic variant for the enum flag

---
 src/lib/frontend/d_cnf.ml          |  7 +++++--
 src/lib/frontend/typechecker.ml    | 10 +++++-----
 src/lib/reasoners/adt_rel.ml       |  2 +-
 src/lib/structures/fpa_rounding.ml |  2 +-
 src/lib/structures/ty.ml           |  6 +++---
 src/lib/structures/ty.mli          | 14 +++++++-------
 6 files changed, 22 insertions(+), 19 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index fd8d2bc6ad..bb03097cac 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -632,7 +632,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
       ) ([], true) cases
     in
     let body = Some (List.rev rev_cs) in
-    let ty = Ty.t_adt ~enum:is_enum ~body uid tyvl in
+    let kind = if is_enum then `Enum else `Adt in
+    let ty = Ty.t_adt ~kind ~body uid tyvl in
     Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
@@ -748,7 +749,9 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             if (record || Array.length cases = 1) && not contains_adts
             then
               Ty.trecord ~record_constr:uid tyvl uid []
-            else Ty.t_adt ~enum:is_enum uid tyvl
+            else
+              let kind = if is_enum then `Enum else `Adt in
+              Ty.t_adt ~kind uid tyvl
           in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 0f8500d46e..7227f90983 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -69,11 +69,11 @@ module Types = struct
     match ty with
     | Ty.Text (lty', s)
     | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty',false) ->
+    | Ty.Tadt (s,lty',`Adt) ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
-    | Ty.Tadt (s,lty',true) ->
+    | Ty.Tadt (s,lty',`Enum) ->
       if List.length lty <> 0 || List.length lty' <> 0 then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       []
@@ -149,7 +149,7 @@ module Types = struct
       if not (Lists.is_empty ty_vars) then
         Errors.typing_error (PolymorphicEnum id) loc;
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
-      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
+      let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_string id) [] in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
@@ -275,7 +275,7 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tadt (name, [], true) ->
+    | Ty.Tadt (name, [], `Enum) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
@@ -301,7 +301,7 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tadt (name, [], true) ->
+    | Ty.Tadt (name, [], `Enum) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.find (Uid.equal n) cstrs
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index d2f02ebcdf..ca13e5c766 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -156,7 +156,7 @@ module Domains = struct
 
   let is_enum r =
     match X.type_info r with
-    | Ty.Tadt (_, [], true) -> true
+    | Ty.Tadt (_, [], `Enum) -> true
     | _ -> false
 
   let internal_update r nd t =
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index bb59c2c9e5..73fb653e14 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -96,7 +96,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let body =
     List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
   in
-  let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 3afbd598b2..ed9c2fe70d 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -34,7 +34,7 @@ type t =
   | Tbitv of int
   | Text of t list * Uid.t
   | Tfarray of t * t
-  | Tadt of Uid.t * t list * bool
+  | Tadt of Uid.t * t list * [`Adt | `Enum]
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
@@ -529,8 +529,8 @@ let fresh_empty_text =
     in
     text [] (Uid.of_dolmen id)
 
-let t_adt ?(enum=false) ?(body=None) s ty_vars =
-  let ty = Tadt (s, ty_vars, enum) in
+let t_adt ?(kind=`Adt) ?(body=None) s ty_vars =
+  let ty = Tadt (s, ty_vars, kind) in
   begin match body with
     | None -> ()
     | Some [] -> assert false
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index d71753441d..c532b433b4 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -53,13 +53,13 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.t * t list * bool
-  (** Application of algebraic data types. [Tadt (a, params, enum)] denotes
+  | Tadt of Uid.t * t list * [`Adt | `Enum]
+  (** Application of algebraic data types. [Tadt (a, params, kind)] denotes
       the application of the polymorphic datatype [a] to the types parameters
-      [params]. The flag [enum] determines if the ADT is an enum.
+      [params]. The flag [kind] determines if the ADT is an enum.
 
       For instance the type of integer lists can be represented by the
-      value [Tadt (Hstring.make "list", [Tint], false)] where the identifier
+      value [Tadt (Hstring.make "list", [Tint], `Adt)] where the identifier
       {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
   | Trecord of trecord
@@ -169,7 +169,7 @@ val text : t list -> Uid.t -> t
     given. *)
 
 val t_adt :
-  ?enum:bool ->
+  ?kind:[`Adt | `Enum] ->
   ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
@@ -178,8 +178,8 @@ val t_adt :
     argument is the name of the type. The third one provides its list
     of arguments.
 
-    The flag [enum] is used to annotate ADT whose all the constructors have no
-    payload. *)
+    The flag [kind] is used to annotate ADT that are enum types. [`Adt]
+    kind is the default. *)
 
 val trecord :
   ?sort_fields:bool ->

From 73739aa790fae4d5271e0613d1bdd2a893e7d039 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 15:43:08 +0200
Subject: [PATCH 6/7] Store the enum flag in the `type_body`

---
 src/lib/frontend/d_cnf.ml          |  29 +++----
 src/lib/frontend/typechecker.ml    |  26 +++----
 src/lib/reasoners/adt.ml           |   8 +-
 src/lib/reasoners/adt_rel.ml       |  23 +++---
 src/lib/reasoners/theory.ml        |   2 +-
 src/lib/structures/fpa_rounding.ml |   2 +-
 src/lib/structures/ty.ml           | 118 ++++++++++++++++-------------
 src/lib/structures/ty.mli          |  31 ++++----
 8 files changed, 124 insertions(+), 115 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index bb03097cac..7b3582e86f 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -546,8 +546,8 @@ and handle_ty_app ?(update = false) ty_c l =
         apply_ty_substs tysubsts tv
       )
 
-    | Tadt (hs, tyl, enum) ->
-      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl, enum)
+    | Tadt (hs, tyl) ->
+      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl)
 
     | Trecord ({ args; lbs; _ } as rcrd) ->
       Trecord {
@@ -565,7 +565,7 @@ and handle_ty_app ?(update = false) ty_c l =
   (* Recover the initial versions of the types and apply them on the provided
      type arguments stored in [tyl]. *)
   match Cache.find_ty ty_c with
-  | Tadt (hs, _, enum) -> Tadt (hs, tyl, enum)
+  | Tadt (hs, _) -> Tadt (hs, tyl)
 
   | Trecord { args; _ } as ty ->
     let tysubsts =
@@ -615,10 +615,9 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let uid = Uid.of_dolmen 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, is_enum =
+    let rev_cs =
       Array.fold_left (
-        fun (accl, is_enum) DE.{ cstr; dstrs; _ } ->
-          let is_enum = is_enum && Array.length dstrs = 0 in
+        fun accl DE.{ cstr; dstrs; _ } ->
           let rev_fields =
             Array.fold_left (
               fun acc tc_o ->
@@ -628,12 +627,11 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
                 | None -> assert false
             ) [] dstrs
           in
-          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl, is_enum
-      ) ([], true) cases
+          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+      ) [] cases
     in
     let body = Some (List.rev rev_cs) in
-    let kind = if is_enum then `Enum else `Adt in
-    let ty = Ty.t_adt ~kind ~body uid tyvl in
+    let ty = Ty.t_adt ~body uid tyvl in
     Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
@@ -693,7 +691,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       Cache.store_ty ty_c ty
 
-    | Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) ->
+    | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->
@@ -737,12 +735,6 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       fun acc tdef ->
         match tdef with
         | DE.Adt { cases; record; ty = ty_c; } as adt ->
-          let is_enum =
-            Array.fold_left (
-              fun is_enum DE.{ dstrs; _ } ->
-                is_enum && Array.length dstrs = 0
-            ) true cases
-          in
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
           let uid = Uid.of_dolmen ty_c in
           let ty =
@@ -750,8 +742,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             then
               Ty.trecord ~record_constr:uid tyvl uid []
             else
-              let kind = if is_enum then `Enum else `Adt in
-              Ty.t_adt ~kind uid tyvl
+              Ty.t_adt uid tyvl
           in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 7227f90983..fdc2373c0e 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -69,14 +69,10 @@ module Types = struct
     match ty with
     | Ty.Text (lty', s)
     | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty',`Adt) ->
+    | Ty.Tadt (s,lty') ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
-    | Ty.Tadt (s,lty',`Enum) ->
-      if List.length lty <> 0 || List.length lty' <> 0 then
-        Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
-      []
     | _ -> assert false
 
   let equal_pp_vars lpp lvars =
@@ -149,7 +145,7 @@ module Types = struct
       if not (Lists.is_empty ty_vars) then
         Errors.typing_error (PolymorphicEnum id) loc;
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
-      let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_string id) [] in
+      let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
@@ -275,8 +271,9 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tadt (name, [], `Enum) ->
-      let Adt cases = Ty.type_body name [] in
+    | Ty.Tadt (name, []) ->
+      let Ty.{ cases; kind } = Ty.type_body name [] in
+      assert (Stdlib.(kind = Ty.Enum));
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
         (fun m c ->
@@ -301,8 +298,9 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tadt (name, [], `Enum) ->
-      let Adt cases = Ty.type_body name [] in
+    | Ty.Tadt (name, []) ->
+      let Ty.{ cases; kind } = Ty.type_body name [] in
+      assert (Stdlib.(kind = Ty.Enum));
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.find (Uid.equal n) cstrs
     | _ ->
@@ -1005,8 +1003,8 @@ let rec type_term ?(call_from_type_form=false) env f =
       let e = type_term env e in
       let ty = Ty.shorten e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params, _) ->
-          let Ty.Adt cases = Ty.type_body name params in
+        | Ty.Tadt (name, params) ->
+          let Ty.{ cases; _ } = Ty.type_body name params in
           cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr; destrs = lbs}]
@@ -1413,8 +1411,8 @@ and type_form ?(in_theory=false) env f =
       let e = type_term env e in
       let ty = e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params, _) ->
-          let Ty.Adt cases = Ty.type_body name params in
+        | Ty.Tadt (name, params) ->
+          let Ty.{ cases; _ } = Ty.type_body name params in
           cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr ; destrs = lbs}]
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 34cfc922f8..be34ff7938 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -54,9 +54,9 @@ let constr_of_destr ty dest =
       ~module_name:"Adt" ~function_name:"constr_of_destr"
       "ty = %a" Ty.print ty;
   match ty with
-  | Ty.Tadt (s, params, _) ->
+  | Ty.Tadt (s, params) ->
     begin
-      let Ty.Adt cases = Ty.type_body s params in
+      let Ty.{ cases; _ } = Ty.type_body s params in
       try
         List.find
           (fun { Ty.destrs; _ } ->
@@ -173,8 +173,8 @@ module Shostak (X : ALIEN) = struct
     in
     let xs = List.rev sx in
     match f, xs, ty with
-    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) ->
-      let Ty.Adt cases = Ty.type_body name params in
+    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
+      let Ty.{ cases; _ } = Ty.type_body name params in
       let case_hs =
         try Ty.assoc_destrs hs cases with Not_found -> assert false
       in
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index ca13e5c766..e85d243c43 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -83,14 +83,14 @@ module Domain = struct
 
   let unknown ty =
     match ty with
-    | Ty.Tadt (name, params, _) ->
+    | Ty.Tadt (name, params) ->
       (* Return the list of all the constructors of the type of [r]. *)
-      let Adt body = Ty.type_body name params in
+      let Ty.{ cases; _ } = Ty.type_body name params in
       let constrs =
         List.fold_left
           (fun acc Ty.{ constr; _ } ->
              TSet.add constr acc
-          ) TSet.empty body
+          ) TSet.empty cases
       in
       assert (not @@ TSet.is_empty constrs);
       { constrs; ex = Ex.empty }
@@ -156,7 +156,12 @@ module Domains = struct
 
   let is_enum r =
     match X.type_info r with
-    | Ty.Tadt (_, [], `Enum) -> true
+    | Ty.Tadt (name, params) ->
+      let Ty.{ kind; _ } = Ty.type_body name params in
+      begin match kind with
+        | Enum -> true
+        | Adt -> false
+      end
     | _ -> false
 
   let internal_update r nd t =
@@ -477,10 +482,10 @@ let build_constr_eq r c =
   match Th.embed r with
   | Alien r ->
     begin match X.type_info r with
-      | Ty.Tadt (name, params, _) as ty ->
-        let Ty.Adt body = Ty.type_body name params in
+      | Ty.Tadt (name, params) as ty ->
+        let Ty.{ cases; _ } = Ty.type_body name params in
         let ds =
-          try Ty.assoc_destrs c body with Not_found -> assert false
+          try Ty.assoc_destrs c cases with Not_found -> assert false
         in
         let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in
         let cons = E.mk_constr c xs ty in
@@ -578,9 +583,9 @@ let two = Numbers.Q.from_int 2
 (* TODO: we should compute this reverse map in `Ty` and store it there. *)
 let constr_of_destr ty d =
   match ty with
-  | Ty.Tadt (name, params, _) ->
+  | Ty.Tadt (name, params) ->
     begin
-      let Ty.Adt cases = Ty.type_body name params in
+      let Ty.{ cases; _ } = Ty.type_body name params in
       try
         let r =
           List.find
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 9c8e098b28..5c5dddd8a4 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -170,7 +170,7 @@ module Main_Default : S = struct
              (* cannot do better for records ? *)
              Uid.Map.add name ty mp
 
-           | Tadt (hs, _, _) ->
+           | Tadt (hs, _) ->
              (* cannot do better for ADT ? *)
              Uid.Map.add hs ty mp
         )sty Uid.Map.empty
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index 73fb653e14..d12e38d513 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -96,7 +96,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let body =
     List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
   in
-  let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index ed9c2fe70d..0f2dcafbfd 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -34,7 +34,7 @@ type t =
   | Tbitv of int
   | Text of t list * Uid.t
   | Tfarray of t * t
-  | Tadt of Uid.t * t list * [`Adt | `Enum]
+  | Tadt of Uid.t * t list
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
@@ -55,9 +55,9 @@ module Smtlib = struct
     | Tfarray (a_t, r_t) ->
       Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t
     | Text ([], name)
-    | Trecord { args = []; name; _ } | Tadt (name, [], _) -> Uid.pp ppf name
+    | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name
     | Text (args, name)
-    | Trecord { args; name; _ } | Tadt (name, args, _) ->
+    | Trecord { args; name; _ } | Tadt (name, args) ->
       Fmt.(pf ppf "(@[%a %a@])" Uid.pp name (list ~sep:sp pp) args)
     | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
     | Tvar { value = Some t; _ } -> pp ppf t
@@ -72,8 +72,12 @@ type adt_constr =
   { constr : Uid.t ;
     destrs : (Uid.t * t) list }
 
-type type_body =
-  | Adt of adt_constr list
+type adt_kind = Enum | Adt
+
+type type_body = {
+  cases : adt_constr list;
+  kind : adt_kind
+}
 
 
 let assoc_destrs hs cases =
@@ -136,14 +140,12 @@ let print_generic body_of =
             fprintf fmt "}"
           end
         end
-      | Tadt (n, lv, _) ->
+      | Tadt (n, lv) ->
         fprintf fmt "%a <adt>%a" print_list lv Uid.pp n;
         begin match body_of with
           | None -> ()
           | Some type_body ->
-            let cases = match type_body n lv with
-              | Adt cases -> cases
-            in
+            let { cases; _ } = type_body n lv in
             fprintf fmt " = {";
             let first = ref true in
             List.iter
@@ -219,11 +221,11 @@ let rec shorten ty =
     r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs;
     ty
 
-  | Tadt (n, args, enum) ->
+  | Tadt (n, args) ->
     let args' = List.map shorten args in
     shorten_body n args;
     (* should not rebuild the type if no changes are made *)
-    Tadt (n, args', enum)
+    Tadt (n, args')
 
   | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
 
@@ -255,7 +257,7 @@ let rec compare t1 t2 =
         compare_list l1 l2
   | Trecord _, _ -> -1 | _ , Trecord _ -> 1
 
-  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
+  | Tadt (s1, pars1), Tadt (s2, pars2) ->
     let c = Uid.compare s1 s2 in
     if c <> 0 then c
     else compare_list pars1 pars2
@@ -307,7 +309,7 @@ let rec equal t1 t2 =
   | Tint, Tint | Treal, Treal | Tbool, Tbool | Tunit, Tunit -> true
   | Tbitv n1, Tbitv n2 -> n1 =n2
 
-  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
+  | Tadt (s1, pars1), Tadt (s2, pars2) ->
     begin
       try Uid.equal s1 s2 && List.for_all2 equal pars1 pars2
       with Invalid_argument _ -> false
@@ -338,7 +340,7 @@ let rec matching s pat t =
       (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs
   | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s
   | Tbitv n , Tbitv m when n=m -> s
-  | Tadt(n1, args1, _), Tadt(n2, args2, _) when Uid.equal n1 n2 ->
+  | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 ->
     List.fold_left2 matching s args1 args2
   | _ , _ ->
     raise (TypeClash(pat,t))
@@ -368,10 +370,10 @@ let apply_subst =
                   name = r.name;
                   lbs = lbs}
 
-    | Tadt(name, params, enum)
+    | Tadt(name, params)
       [@ocaml.ppwarning "TODO: detect when there are no changes "]
       ->
-      Tadt (name, List.map (apply_subst s) params, enum)
+      Tadt (name, List.map (apply_subst s) params)
 
     | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
   in
@@ -402,9 +404,9 @@ let rec fresh ty subst =
            (x, ty)::lbs, subst) lbs ([], subst)
     in
     Trecord {r with  args = args; name = n; lbs = lbs}, subst
-  | Tadt(s, args, enum) ->
+  | Tadt(s, args) ->
     let args, subst = fresh_list args subst in
-    Tadt (s, args, enum), subst
+    Tadt (s, args), subst
   | t -> t, subst
 
 and fresh_list lty subst =
@@ -434,22 +436,21 @@ module Decls = struct
 
   let fresh_type params body =
     let params, subst = fresh_list params esubst in
-    match body with
-    | Adt cases ->
-      let _subst, cases =
-        List.fold_left
-          (fun (subst, cases) {constr; destrs} ->
-             let subst, destrs =
-               List.fold_left
-                 (fun (subst, destrs) (d, ty) ->
-                    let ty, subst = fresh ty subst in
-                    subst, (d, ty) :: destrs
-                 )(subst, []) (List.rev destrs)
-             in
-             subst, {constr; destrs} :: cases
-          )(subst, []) (List.rev cases)
-      in
-      params, Adt cases
+    let { cases; kind } = body in
+    let _subst, cases =
+      List.fold_left
+        (fun (subst, cases) {constr; destrs} ->
+           let subst, destrs =
+             List.fold_left
+               (fun (subst, destrs) (d, ty) ->
+                  let ty, subst = fresh ty subst in
+                  subst, (d, ty) :: destrs
+               )(subst, []) (List.rev destrs)
+           in
+           subst, {constr; destrs} :: cases
+        )(subst, []) (List.rev cases)
+    in
+    params, { cases; kind }
 
 
   let add name params body =
@@ -488,16 +489,17 @@ module Decls = struct
               )M.empty params args
           with Invalid_argument _ -> assert false
         in
-        let body = match body with
-          | Adt cases ->
-            Adt(
-              List.map
-                (fun {constr; destrs} ->
-                   {constr;
-                    destrs =
-                      List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs }
-                ) cases
-            )
+        let body =
+          let { cases; kind } = body in
+          let cases =
+            List.map
+              (fun {constr; destrs} ->
+                 {constr;
+                  destrs =
+                    List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs }
+              ) cases
+          in
+          { cases; kind }
         in
         let params = List.map (fun ty -> apply_subst sbt ty) params in
         add name params body;
@@ -529,8 +531,8 @@ let fresh_empty_text =
     in
     text [] (Uid.of_dolmen id)
 
-let t_adt ?(kind=`Adt) ?(body=None) s ty_vars =
-  let ty = Tadt (s, ty_vars, kind) in
+let t_adt ?(body=None) s ty_vars =
+  let ty = Tadt (s, ty_vars) in
   begin match body with
     | None -> ()
     | Some [] -> assert false
@@ -541,12 +543,20 @@ let t_adt ?(kind=`Adt) ?(body=None) s ty_vars =
       let cases =
         List.map (fun (constr, destrs) -> {constr; destrs}) cases
       in
-      Decls.add s ty_vars (Adt cases)
+      let is_enum =
+        List.for_all (fun { destrs; _ } -> Lists.is_empty destrs) cases
+      in
+      let kind = if is_enum then Enum else Adt in
+      Decls.add s ty_vars { cases; kind }
     | Some cases ->
       let cases =
         List.map (fun (constr, destrs) -> {constr; destrs}) cases
       in
-      Decls.add s ty_vars (Adt cases)
+      let is_enum =
+        List.for_all (fun { destrs; _ } -> Lists.is_empty destrs) cases
+      in
+      let kind = if is_enum then Enum else Adt in
+      Decls.add s ty_vars { cases; kind }
   end;
   ty
 
@@ -576,7 +586,7 @@ let rec hash t =
     in
     abs h
 
-  | Tadt (s, args, _) ->
+  | Tadt (s, args) ->
     (* We do not hash constructors. *)
     let h =
       List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args
@@ -590,7 +600,7 @@ let occurs { v = n; _ } t =
     | Tvar { v = m; _ } -> n=m
     | Text(l,_) -> List.exists occursrec l
     | Tfarray (t1,t2) -> occursrec t1 || occursrec t2
-    | Trecord { args ; _ } | Tadt (_, args, _) -> List.exists occursrec args
+    | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args
     | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
   in occursrec t
 
@@ -615,7 +625,7 @@ let rec unify t1 t2 =
   | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> ()
   | Tbitv n , Tbitv m when m=n -> ()
 
-  | Tadt(n1, p1, _), Tadt (n2, p2, _) when Uid.equal n1 n2 ->
+  | Tadt(n1, p1), Tadt (n2, p2) when Uid.equal n1 n2 ->
     List.iter2 unify p1 p2
 
   | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] ->
@@ -658,7 +668,7 @@ let vty_of t =
     | Trecord { args; lbs; _ } ->
       let acc = List.fold_left vty_of_rec acc args in
       List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs
-    | Tadt(_, args, _) ->
+    | Tadt(_, args) ->
       List.fold_left vty_of_rec acc args
 
     | Tvar { value = Some _ ; _ }
@@ -683,8 +693,8 @@ let rec monomorphize ty =
   | Tvar {v=v; value=None} -> text [] (Uid.of_string ("'_c"^(string_of_int v)))
   | Tvar ({ value = Some ty1; _ } as r) ->
     Tvar { r with value = Some (monomorphize ty1)}
-  | Tadt(name, params, enum) ->
-    Tadt(name, List.map monomorphize params, enum)
+  | Tadt(name, params) ->
+    Tadt(name, List.map monomorphize params)
 
 let print_subst fmt sbt =
   M.iter (fun n ty -> Format.fprintf fmt "%d -> %a" n print ty) sbt;
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index c532b433b4..2b730c67a9 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -53,13 +53,13 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.t * t list * [`Adt | `Enum]
-  (** Application of algebraic data types. [Tadt (a, params, kind)] denotes
+  | Tadt of Uid.t * t list
+  (** Application of algebraic data types. [Tadt (a, params)] denotes
       the application of the polymorphic datatype [a] to the types parameters
-      [params]. The flag [kind] determines if the ADT is an enum.
+      [params].
 
       For instance the type of integer lists can be represented by the
-      value [Tadt (Hstring.make "list", [Tint], `Adt)] where the identifier
+      value [Tadt (Hstring.make "list", [Tint]] where the identifier
       {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
   | Trecord of trecord
@@ -99,13 +99,22 @@ type adt_constr =
         their respective types *)
   }
 
-(** bodies of types definitions. Currently, bodies are inlined in the
+type adt_kind =
+  | Enum (* ADT whose all the constructors have no payload. *)
+  | Adt
+
+(** Bodies of types definitions. Currently, bodies are inlined in the
     type [t] for records and enumerations. But, this is not possible
     for recursive ADTs *)
-type type_body =
-  | Adt of adt_constr list
+type type_body = {
+  cases : adt_constr list;
   (** body of an algebraic datatype *)
 
+  kind : adt_kind
+  (** This flag is used by the case splitting mechanism of the ADT theory.
+      We perform eager splitting on ADT of kind [enum]. *)
+}
+
 module Svty : Set.S with type elt = int
 (** Sets of type variables, indexed by their identifier. *)
 
@@ -169,17 +178,13 @@ val text : t list -> Uid.t -> t
     given. *)
 
 val t_adt :
-  ?kind:[`Adt | `Enum] ->
-  ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
+  ?body:((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> 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,
     then no definition will be registered for this type. The second
     argument is the name of the type. The third one provides its list
-    of arguments.
-
-    The flag [kind] is used to annotate ADT that are enum types. [`Adt]
-    kind is the default. *)
+    of arguments. *)
 
 val trecord :
   ?sort_fields:bool ->

From 3fc21123232bea1d4f881c71a172e15fa0aa1f5c Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 16:00:16 +0200
Subject: [PATCH 7/7] Factorize the code of `split_enum` and `split_best`

---
 src/lib/reasoners/adt_rel.ml | 69 ++++++++++++++----------------------
 1 file changed, 27 insertions(+), 42 deletions(-)

diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index e85d243c43..612a31cac1 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -538,7 +538,7 @@ let remove_redundancies la =
        end
     ) la
 
-(* Update the counter of case-split size in [env]. *)
+(* Update the counter of case split size in [env]. *)
 let count_splits env la =
   List.fold_left
     (fun nb (_, _, _, i) ->
@@ -608,7 +608,7 @@ let can_split env n =
 
 let (let*) = Option.bind
 
-(* Do a cases-plit by choosing a semantic value [r] and constructor [c]
+(* Do a case split by choosing a semantic value [r] and constructor [c]
    for which there are delayed destructor applications and propagate the
    literal [(not (_ is c) r)]. *)
 let split_delayed_destructor env =
@@ -630,27 +630,26 @@ let split_delayed_destructor env =
 (* Pick a constructor in a tracked domain with minimal cardinal.
    Returns [None] if there is no such constructor. *)
 let pick_best ds =
-  let* _, r, c =
-    Domains.fold
-      (fun r d best ->
-         let cd = Domain.cardinal d in
-         match Th.embed r, best with
-         | Constr _, _ -> best
-         | _, Some (n, _, _) when n <= cd -> best
-         | _ ->
-           let c = Domain.choose d in
-           Some (cd, r, c)
-      ) ds None
-  in
-  Some (r, c)
+  Domains.fold
+    (fun r d best ->
+       let cd = Domain.cardinal d in
+       match Th.embed r, best with
+       | Constr _, _ -> best
+       | _, Some (n, _, _) when n <= cd -> best
+       | _ ->
+         let c = Domain.choose d in
+         Some (cd, r, c)
+    ) ds None
 
-let pick_enum ds uf =
+(* Pick a constructor in a tracked domain whose the domain is of minimal
+   cardinal among tracked domains of enum types. Returns [None] if there is no
+   such constructor. *)
+let pick_enum ds =
   Domains.fold_enums
     (fun r best ->
-       let rr, _ = Uf.find_r uf r in
        let d = Domains.get r ds in
        let cd = Domain.cardinal d in
-       match Th.embed rr, best with
+       match Th.embed r, best with
        | Constr _, _ -> best
        | _, Some (n, _, _) when n <= cd -> best
        | _ ->
@@ -658,11 +657,15 @@ let pick_enum ds uf =
          Some (cd, r, c)
     ) ds None
 
-let split_enum env uf =
+let pick_domain ~for_model uf =
   let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
-  let* n, r, c = pick_enum ds uf in
-  let n = Numbers.Q.from_int n in
-  if can_split env n then
+  match pick_enum ds with
+  | None when for_model -> pick_best ds
+  | r -> r
+
+let split_domain ~for_model env uf =
+  let* cd, r, c = pick_domain ~for_model uf in
+  if for_model || can_split env (Numbers.Q.from_int cd) then
     let _, cons = Option.get @@ build_constr_eq r c in
     let nr, ctx = X.make cons in
     (* In the current implementation of `X.make`, we produce
@@ -674,28 +677,10 @@ let split_enum env uf =
   else
     None
 
-let split_best_domain ~for_model uf =
-  if not for_model then
-    None
-  else
-    let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
-    let* r, c = pick_best ds in
-    let _, cons = Option.get @@ build_constr_eq r c in
-    let nr, ctx = X.make cons in
-    (* In the current implementation of `X.make`, we produce
-       a nonempty context only for interpreted semantic values
-       of the `Arith` and `Records` theories. The semantic
-       values `cons` never involves such values. *)
-    assert (Lists.is_empty ctx);
-    Some (LR.mkv_eq r nr)
-
 let next_case_split ~for_model env uf =
   match split_delayed_destructor env with
-  | Some _ as r -> r
-  | None ->
-    match split_enum env uf with
-    | Some _ as r -> r
-    | None -> split_best_domain ~for_model uf
+  | None -> split_domain ~for_model env uf
+  | r -> r
 
 let case_split env uf ~for_model =
   if Options.get_disable_adts () then