Skip to content

Commit

Permalink
No intersection in update
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Halbaroth committed Apr 4, 2024
1 parent ab374b0 commit 3f4453c
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/lib/reasoners/enum_rel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 3f4453c

Please sign in to comment.