Restore casesplit for enum types in Adt_rel

src/lib/reasoners/adt_rel.ml

@@ -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
@@ -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 =
@@ -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 casesplit by choosing a semantic value [r] and constructor [c]
@@ -627,6 +644,32 @@ let pick_best ds uf =
          Some (cd, r, c)
     ) ds None
 
+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
@@ -638,15 +681,17 @@ let split_best_domain ~for_model uf =
     assert (Lists.is_empty ctx);
     Some (LR.mkv_eq r nr)
 
-let next_casesplit ~for_model env =
+let next_split ~for_model env =
   let open Util in
-  (split_delayed_destructor env) <?> (split_best_domain ~for_model)
+  (split_delayed_destructor env)
+  <?> (split_enum env)
+  <?> (split_best_domain ~for_model)
 
 let case_split env uf ~for_model =
   if Options.get_disable_adts () then
     []
   else begin
-    match next_casesplit ~for_model env uf with
+    match next_split ~for_model env uf with
     | Some cs ->
       if Options.get_debug_adt () then begin
         Debug.pp_domains "before cs"