From 6ffb0bc17a488354038e627ea686a3bf69bf2661 Mon Sep 17 00:00:00 2001 From: Fardale Date: Tue, 21 Nov 2023 00:45:05 +0100 Subject: [PATCH] fix(Bitv): fix the is_subset function in a bit vector, given two set i and b, testing "(i && b) <> 0" is testing if the intersection is non-empty and not if i is a subset of b. --- lib/unification/Bitv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/unification/Bitv.ml b/lib/unification/Bitv.ml index af8f21a..1a22bd7 100644 --- a/lib/unification/Bitv.ml +++ b/lib/unification/Bitv.ml @@ -34,7 +34,7 @@ module Int : S with type t = private int = struct let is_empty n = (n = 0) let is_singleton n = n land (n-1) = 0 - let is_subset i b = (i && b) <> 0 + let is_subset i b = (i && b) = i let mem i b = is_subset (singleton i) b let pp = CCInt.pp_binary @@ -57,7 +57,7 @@ module Z : S with type t = private Z.t = struct let is_empty n = Z.(n = zero) let is_singleton n = Z.(n land (n-one) = zero) - let is_subset i b = Z.((i && b) <> zero) + let is_subset i b = (i && b) = i let mem i b = is_subset (singleton i) b let pp = Z.pp_print