From c13135f4a78f74bd0524305bf0ce268940e3dca4 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 26 Mar 2024 19:02:18 +0100
Subject: [PATCH 01/15] Refactoring `Enum_rel` using domains on class
 representatives only

This PR refactors the `Enum` relations in order to use a proper type
for the domains of enum semantic values.

Now, we only store domains for class representatives and I believe that the new
implementation is simpler to understand and to maintain.

I don't use the functor `Domains_make` of `Rel_utils` as domain's
propagations performed in `Enum_rel` are much simpler than the propagations in
the BV theory.
---
 src/lib/reasoners/bitv_rel.ml  |   5 +-
 src/lib/reasoners/enum_rel.ml  | 461 ++++++++++++++++-----------------
 src/lib/reasoners/rel_utils.ml | 150 ++++++++++-
 3 files changed, 367 insertions(+), 249 deletions(-)

diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 6b41b2146..778491e80 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -77,7 +77,7 @@ let is_bv_ty = function
 
 let is_bv_r r = is_bv_ty @@ X.type_info r
 
-module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
+module Domain = struct
   (* Note: these functions are not in [Bitlist] proper in order to avoid a
      (direct) dependency from [Bitlist] to the [Shostak] module. *)
 
@@ -124,7 +124,8 @@ module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
         | Ext (r, _r_size, i, j) -> extract (map_signed f r acc) i j
       ) empty (Shostak.Bitv.embed r)
 
-  let unknown = function
+  let unknown r =
+    match X.type_info r with
     | Ty.Tbitv n -> unknown n Ex.empty
     | _ ->
       (* Only bit-vector values can have bitlist domains. *)
diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 391aa95ea..ea433b841 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -28,32 +28,81 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module A  = Xliteral
 module L  = List
-module Hs = Hstring
+module X = Shostak.Combine
+module Ex = Explanation
+module MX = Shostak.MXH
+module SX = Shostak.SXH
+module HSS = Set.Make (Hstring)
+module LR = Uf.LX
+module Th = Shostak.Enum
 
 let timer = Timers.M_Sum
 
-type 'a abstract = 'a Enum.abstract =
-  | Cons of Hs.t * Ty.t
-  | Alien of 'a
+module Domain = struct
+  type t = {
+    constrs : HSS.t;
+    ex : Ex.t;
+  }
 
-module X = Shostak.Combine
-module Sh = Shostak.Enum
+  exception Inconsistent of Ex.t
 
-module Ex = Explanation
+  let[@inline always] cardinal { constrs; _ } = HSS.cardinal constrs
 
-module MX = Shostak.MXH
-module HSS = Set.Make (struct type t=Hs.t let compare = Hs.compare end)
+  let[@inline always] choose { constrs; _ } = HSS.choose constrs
 
