Review changes

src/lib/reasoners/enum_rel.ml

@@ -136,7 +136,14 @@ let values_of r =
     None
 
 (* Update the domains of the semantic values [sm1] and [sm2] according to
-   the disequality [sm1 <> sm2]. *)
+   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)
@@ -181,7 +188,13 @@ let add_diseq hss sm1 sm2 dep env eqs =
   |  _ -> env, eqs
 
 (* Update the domains of the semantic values [sm1] and [sm2] according to
-   the equation [sm1 = sm2]. *)
+   the equation [sm1 = sm2]. More precisely, we replace their domains by
+   the intersection of these domains.
+
+   In any case, we produce an equality if the domain of these semantic values
+   becomes a singleton.
+
+   @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,_)
@@ -222,7 +235,8 @@ let count_splits env la =
   in
   {env with size_splits = nb}
 
-(* Add the uninterpreted semantic value [r] to the environment. *)
+(* Add the uninterpreted semantic value [r] to the environment [env] with the
+   total domain. *)
 let add_aux env r =
   Debug.add r;
   match Sh.embed r, values_of r with
@@ -285,9 +299,9 @@ let case_split env uf ~for_model =
               value. *)
            acc
          | _ ->
-           (* We have to do a case-split, even if the domain of [r] is
-              of cardinal 1 as we have to put this value in the
-              equivalence class of [r]. *)
+           (* 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