Clean add

OCamlPro · Mar 29, 2024 · c8381b7 · c8381b7
1 parent bcece9d
commit c8381b7
Showing 1 changed file with 12 additions and 19 deletions.
diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
@@ -87,11 +87,9 @@ module Domain = struct
     let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
     domain ~constrs ex
 
-  let complement ~ex d1 d2 =
-    let constrs =
-      HSS.filter (fun c -> not @@ HSS.mem c d2.constrs) d1.constrs
-    in
-    let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
+  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
@@ -175,18 +173,20 @@ let update_domain rr nd env =
 
    @raise Domain.Inconsistent if the disequality is inconsistent with
           the current environment [env]. *)
-let propagate_diseq ~ex r1 r2 env =
+let propagate_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 nd = Domain.complement ~ex d2 d1 in
+      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 nd = Domain.complement ~ex d1 d2 in
+    let c = Domain.choose d2 in
+    let nd = Domain.remove ~ex c d1 in
     update_domain r1 nd env
   else
     env
@@ -210,16 +210,9 @@ let add r uf 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 =
-  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 env uf r _t = add r uf env, []
 
-let propagate_literals la uf env =
+let assume_literals la uf env =
   List.fold_left
     (fun env lit ->
        let open Xliteral in
@@ -234,7 +227,7 @@ let propagate_literals la uf env =
          Debug.assume l;
          let env = add_rec r1 uf env in
          let env = add_rec r2 uf env in
-         propagate_diseq ~ex r1 r2 env
+         propagate_distinct ~ex r1 r2 env
 
        | _ ->
          env
@@ -259,7 +252,7 @@ let assume env uf la =
   let env = { env with classes = classes } in
   let env =
     try
-      propagate_literals la uf env
+      assume_literals la uf env
     with Domain.Inconsistent ex ->
       raise_notrace (Ex.Inconsistent (ex, env.classes))
   in