-module LR = Uf.LX
+  let domain ~constrs ex =
+    if HSS.is_empty constrs then
+      raise_notrace @@ Inconsistent ex
+    else
+      { constrs; ex }
+
+  let unknown r =
+    match Th.embed r with
+    | Cons (c, _) ->
+      domain ~constrs:(HSS.singleton c) Ex.empty
+    | _ ->
+      match X.type_info r with
+      | Ty.Tsum (_, constrs) ->
+        (* Return the list of all the constructors of the type of [r]. *)
+        let constrs = HSS.of_list constrs in
+        assert (not @@ HSS.is_empty constrs);
+        { constrs; ex = Ex.empty }
+      | _ ->
+        (* Only Enum values can have a domain. This case can happen since we
+           don't dispatch the literals processed in [assume] by their types in
+           the Relation module. *)
+        invalid_arg "unknown"
+
+  let equal d1 d2 = HSS.equal d1.constrs d2.constrs
+
+  let pp ppf d =
+    Fmt.pf ppf "%a"
+      Fmt.(iter ~sep:comma HSS.iter Hstring.print) d.constrs;
+    if Options.(get_verbose () || get_unsat_core ()) then
+      Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
+
+  let intersect ~ex d1 d2 =
+    let constrs = HSS.inter d1.constrs d2.constrs in
+    let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
+    domain ~constrs ex
+
+  let remove ~ex c d =
+    let constrs = HSS.remove c d.constrs in
+    let ex = Ex.union ex d.ex in
+    domain ~constrs ex
+
+  let fold_leaves _f _rr _d _ = assert false
+
+  let map_leaves _f _rr _ = assert false
+end
+
+module Domains = Rel_utils.SimpleDomains_make (Domain)
 
 type t = {
-  (* TODO: rename the field domains to be consistent with the ADT theory. *)
-  mx : (HSS.t * Ex.t) MX.t;
-  (* Map of uninterpreted enum semantic values to domains of their possible
-     values. The explanation justifies that any value assigned to the semantic
-     value has to lie in the domain. *)
+  domains : Domains.t;
+  (* Map of class representatives of enum semantic values to their
+     domains. *)
 
   classes : Expr.Set.t list;
   (* State of the union-find represented by all its equivalence classes.
@@ -68,265 +117,203 @@ type t = {
      [Options.get_max_split ()]. *)
 }
 
-let empty classes = {
-  mx = MX.empty;
-  classes = classes;
-  size_splits = Numbers.Q.one
-}
-
 (*BISECT-IGNORE-BEGIN*)
 module Debug = struct
-  open Printer
-
-  let assume bol r1 r2 =
+  let assume l =
     if Options.get_debug_sum () then
-      print_dbg
-        ~module_name:"Enum_rel" ~function_name:"assume"
-        "we assume %a %s %a"
-        X.print r1 (if bol then "=" else "<>") X.print r2
-
-  let print_env env =
-    if Options.get_debug_sum () then begin
-      Printer.print_dbg ~flushed:false
-        ~module_name:"Enum_rel" ~function_name:"print_env"
-        "@[<v 2>--SUM env ---------------------------------@ ";
-      MX.iter
-        (fun r (hss, ex) ->
-           Printer.print_dbg  ~flushed:false ~header:false
-             "%a ::= " X.print r;
-           begin
-             match HSS.elements hss with
-               []      -> ()
-             | hs :: l ->
-               Printer.print_dbg  ~flushed:false ~header:false
-                 " %s" (Hs.view hs);
-               L.iter (fun hs ->
-                   Printer.print_dbg  ~flushed:false ~header:false
-                     " | %s" (Hs.view hs)) l
-           end;
-           Printer.print_dbg ~flushed:false ~header:false
-             " : %a@ " Ex.print ex;
-        ) env.mx;
-      Printer.print_dbg ~header:false
-        "@ -------------------------------------------";
-    end
-
-  let case_split r r' =
+      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"assume"
+        "assume %a"
+        (Xliteral.print_view X.print) l
+
+  let case_split r1 r2 =
     if Options.get_debug_sum () then
-      Printer.print_dbg
-        ~module_name:"Enum_rel" ~function_name:"case_split"
-        "%a = %a" X.print r X.print r'
+      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split"
+        "%a = %a" X.print r1 X.print r2
 
   let no_case_split () =
     if Options.get_debug_sum () then
-      Printer.print_dbg
-        ~module_name:"Enum_rel" ~function_name:"no_case_split"
-        "sum: nothing"
+      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split"
+        "nothing"
 
   let add r =
     if Options.get_debug_sum () then
-      Printer.print_dbg
-        ~module_name:"Enum_rel" ~function_name:"add"
+      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"add"
         "%a" X.print r
 
+  let pp_env env =
+    if Options.get_debug_sum () then
+      Printer.print_dbg ~module_name:"Enum_rel"
+        "The environment before assuming:@ @[%a@]" Domains.pp env.domains
 end
 (*BISECT-IGNORE-END*)
 
-(* Return the list of all the constructors of the type of [r]. *)
-let values_of r =
-  match X.type_info r with
-  | Ty.Tsum (_,l) ->
-    Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l)
-  | _ ->
-    (* This case can happen since we don't dispatch the literals
-       processed in [assume] by their types in the Relation module. *)
-    None
-
-(* Update the domains of the semantic values [sm1] and [sm2] according to
-   the disequality [sm1 <> sm2]. More precisely, if one of these semantic
-   values is a constructor, we remove it from the domain of the other one.
-
-   In any case, we produce an equality if the domain of one of these semantic
-   values becomes a singleton.
-
-   @raise Ex.Inconsistent if the disequality is inconsistent with the
-   current environment [env]. *)
-let add_diseq hss sm1 sm2 dep env eqs =
-  match sm1, sm2 with
-  | Alien r , Cons(h,ty)
-  | Cons (h,ty), Alien r  ->
-    let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in
-    let enum = HSS.remove h enum in
-    let ex = Ex.union ex dep in
-    if HSS.is_empty enum then raise (Ex.Inconsistent (ex, env.classes))
-    else
-      let env = { env with mx = MX.add r (enum, ex) env.mx } in
-      if HSS.cardinal enum = 1 then
-        let h' = HSS.choose enum in
-        env,
-        (Literal.LSem (LR.mkv_eq r (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else env, eqs
-
-  | Alien r1, Alien r2 ->
-    let enum1,ex1= try MX.find r1 env.mx with Not_found -> hss,Ex.empty in
-    let enum2,ex2= try MX.find r2 env.mx with Not_found -> hss,Ex.empty in
-
-    let eqs =
-      if HSS.cardinal enum1 = 1 then
-        let ex = Ex.union dep ex1 in
-        let h' = HSS.choose enum1 in
-        let ty = X.type_info r1 in
-        (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else eqs
-    in
-    let eqs =
-      if HSS.cardinal enum2 = 1 then
-        let ex = Ex.union dep ex2 in
-        let h' = HSS.choose enum2 in
-        let ty = X.type_info r2 in
-        (Literal.LSem (LR.mkv_eq r2 (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else eqs
-    in
-    env, eqs
-
-  |  _ -> env, eqs
-
-(* Update the domains of the semantic values [sm1] and [sm2] according to
-   the equation [sm1 = sm2]. More precisely, we replace their domains by
-   the intersection of these domains.
-
-   @raise Ex.Inconsistent if the domains of [sm1] and [sm2] are disjoint. *)
-let add_eq hss sm1 sm2 dep env eqs =
-  match sm1, sm2 with
-  | Alien r, Cons(h,_)
-  | Cons (h,_), Alien r  ->
-    let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in
-    let ex = Ex.union ex dep in
-    if not (HSS.mem h enum) then raise (Ex.Inconsistent (ex, env.classes));
-    (* We don't need to produce a new equality as we are already processing
-       it. *)
-    {env with mx = MX.add r (HSS.singleton h, ex) env.mx} , eqs
-
-  | Alien r1, Alien r2   ->
-    let enum1,ex1 =
-      try MX.find r1 env.mx with Not_found -> hss, Ex.empty in
-    let enum2,ex2 =
-      try MX.find r2 env.mx with Not_found -> hss, Ex.empty in
-    let ex = Ex.union dep (Ex.union ex1 ex2) in
-    let diff = HSS.inter enum1 enum2 in
-    if HSS.is_empty diff then raise (Ex.Inconsistent (ex, env.classes));
-    let mx = MX.add r1 (diff, ex) env.mx in
-    let env = {env with mx = MX.add r2 (diff, ex) mx } in
-
-    (* We produce an equality if the domain of these semantic values becomes
-       a singleton. *)
-    if HSS.cardinal diff = 1 then
-      let h' = HSS.choose diff in
-      let ty = X.type_info r1 in
-      env, (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
-            ex, Th_util.Other)::eqs
-    else env, eqs
-
-  |  _ -> env, eqs
+let empty classes = {
+  domains = Domains.empty;
+  classes = classes;
+  size_splits = Numbers.Q.one
+}
 
 (* Update the counter of case-split size in [env]. *)
 let count_splits env la =
   let nb =
     List.fold_left
-      (fun nb (_,_,_,i) ->
+      (fun nb (_, _, _, i) ->
          match i with
          | Th_util.CS (Th_util.Th_sum, n) -> Numbers.Q.mult nb n
          | _ -> nb
-      )env.size_splits la
+      ) env.size_splits la
   in
   {env with size_splits = nb}
 
-(* Add the uninterpreted semantic value [r] to the environment [env] with
-   all the constructors of its type as domain. *)
-let add_aux env r =
-  Debug.add r;
-  match Sh.embed r, values_of r with
-  | Alien r, Some hss ->
-    if MX.mem r env.mx then env else
-      { env with mx = MX.add r (hss, Ex.empty) env.mx }
-  | _ -> env
+let update_domain rr nd env =
+  { env with domains = Domains.update rr nd env.domains }
+
+(* Update the domains of the semantic values [r1] and [r2] according to
+   the substitution `r1 |-> r2`.
+
+   @raise Domain.Inconsistent if this substitution is inconsistent with
+          the current environment [env]. *)
+let assume_subst ~ex r1 r2 env =
+  { env with domains = Domains.subst ~ex r1 r2 env.domains }
+
+(* 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
+   procedure for the Enum 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 haven't enough
+   information to discover this contradiction.
+
+   Now, if we produce a case-split for one of these semantic values,
+   we reach a contradiction for each choice and so our implementation got
+   a complete decision procedure (assuming we have fuel to produce enough
+   case-splits).
+
+   @raise Domain.Inconsistent if the disequality is inconsistent with
+          the current environment [env]. *)
+let assume_distinct ~ex r1 r2 env =
+  let d1 = Domains.get r1 env.domains in
+  let d2 = Domains.get r2 env.domains in
+  let env =
+    if Domain.cardinal d1 = 1 then
+      let c = Domain.choose d1 in
+      let nd = Domain.remove ~ex c d2 in
+      update_domain r2 nd env
+    else
+      env
+  in
+  if Domain.cardinal d2 = 1 then
+    let c = Domain.choose d2 in
+    let nd = Domain.remove ~ex c d1 in
+    update_domain r1 nd env
+  else
+    env
+
+let is_enum r =
+  match X.type_info r with
+  | Ty.Tsum _ -> true
+  | _ -> false
 
-(* Needed for models generation because fresh terms are not added with function
-   add. *)
-let add_rec env r = List.fold_left add_aux env (X.leaves r)
+(* Needed for models generation because fresh terms are not added with the
+   function add. *)
+let add r uf env =
+  match X.type_info r with
+  | Ty.Tsum _ ->
+    Debug.add r;
+    let rr, _ = Uf.find_r uf r in
+    { env with domains = Domains.add rr env.domains }
+  | _ ->
+    env
+
+let add_rec r uf env =
+  List.fold_left (fun env leaf -> add leaf uf env) env (X.leaves r)
+
+let add env uf r _t = add r uf env, []
+
+let assume_literals la uf env =
+  List.fold_left
+    (fun env lit ->
+       let open Xliteral in
+       match lit with
+       | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_enum r1 ->
+         Debug.assume l;
+         let env = add_rec r1 uf env in
+         let env = add_rec r2 uf env in
+         assume_subst ~ex r1 r2 env
+
+       | Distinct (false, [r1; r2]) as l, _, ex, _ when is_enum r2 ->
+         Debug.assume l;
+         let env = add_rec r1 uf env in
+         let env = add_rec r2 uf env in
+         assume_distinct ~ex r1 r2 env
+
+       | _ ->
+         (* We ignore [Eq] literals that aren't substitutions as the propagation
+            of such equalities will produce substitutions later.
+            More precisely, the equation [Eq (r1, r2)] will produce two
+            substitutions:
+              [Eq (r1, rr)] and [Eq (r2, rr)]
+            where [rr] is the new class representative. *)
+         env
+    ) env la
+
+let propagate_domains env =
+  Domains.propagate
+    (fun eqs rr d ->
+       if Domain.cardinal d = 1 then
+         let c = Domain.choose d in
+         let nr = Th.is_mine (Cons (c, X.type_info rr)) in
+         let eq = Literal.LSem (LR.mkv_eq rr nr), d.ex, Th_util.Other in
+         eq :: eqs
+       else
+         eqs
+    ) [] env.domains
 
 let assume env uf la =
+  Debug.pp_env env;
   let env = count_splits env la in
   let classes = Uf.cl_extract uf in
   let env = { env with classes = classes } in
-  let aux bol r1 r2 dep env eqs = function
-    | None     -> env, eqs
-    | Some hss ->
-      Debug.assume bol r1 r2;
-      if bol then
-        add_eq hss (Sh.embed r1) (Sh.embed r2) dep env eqs
-      else
-        add_diseq hss (Sh.embed r1) (Sh.embed r2) dep env eqs
-  in
-  Debug.print_env env;
-  let env, eqs =
-    List.fold_left
-      (fun (env,eqs) -> function
-         | A.Eq(r1,r2), _, ex, _ ->
-           (* needed for models generation because fresh terms are not
-              added with function add *)
-           let env = add_rec (add_rec env r1) r2 in
-           aux true  r1 r2 ex env eqs (values_of r1)
-
-         | A.Distinct(false, [r1;r2]), _, ex, _ ->
-           (* needed for models generation because fresh terms are not
-              added with function add *)
-           let env = add_rec (add_rec env r1) r2 in
-           aux false r1 r2 ex env eqs (values_of r1)
-
-         | _ -> env, eqs
-
-      ) (env,[]) la
+  let env =
+    try
+      assume_literals la uf env
+    with Domain.Inconsistent ex ->
+      raise_notrace (Ex.Inconsistent (ex, env.classes))
   in
-  env, { Sig_rel.assume = eqs; remove = [] }
+  let assume, domains = propagate_domains env in
+  { env with domains }, Sig_rel.{ assume; remove = [] }
 
-let add env _ r _ = add_aux env r, []
+let case_split_limit env n =
+  let m = Options.get_max_split () in
+  Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0
 
-(* Do a case-split by choosing a value for an uninterpreted semantic value
-   whose domain in [env] is of minimal size. *)
+(* Do a case-split by choosing a constructor for class representatives of
+   minimal size. *)
 let case_split env uf ~for_model =
-  let acc = MX.fold
-      (fun r (hss, _) acc ->
-         let x, _ = Uf.find_r uf r in
-         match Sh.embed x with
-         | Cons _ ->
-           (* The equivalence class of [r] already contains a value so
-              we don't need to make another case-split for this semantic
-              value. *)
-           acc
-         | _ ->
-           (* We have to perform a case-split, even if the domain of [r] is
-              of cardinal 1 as we have to let the union-find know this
-              equality. *)
-           let sz = HSS.cardinal hss in
-           match acc with
-           | Some (n,_,_) when n <= sz -> acc
-           | _ -> Some (sz, r, HSS.choose hss)
-      ) env.mx None
+  let best =
+    Domains.fold (fun r d best ->
+        let rr, _ = Uf.find_r uf r in
+        match Th.embed rr with
+        | Cons _ ->
+          (* The equivalence class of [r] already contains a model term so
+             we don't need to make another case-split for this semantic
+             value. *)
+          best
+        | _ ->
+          let cd = Domain.cardinal d in
+          match best with
+          | Some (n, _, _) when n <= cd -> best
+          | _ -> Some (cd, r, Domain.choose d)
+      ) env.domains None
   in
-  match acc with
-  | Some (n,r,hs) ->
+  match best with
+  | Some (n, r, c) ->
     let n = Numbers.Q.from_int n in
-    if for_model ||
-       Numbers.Q.compare
-         (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0  ||
-       Numbers.Q.sign  (Options.get_max_split ()) < 0 then
-      let r' = Sh.is_mine (Cons(hs,X.type_info r)) in
-      Debug.case_split r r';
-      [LR.mkv_eq r r', true, Th_util.CS (Th_util.Th_sum, n)]
+    if for_model || case_split_limit env n then
+      let nr = Th.is_mine (Cons (c, X.type_info r)) in
+      Debug.case_split r nr;
+      [LR.mkv_eq r nr, true, Th_util.CS (Th_util.Th_sum, n)]
     else
       []
   | None ->
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index fb17f1528..a40bfff3c 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -214,13 +214,8 @@ module type Domain = sig
   exception Inconsistent of Explanation.t
   (** Exception raised by [intersect] when an inconsistency is detected. *)
 
-  val unknown : Ty.t -> t
-  (** [unknown ty] returns a full domain for values of type [t]. *)
-
-  val add_explanation : ex:Explanation.t -> t -> t
-  (** [add_explanation ~ex d] adds the justification [ex] to the domain d. The
-      returned domain is identical to the domain of [d], only the
-      justifications are changed. *)
+  val unknown : X.r -> t
+  (** [unknown r] returns a full domain for values of the semantic value [r]. *)
 
   val intersect : ex:Explanation.t -> t -> t -> t
   (** [intersect ~ex d1 d2] returns a new domain [d] that subsumes both [d1]
@@ -250,7 +245,7 @@ end
 module type Domains = sig
   type t
   (** The type of domain maps. A domain map maps each representative (semantic
-      value, of type [X.r]) to its associated domain.*)
+      value, of type [X.r]) to its associated domain. *)
 
   val pp : t Fmt.t
   (** Pretty-printer for domain maps. *)
@@ -269,7 +264,7 @@ module type Domains = sig
   val add : X.r -> t -> t
   (** [add r t] adds a domain for [r] in the domain map. If [r] does not
       already have an associated domain, a fresh domain will be created for
-      [r]. *)
+      [r] using [Domain.unknown]. *)
 
   val get : X.r -> t -> elt
   (** [get r t] returns the domain currently associated with [r] in [t]. *)
@@ -398,7 +393,7 @@ struct
 
   let create_domain r =
     Domain.map_leaves (fun r () ->
-        Domain.unknown (X.type_info r)
+        Domain.unknown r
       ) r ()
 
   let add r t =
@@ -623,6 +618,141 @@ struct
       ) t.Ephemeral.dirty_cache t.persistent
 end
 
+(** Simplified version of [Domains_make] used by theories that perform
+    only one step of propagation.
+
+    The input [Domain] doesn't need to implement [fold_leaves] or
+    [map_leaves]. *)
+module SimpleDomains_make (Domain : Domain) : sig
+  type t
+  (** The type of simple domain maps. A domain map maps each representative
+      (semantic value, of type [X.r]) to its associated domain. *)
+
+  val pp : t Fmt.t
+  (** Pretty-printer for domain maps. *)
+
+  val empty : t
+  (** The empty domain map. *)
+
+  type elt = Domain.t
+  (** The type of domains contained in the map. Each domain of type [elt]
+      applies to a single semantic value. *)
+
+  exception Inconsistent of Explanation.t
+  (** Exception raised by [update] or [subst] when an inconsistency is
+      detected. *)
+
+  val add : X.r -> t -> t
+  (** [add r t] adds a domain for [r] in the domain map. If [r] does not
+      already have an associated domain, a fresh domain will be created for
+      [r] using [Domain.unknown]. *)
+
+  val get : X.r -> t -> elt
+  (** [get r t] returns the domain currently associated with [r] in [t]. *)
+
+  val subst : ex:Explanation.t -> X.r -> X.r -> t -> t
+  (** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
+      domains, merging the corresponding domains as appropriate.
+
+      The explanation [ex] justifies the equality [p = v].
+
+      @raise Domain.Inconsistent if this causes any domain in [d] to become
+             empty. *)
+
+  val update : X.r -> elt -> t -> t
+  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
+      representative [r] is marked [changed] after this call. *)
+
+  val propagate : ('a -> X.r -> elt -> 'a) -> 'a -> t -> 'a * t
+  (* [propagate f a t] iterates on all the changed domains of [t] since the
+     last call of [propagate]. The list of changed domains is flushed after
+     this call. *)
+
+  val fold : (X.r -> elt -> 'a -> 'a) -> t -> 'a -> 'a
+  (* [fold f t a] iterates on all the domains of [t]. *)
+end = struct
+  type elt = Domain.t
+
+  exception Inconsistent = Domain.Inconsistent
+
+  type t = {
+    domains : Domain.t MX.t;
+    (** Map from tracked representatives to their domain. *)
+
+    changed : SX.t;
+    (** Representatives whose domain has changed since the last flush
+        in [propagation]. *)
+  }
+
+  let pp ppf t =
+    Fmt.(iter_bindings ~sep:semi MX.iter
+           (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
+         |> braces
+        )
+      ppf t.domains
+
+  let empty = { domains = MX.empty; changed = SX.empty }
+
+  let internal_update r nd t =
+    let domains = MX.add r nd t.domains in
+    let changed = SX.add r t.changed in
+    { domains; changed }
+
+  let add r t =
+    match MX.find r t.domains with
+    | _ -> t
+    | exception Not_found ->
+      let nd = Domain.unknown r in
+      internal_update r nd t
+
+  let update r d t =
+    match MX.find r t.domains with
+    | od ->
+      let nd = Domain.intersect ~ex:Explanation.empty od d in
+      if Domain.equal od nd then
+        t
+      else
+        internal_update r nd t
+
+    | exception Not_found ->
+      let nd = Domain.intersect ~ex:Explanation.empty (Domain.unknown r) d in
+      internal_update r nd t
+
+  let get r t =
+    try MX.find r t.domains
+    with Not_found -> Domain.unknown r
+
+  let remove r t =
+    let domains = MX.remove r t.domains in
+    let changed = SX.remove r t.changed in
+    { domains ; changed }
+
+  let subst ~ex r nr t =
+    match MX.find r t.domains with
+    | d ->
+      let nnd =
+        match MX.find nr t.domains with
+        | nd -> Domain.intersect ~ex d nd
+        | exception Not_found -> d
+      in
+      let t = remove r t in
+      internal_update nr nnd t
+
+    | exception Not_found -> t
+
+  let fold f t acc = MX.fold f t.domains acc
+
+  let propagate f acc t =
+    let acc =
+      SX.fold
+        (fun r acc ->
+           let d = get r t in
+           f acc r d
+        ) t.changed acc
+    in
+    acc, { t with changed = SX.empty }
+end
+
 (** The ['c acts] type is used to register new facts and constraints in
     [Constraint.simplify]. *)
 type 'c acts =

From 60570226d9332963dd0c8543dcd1cb0e6ceb5678 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 3 Apr 2024 13:39:52 +0200
Subject: [PATCH 02/15] Use stubs for `fold_leaves` and `map_leaves`

---
 src/lib/reasoners/enum_rel.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index ea433b841..6abf423b5 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -92,9 +92,9 @@ module Domain = struct
     let ex = Ex.union ex d.ex in
     domain ~constrs ex
 
-  let fold_leaves _f _rr _d _ = assert false
+  let fold_leaves f r d acc = f r d acc
 
-  let map_leaves _f _rr _ = assert false
+  let map_leaves f r acc = f r acc
 end
 
 module Domains = Rel_utils.SimpleDomains_make (Domain)

From 5707aabd56def0960b2aab20d9abdf5b282b33fe Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 3 Apr 2024 13:41:11 +0200
Subject: [PATCH 03/15] Move the comment

---
 src/lib/reasoners/enum_rel.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 6abf423b5..c6b84da8e 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -215,8 +215,6 @@ let is_enum r =
   | Ty.Tsum _ -> true
   | _ -> false
 
-(* Needed for models generation because fresh terms are not added with the
-   function add. *)
 let add r uf env =
   match X.type_info r with
   | Ty.Tsum _ ->
@@ -238,12 +236,16 @@ let assume_literals la uf env =
        match lit with
        | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_enum r1 ->
          Debug.assume l;
+         (* Needed for models generation because fresh terms are not added with
+            the function add. *)
          let env = add_rec r1 uf env in
          let env = add_rec r2 uf env in
          assume_subst ~ex r1 r2 env
 
        | Distinct (false, [r1; r2]) as l, _, ex, _ when is_enum r2 ->
          Debug.assume l;
+         (* Needed for models generation because fresh terms are not added with
+            the function add. *)
          let env = add_rec r1 uf env in
          let env = add_rec r2 uf env in
          assume_distinct ~ex r1 r2 env

From d9ad40baa39edf41b872bd797b53cba5db02ab69 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 3 Apr 2024 13:49:22 +0200
Subject: [PATCH 04/15] Add `as_singleton` in `Domain`

---
 src/lib/reasoners/enum_rel.ml | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index c6b84da8e..90655c51c 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -51,6 +51,12 @@ module Domain = struct
 
   let[@inline always] choose { constrs; _ } = HSS.choose constrs
 
+  let[@inline always] as_singleton { constrs; _ } =
+    if HSS.cardinal constrs = 1 then
+      Some (HSS.choose constrs)
+    else
+      None
+
   let domain ~constrs ex =
     if HSS.is_empty constrs then
       raise_notrace @@ Inconsistent ex
@@ -196,18 +202,18 @@ let assume_distinct ~ex r1 r2 env =
   let d1 = Domains.get r1 env.domains in
   let d2 = Domains.get r2 env.domains in
   let env =
-    if Domain.cardinal d1 = 1 then
-      let c = Domain.choose d1 in
+    match Domain.as_singleton d1 with
+    | Some c ->
       let nd = Domain.remove ~ex c d2 in
       update_domain r2 nd env
-    else
+    | None ->
       env
   in
-  if Domain.cardinal d2 = 1 then
-    let c = Domain.choose d2 in
+  match Domain.as_singleton d2 with
+  | Some c ->
     let nd = Domain.remove ~ex c d1 in
     update_domain r1 nd env
-  else
+  | None ->
     env
 
 let is_enum r =
@@ -263,12 +269,12 @@ let assume_literals la uf env =
 let propagate_domains env =
   Domains.propagate
     (fun eqs rr d ->
-       if Domain.cardinal d = 1 then
-         let c = Domain.choose d in
+       match Domain.as_singleton d with
+       | Some c ->
          let nr = Th.is_mine (Cons (c, X.type_info rr)) in
          let eq = Literal.LSem (LR.mkv_eq rr nr), d.ex, Th_util.Other in
          eq :: eqs
-       else
+       | None ->
          eqs
     ) [] env.domains
 

From 02b864580b492537e74df2389d55515dad135daa Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 3 Apr 2024 13:50:01 +0200
Subject: [PATCH 05/15] Rename `case_split_limit` to `can_split`

---
 src/lib/reasoners/enum_rel.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 90655c51c..6b5c00a8a 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -292,7 +292,7 @@ let assume env uf la =
   let assume, domains = propagate_domains env in
   { env with domains }, Sig_rel.{ assume; remove = [] }
 
-let case_split_limit env n =
+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
 
@@ -318,7 +318,7 @@ let case_split env uf ~for_model =
   match best with
   | Some (n, r, c) ->
     let n = Numbers.Q.from_int n in
-    if for_model || case_split_limit env n then
+    if for_model || can_split env n then
       let nr = Th.is_mine (Cons (c, X.type_info r)) in
       Debug.case_split r nr;
       [LR.mkv_eq r nr, true, Th_util.CS (Th_util.Th_sum, n)]

From 2c27bcc960c320e546f4ce13c484ae1450bfb830 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 3 Apr 2024 14:08:13 +0200
Subject: [PATCH 06/15] Inline the function SimpleDomains in `Enum_rel`

---
 src/lib/reasoners/enum_rel.ml  | 103 ++++++++++++++++++++++++-
 src/lib/reasoners/rel_utils.ml | 135 ---------------------------------
 2 files changed, 99 insertions(+), 139 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 6b5c00a8a..3fc7ca1ca 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -97,13 +97,108 @@ module Domain = struct
     let constrs = HSS.remove c d.constrs in
     let ex = Ex.union ex d.ex in
     domain ~constrs ex
+end
 
-  let fold_leaves f r d acc = f r d acc
+module Domains = struct
+  exception Inconsistent = Domain.Inconsistent
+  (** Exception raised by [update] or [subst] when an inconsistency is
+      detected. *)
 
-  let map_leaves f r acc = f r acc
-end
+  (** The type of simple domain maps. A domain map maps each representative
+      (semantic value, of type [X.r]) to its associated domain. *)
+  type t = {
+    domains : Domain.t MX.t;
+    (** Map from tracked representatives to their domain. *)
 
-module Domains = Rel_utils.SimpleDomains_make (Domain)
+    changed : SX.t;
+    (** Representatives whose domain has changed since the last flush
+        in [propagation]. *)
+  }
+
+  let pp ppf t =
+    Fmt.(iter_bindings ~sep:semi MX.iter
+           (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
+         |> braces
+        )
+      ppf t.domains
+
+  let empty = { domains = MX.empty; changed = SX.empty }
+
+  let internal_update r nd t =
+    let domains = MX.add r nd t.domains in
+    let changed = SX.add r t.changed in
+    { domains; changed }
+
+  (** [add r t] adds a domain for [r] in the domain map. If [r] does not
+      already have an associated domain, a fresh domain will be created for
+      [r] using [Domain.unknown]. *)
+  let add r t =
+    match MX.find r t.domains with
+    | _ -> t
+    | exception Not_found ->
+      let nd = Domain.unknown r in
+      internal_update r nd t
+
+  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
+      representative [r] is marked [changed] after this call. *)
+  let update r d t =
+    match MX.find r t.domains with
+    | od ->
+      let nd = Domain.intersect ~ex:Explanation.empty od d in
+      if Domain.equal od nd then
+        t
+      else
+        internal_update r nd t
+
+    | exception Not_found ->
+      let nd = Domain.intersect ~ex:Explanation.empty (Domain.unknown r) d in
+      internal_update r nd t
+
+  (** [get r t] returns the domain currently associated with [r] in [t]. *)
+  let get r t =
+    try MX.find r t.domains
+    with Not_found -> Domain.unknown r
+
+  let remove r t =
+    let domains = MX.remove r t.domains in
+    let changed = SX.remove r t.changed in
+    { domains ; changed }
+
+  (** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
+      domains, merging the corresponding domains as appropriate.
+
+      The explanation [ex] justifies the equality [p = v].
+
+      @raise Domain.Inconsistent if this causes any domain in [d] to become
+             empty. *)
+  let subst ~ex r nr t =
+    match MX.find r t.domains with
+    | d ->
+      let nnd =
+        match MX.find nr t.domains with
+        | nd -> Domain.intersect ~ex d nd
+        | exception Not_found -> d
+      in
+      let t = remove r t in
+      internal_update nr nnd t
+
+    | exception Not_found -> t
+
+  let fold f t acc = MX.fold f t.domains acc
+
+  (* [propagate f a t] iterates on all the changed domains of [t] since the
+     last call of [propagate]. The list of changed domains is flushed after
+     this call. *)
+  let propagate f acc t =
+    let acc =
+      SX.fold
+        (fun r acc ->
+           let d = get r t in
+           f acc r d
+        ) t.changed acc
+    in
+    acc, { t with changed = SX.empty }
+end
 
 type t = {
   domains : Domains.t;
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index a40bfff3c..5575c91d9 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -618,141 +618,6 @@ struct
       ) t.Ephemeral.dirty_cache t.persistent
 end
 
-(** Simplified version of [Domains_make] used by theories that perform
-    only one step of propagation.
-
-    The input [Domain] doesn't need to implement [fold_leaves] or
-    [map_leaves]. *)
-module SimpleDomains_make (Domain : Domain) : sig
-  type t
-  (** The type of simple domain maps. A domain map maps each representative
-      (semantic value, of type [X.r]) to its associated domain. *)
-
-  val pp : t Fmt.t
-  (** Pretty-printer for domain maps. *)
-
-  val empty : t
-  (** The empty domain map. *)
-
-  type elt = Domain.t
-  (** The type of domains contained in the map. Each domain of type [elt]
-      applies to a single semantic value. *)
-
-  exception Inconsistent of Explanation.t
-  (** Exception raised by [update] or [subst] when an inconsistency is
-      detected. *)
-
-  val add : X.r -> t -> t
-  (** [add r t] adds a domain for [r] in the domain map. If [r] does not
-      already have an associated domain, a fresh domain will be created for
-      [r] using [Domain.unknown]. *)
-
-  val get : X.r -> t -> elt
-  (** [get r t] returns the domain currently associated with [r] in [t]. *)
-
-  val subst : ex:Explanation.t -> X.r -> X.r -> t -> t
-  (** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
-      domains, merging the corresponding domains as appropriate.
-
-      The explanation [ex] justifies the equality [p = v].
-
-      @raise Domain.Inconsistent if this causes any domain in [d] to become
-             empty. *)
-
-  val update : X.r -> elt -> t -> t
-  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
-      representative [r] is marked [changed] after this call. *)
-
-  val propagate : ('a -> X.r -> elt -> 'a) -> 'a -> t -> 'a * t
-  (* [propagate f a t] iterates on all the changed domains of [t] since the
-     last call of [propagate]. The list of changed domains is flushed after
-     this call. *)
-
-  val fold : (X.r -> elt -> 'a -> 'a) -> t -> 'a -> 'a
-  (* [fold f t a] iterates on all the domains of [t]. *)
-end = struct
-  type elt = Domain.t
-
-  exception Inconsistent = Domain.Inconsistent
-
-  type t = {
-    domains : Domain.t MX.t;
-    (** Map from tracked representatives to their domain. *)
-
-    changed : SX.t;
-    (** Representatives whose domain has changed since the last flush
-        in [propagation]. *)
-  }
-
-  let pp ppf t =
-    Fmt.(iter_bindings ~sep:semi MX.iter
-           (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
-         |> braces
-        )
-      ppf t.domains
-
-  let empty = { domains = MX.empty; changed = SX.empty }
-
-  let internal_update r nd t =
-    let domains = MX.add r nd t.domains in
-    let changed = SX.add r t.changed in
-    { domains; changed }
-
-  let add r t =
-    match MX.find r t.domains with
-    | _ -> t
-    | exception Not_found ->
-      let nd = Domain.unknown r in
-      internal_update r nd t
-
-  let update r d t =
-    match MX.find r t.domains with
-    | od ->
-      let nd = Domain.intersect ~ex:Explanation.empty od d in
-      if Domain.equal od nd then
-        t
-      else
-        internal_update r nd t
-
-    | exception Not_found ->
-      let nd = Domain.intersect ~ex:Explanation.empty (Domain.unknown r) d in
-      internal_update r nd t
-
-  let get r t =
-    try MX.find r t.domains
-    with Not_found -> Domain.unknown r
-
-  let remove r t =
-    let domains = MX.remove r t.domains in
-    let changed = SX.remove r t.changed in
-    { domains ; changed }
-
-  let subst ~ex r nr t =
-    match MX.find r t.domains with
-    | d ->
-      let nnd =
-        match MX.find nr t.domains with
-        | nd -> Domain.intersect ~ex d nd
-        | exception Not_found -> d
-      in
-      let t = remove r t in
-      internal_update nr nnd t
-
-    | exception Not_found -> t
-
-  let fold f t acc = MX.fold f t.domains acc
-
-  let propagate f acc t =
-    let acc =
-      SX.fold
-        (fun r acc ->
-           let d = get r t in
-           f acc r d
-        ) t.changed acc
-    in
-    acc, { t with changed = SX.empty }
-end
-
 (** The ['c acts] type is used to register new facts and constraints in
     [Constraint.simplify]. *)
 type 'c acts =

From 1e0deb74d9380185c9b4c71254ba37883fc17c3f Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 11:39:39 +0200
Subject: [PATCH 07/15] Fix comment about the `unknown` function of `Domain`

---
 src/lib/reasoners/enum_rel.ml | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 3fc7ca1ca..1bd5c80e3 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -75,16 +75,16 @@ module Domain = struct
         assert (not @@ HSS.is_empty constrs);
         { constrs; ex = Ex.empty }
       | _ ->
-        (* Only Enum values can have a domain. This case can happen since we
-           don't dispatch the literals processed in [assume] by their types in
-           the Relation module. *)
-        invalid_arg "unknown"
+        (* Only Enum values can have a domain. This case shouldn't happen since
+           we check the type of [r] in [add] and [assume] functions of this
+           module. *)
+        assert false
 
   let equal d1 d2 = HSS.equal d1.constrs d2.constrs
 
   let pp ppf d =
-    Fmt.pf ppf "%a"
-      Fmt.(iter ~sep:comma HSS.iter Hstring.print) d.constrs;
+    Fmt.(braces @@
+         iter ~sep:comma HSS.iter Hstring.print) ppf d.constrs;
     if Options.(get_verbose () || get_unsat_core ()) then
       Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
 
@@ -100,10 +100,6 @@ module Domain = struct
 end
 
 module Domains = struct
-  exception Inconsistent = Domain.Inconsistent
-  (** Exception raised by [update] or [subst] when an inconsistency is
-      detected. *)
-
   (** The type of simple domain maps. A domain map maps each representative
       (semantic value, of type [X.r]) to its associated domain. *)
   type t = {

From 2b0e898a1b5a31c7ba171a8bfd27fe37bc41aac0 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 11:42:56 +0200
Subject: [PATCH 08/15] Revert the modification of `unknown` in `Rel_utils`

---
 src/lib/reasoners/bitv_rel.ml  | 4 ++--
 src/lib/reasoners/rel_utils.ml | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 778491e80..f3f996eef 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -124,8 +124,8 @@ module Domain = struct
         | Ext (r, _r_size, i, j) -> extract (map_signed f r acc) i j
       ) empty (Shostak.Bitv.embed r)
 
-  let unknown r =
-    match X.type_info r with
+  let unknown ty =
+    match ty with
     | Ty.Tbitv n -> unknown n Ex.empty
     | _ ->
       (* Only bit-vector values can have bitlist domains. *)
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index 5575c91d9..b530b95af 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -214,8 +214,8 @@ module type Domain = sig
   exception Inconsistent of Explanation.t
   (** Exception raised by [intersect] when an inconsistency is detected. *)
 
-  val unknown : X.r -> t
-  (** [unknown r] returns a full domain for values of the semantic value [r]. *)
+  val unknown : Ty.t -> t
+  (** [unknown ty] returns a full domain for values of type [t]. *)
 
   val intersect : ex:Explanation.t -> t -> t -> t
   (** [intersect ~ex d1 d2] returns a new domain [d] that subsumes both [d1]
@@ -393,7 +393,7 @@ struct
 
   let create_domain r =
     Domain.map_leaves (fun r () ->
-        Domain.unknown r
+        Domain.unknown (X.type_info r)
       ) r ()
 
   let add r t =

From 1a70ddf94b26de79cc0fff3d36feb9f12f10aeaf Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 12:05:42 +0200
Subject: [PATCH 09/15] Preserve default domain during updates

The previous implementation of `Domain.update` could replace a default
domain (with the empty explanation) by a default one with a non-empty
explanation. There is no reason to add these extra explanations.

This new implementation doesn't update the map `t.domains` if the
intersection is a default domain. It means `update` doesn't add a domain
if `d` is a default domain and `r` isn't in the map, which is ok as we
ensure that all seen semantic values are added to `t.domains` in `assume`.
---
 src/lib/reasoners/enum_rel.ml | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 1bd5c80e3..e03787c57 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -135,26 +135,21 @@ module Domains = struct
       let nd = Domain.unknown r in
       internal_update r nd t
 
-  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
-      representative [r] is marked [changed] after this call. *)
-  let update r d t =
-    match MX.find r t.domains with
-    | od ->
-      let nd = Domain.intersect ~ex:Explanation.empty od d in
-      if Domain.equal od nd then
-        t
-      else
-        internal_update r nd t
-
-    | exception Not_found ->
-      let nd = Domain.intersect ~ex:Explanation.empty (Domain.unknown r) d in
-      internal_update r nd t
-
   (** [get r t] returns the domain currently associated with [r] in [t]. *)
   let get r t =
     try MX.find r t.domains
     with Not_found -> Domain.unknown r
 
+  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
+      representative [r] is marked [changed] after this call. *)
+  let update r d t =
+    let od = get r t in
+    let nd = Domain.intersect ~ex:Explanation.empty od d in
+    if Domain.equal od nd then
+      t
+    else
+      internal_update r nd t
+
   let remove r t =
     let domains = MX.remove r t.domains in
     let changed = SX.remove r t.changed in

From e0a1c8fa0f0344db20ea081de362df7c8bcc0a81 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 12:17:38 +0200
Subject: [PATCH 10/15] Rename `unknown` into `default`

The `unknown` function in `Enum_rel` doesn't return the full domain
for constructor semantic values but the tightest possible domain for it.
The `default` name is more appropriate for this behaviour.
---
 src/lib/reasoners/enum_rel.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index e03787c57..421161721 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -63,7 +63,7 @@ module Domain = struct
     else
       { constrs; ex }
 
-  let unknown r =
+  let default r =
     match Th.embed r with
     | Cons (c, _) ->
       domain ~constrs:(HSS.singleton c) Ex.empty
@@ -127,18 +127,18 @@ module Domains = struct
 
   (** [add r t] adds a domain for [r] in the domain map. If [r] does not
       already have an associated domain, a fresh domain will be created for
-      [r] using [Domain.unknown]. *)
+      [r] using [Domain.default]. *)
   let add r t =
     match MX.find r t.domains with
     | _ -> t
     | exception Not_found ->
-      let nd = Domain.unknown r in
+      let nd = Domain.default r in
       internal_update r nd t
 
   (** [get r t] returns the domain currently associated with [r] in [t]. *)
   let get r t =
     try MX.find r t.domains
-    with Not_found -> Domain.unknown r
+    with Not_found -> Domain.default r
 
   (** [update r d t] replaces the domain of [r] in [t] by [d]. The
       representative [r] is marked [changed] after this call. *)

From 2e0a16ce17bf2a9ab6c5fa66b04e30656f7d501a Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 12:41:05 +0200
Subject: [PATCH 11/15] Improve efficency of `get` and `add`

As we inlined the function `SimpleDomains_make` in `Enum_rel`, we can
write more efficient code for this theory.

We don't need to look in the map `t.domains` for constructor semantic
values as we always produce the same default domain for them, that is
a singleton without any explanation.
---
 src/lib/reasoners/enum_rel.ml | 54 +++++++++++++++++++++--------------
 1 file changed, 32 insertions(+), 22 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 421161721..d6df3f85c 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -63,22 +63,19 @@ module Domain = struct
     else
       { constrs; ex }
 
-  let default r =
-    match Th.embed r with
-    | Cons (c, _) ->
-      domain ~constrs:(HSS.singleton c) Ex.empty
+  let[@inline always] singleton ~ex c = { constrs = HSS.singleton c; ex }
+
+  let unknown ty =
+    match ty with
+    | Ty.Tsum (_, constrs) ->
+      (* Return the list of all the constructors of the type of [r]. *)
+      let constrs = HSS.of_list constrs in
+      assert (not @@ HSS.is_empty constrs);
+      { constrs; ex = Ex.empty }
     | _ ->
-      match X.type_info r with
-      | Ty.Tsum (_, constrs) ->
-        (* Return the list of all the constructors of the type of [r]. *)
-        let constrs = HSS.of_list constrs in
-        assert (not @@ HSS.is_empty constrs);
-        { constrs; ex = Ex.empty }
-      | _ ->
-        (* Only Enum values can have a domain. This case shouldn't happen since
-           we check the type of [r] in [add] and [assume] functions of this
-           module. *)
-        assert false
+      (* Only Enum values can have a domain. This case shouldn't happen since
+         we check the type of semantic values in both [add] and [assume]. *)
+      assert false
 
   let equal d1 d2 = HSS.equal d1.constrs d2.constrs
 
@@ -125,21 +122,34 @@ module Domains = struct
     let changed = SX.add r t.changed in
     { domains; changed }
 
+  (** [get r t] returns the domain currently associated with [r] in [t]. *)
+  let get r t =
+    match Th.embed r with
+    | Cons (r, _) ->
+      (* For sake of efficiency, we don't look in the map if the
+         semantic value is a constructor. *)
+      Domain.singleton ~ex:Explanation.empty r
+    | _ ->
+      try MX.find r t.domains
+      with Not_found ->
+        Domain.unknown (X.type_info r)
+
   (** [add r t] adds a domain for [r] in the domain map. If [r] does not
       already have an associated domain, a fresh domain will be created for
-      [r] using [Domain.default]. *)
+      [r] and add to the map. *)
   let add r t =
     match MX.find r t.domains with
     | _ -> t
     | exception Not_found ->
-      let nd = Domain.default r in
+      let nd =
+        match Th.embed r with
+        | Cons (r, _) ->
+          Domain.singleton ~ex:Explanation.empty r
+        | _ ->
+          Domain.unknown (X.type_info r)
+      in
       internal_update r nd t
 
-  (** [get r t] returns the domain currently associated with [r] in [t]. *)
-  let get r t =
-    try MX.find r t.domains
-    with Not_found -> Domain.default r
-
   (** [update r d t] replaces the domain of [r] in [t] by [d]. The
       representative [r] is marked [changed] after this call. *)
   let update r d t =

From 03c5af7cc94cdb75136f924b7e91e68db62215c8 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 13:13:48 +0200
Subject: [PATCH 12/15] No intersection in `update`

We don't need to perform an intersection in `Domain.update` as we always
call it on domains that are subsets of the old ones.
---
 src/lib/reasoners/enum_rel.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index d6df3f85c..e311a9d72 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -151,14 +151,14 @@ module Domains = struct
       internal_update r nd t
 
   (** [update r d t] replaces the domain of [r] in [t] by [d]. The
-      representative [r] is marked [changed] after this call. *)
+      representative [r] is marked [changed] after this call if the domain
+      [d] isn't equal to the old one. *)
   let update r d t =
     let od = get r t in
-    let nd = Domain.intersect ~ex:Explanation.empty od d in
-    if Domain.equal od nd then
+    if Domain.equal od d then
       t
     else
-      internal_update r nd t
+      internal_update r d t
 
   let remove r t =
     let domains = MX.remove r t.domains in

From 9e1aed03e55401a9bc5e399493a61c328157e091 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 13:18:37 +0200
Subject: [PATCH 13/15] Restore bitv_rel and rel_utils

---
 src/lib/reasoners/bitv_rel.ml  | 5 ++---
 src/lib/reasoners/rel_utils.ml | 5 +++++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index f3f996eef..6b41b2146 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -77,7 +77,7 @@ let is_bv_ty = function
 
 let is_bv_r r = is_bv_ty @@ X.type_info r
 
-module Domain = struct
+module Domain : Rel_utils.Domain with type t = Bitlist.t = struct
   (* Note: these functions are not in [Bitlist] proper in order to avoid a
      (direct) dependency from [Bitlist] to the [Shostak] module. *)
 
@@ -124,8 +124,7 @@ module Domain = struct
         | Ext (r, _r_size, i, j) -> extract (map_signed f r acc) i j
       ) empty (Shostak.Bitv.embed r)
 
-  let unknown ty =
-    match ty with
+  let unknown = function
     | Ty.Tbitv n -> unknown n Ex.empty
     | _ ->
       (* Only bit-vector values can have bitlist domains. *)
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index b530b95af..23232ae7b 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -217,6 +217,11 @@ module type Domain = sig
   val unknown : Ty.t -> t
   (** [unknown ty] returns a full domain for values of type [t]. *)
 
+  val add_explanation : ex:Explanation.t -> t -> t
+  (** [add_explanation ~ex d] adds the justification [ex] to the domain d. The
+      returned domain is identical to the domain of [d], only the
+      justifications are changed. *)
+
   val intersect : ex:Explanation.t -> t -> t -> t
   (** [intersect ~ex d1 d2] returns a new domain [d] that subsumes both [d1]
       and [d2]. The explanation [ex] justifies that the two domains can be

From 0a22844063fb87d2383b4aa570d44e21e7362be9 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 13:51:17 +0200
Subject: [PATCH 14/15] Add comments

---
 src/lib/reasoners/enum_rel.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index e311a9d72..2d348f606 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -65,6 +65,8 @@ module Domain = struct
 
   let[@inline always] singleton ~ex c = { constrs = HSS.singleton c; ex }
 
+  let[@inline always] subset d1 d2 = HSS.subset d1.constrs d2.constrs
+
   let unknown ty =
     match ty with
     | Ty.Tsum (_, constrs) ->
@@ -122,7 +124,6 @@ module Domains = struct
     let changed = SX.add r t.changed in
     { domains; changed }
 
-  (** [get r t] returns the domain currently associated with [r] in [t]. *)
   let get r t =
     match Th.embed r with
     | Cons (r, _) ->
@@ -134,13 +135,13 @@ module Domains = struct
       with Not_found ->
         Domain.unknown (X.type_info r)
 
-  (** [add r t] adds a domain for [r] in the domain map. If [r] does not
-      already have an associated domain, a fresh domain will be created for
-      [r] and add to the map. *)
   let add r t =
     match MX.find r t.domains with
     | _ -> t
     | exception Not_found ->
+      (* 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. *)
       let nd =
         match Th.embed r with
         | Cons (r, _) ->
@@ -155,6 +156,9 @@ module Domains = struct
       [d] isn't equal to the old one. *)
   let update r d t =
     let od = get r t in
+    (* For sake of completeness, the domain [d] has to be a subset
+       of the old domain of [r]. *)
+    assert (not (Options.get_enable_assertions ()) || Domain.subset d od);
     if Domain.equal od d then
       t
     else

From de7645ef205c0a7d528fe5538e6bc220284dcdf5 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 4 Apr 2024 16:38:02 +0200
Subject: [PATCH 15/15] Review changes

---
 src/lib/reasoners/enum_rel.ml | 58 ++++++++++++++++-------------------
 1 file changed, 26 insertions(+), 32 deletions(-)

diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 2d348f606..31f2cd0d2 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -103,7 +103,9 @@ module Domains = struct
       (semantic value, of type [X.r]) to its associated domain. *)
   type t = {
     domains : Domain.t MX.t;
-    (** Map from tracked representatives to their domain. *)
+    (** Map from tracked representatives to their domain.
+
+        We don't store domains for constructors. *)
 
     changed : SX.t;
     (** Representatives whose domain has changed since the last flush
@@ -136,28 +138,24 @@ module Domains = struct
         Domain.unknown (X.type_info r)
 
   let add r t =
-    match MX.find r t.domains with
-    | _ -> t
-    | exception Not_found ->
-      (* 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. *)
-      let nd =
-        match Th.embed r with
-        | Cons (r, _) ->
-          Domain.singleton ~ex:Explanation.empty r
-        | _ ->
-          Domain.unknown (X.type_info r)
-      in
-      internal_update r nd t
-
-  (** [update r d t] replaces the domain of [r] in [t] by [d]. The
-      representative [r] is marked [changed] after this call if the domain
-      [d] isn't equal to the old one. *)
-  let update r d t =
+    if MX.mem r t.domains then t
+    else
+      match Th.embed r with
+      | Cons _ -> t
+      | _ ->
+        (* 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. *)
+        let nd = Domain.unknown (X.type_info r) in
+        internal_update r nd t
+
+  (** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contains
+      in the current domain of [r]. The representative [r] is marked [changed]
+      after this call if the domain [d] is strictly smaller. *)
+  let tighten r d t =
     let od = get r t in
-    (* For sake of completeness, the domain [d] has to be a subset
-       of the old domain of [r]. *)
+    (* For sake of completeness, the domain [d] has to be a subset of the old
+       domain of [r]. *)
     assert (not (Options.get_enable_assertions ()) || Domain.subset d od);
     if Domain.equal od d then
       t
@@ -179,13 +177,9 @@ module Domains = struct
   let subst ~ex r nr t =
     match MX.find r t.domains with
     | d ->
-      let nnd =
-        match MX.find nr t.domains with
-        | nd -> Domain.intersect ~ex d nd
-        | exception Not_found -> d
-      in
+      let nd = Domain.intersect ~ex d (get nr t) in
       let t = remove r t in
-      internal_update nr nnd t
+      tighten nr nd t
 
     | exception Not_found -> t
 
@@ -271,8 +265,8 @@ let count_splits env la =
   in
   {env with size_splits = nb}
 
-let update_domain rr nd env =
-  { env with domains = Domains.update rr nd env.domains }
+let tighten_domain rr nd env =
+  { env with domains = Domains.tighten rr nd env.domains }
 
 (* Update the domains of the semantic values [r1] and [r2] according to
    the substitution `r1 |-> r2`.
@@ -305,14 +299,14 @@ let assume_distinct ~ex r1 r2 env =
     match Domain.as_singleton d1 with
     | Some c ->
       let nd = Domain.remove ~ex c d2 in
-      update_domain r2 nd env
+      tighten_domain r2 nd env
     | None ->
       env
   in
   match Domain.as_singleton d2 with
   | Some c ->
     let nd = Domain.remove ~ex c d1 in
-    update_domain r1 nd env
+    tighten_domain r1 nd env
   | None ->
     env