From aa3eaaf693c77badf551ffc8961ba1e4f9cafe59 Mon Sep 17 00:00:00 2001
From: Fardale <fardale+git@crans.org>
Date: Thu, 21 Dec 2023 12:58:54 +0100
Subject: [PATCH] fix: Bitv and large_enough

`is_subset` was used to check if two sets intersect. After correcting
`is_subset` this broke the iteration on the Hullot tree.
The other change are more esthetical:
 - rename `is_singleton` to `is_singleton_or_empty` to reflexed what the
   implementation is doing
 - implement `mem`directly using primitive fonction instead of
   `is_subset`
---
 lib/unification/AC.ml    |  4 ++--
 lib/unification/Bitv.ml  | 13 ++++++++-----
 lib/unification/Bitv.mli |  3 ++-
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/lib/unification/AC.ml b/lib/unification/AC.ml
index 5c9c3a1..60d7e80 100644
--- a/lib/unification/AC.ml
+++ b/lib/unification/AC.ml
@@ -143,11 +143,11 @@ end = struct
     k = stop || f a.(k) && for_all2_range f a (k+1) stop
 
   let large_enough bitvars subset =
-    let f col = Bitv.is_subset col subset in
+    let f col = Bitv.do_intersect col subset in
     for_all2_range f bitvars 0 @@ Array.length bitvars
 
   let small_enough first_var bitvars bitset =
-    let f col = Bitv.(is_singleton (bitset && col)) in
+    let f col = Bitv.(is_singleton_or_empty (bitset && col)) in
     for_all2_range f bitvars 0 first_var
 
   let iterate_subsets len system bitvars =
diff --git a/lib/unification/Bitv.ml b/lib/unification/Bitv.ml
index 1a22bd7..3aedf12 100644
--- a/lib/unification/Bitv.ml
+++ b/lib/unification/Bitv.ml
@@ -10,7 +10,8 @@ module type S = sig
   val is_empty : t -> bool
   val mem : int -> t -> bool
   val is_subset : t -> t -> bool
-  val is_singleton : t -> bool
+  val do_intersect : t -> t -> bool
+  val is_singleton_or_empty : t -> bool
   val pp : Format.formatter -> t -> unit
 
   val capacity : int
@@ -33,9 +34,10 @@ module Int : S with type t = private int = struct
   let all_until i = check_len (i+1) ; (1 lsl (i+1) - 1)
 
   let is_empty n = (n = 0)
-  let is_singleton n = n land (n-1) = 0
+  let is_singleton_or_empty n = n land (n-1) = 0
   let is_subset i b = (i && b) = i
-  let mem i b = is_subset (singleton i) b
+  let do_intersect i b = (i && b) <> 0
+  let mem i b = ((singleton i) && b) <> 0
 
   let pp = CCInt.pp_binary
 end
@@ -56,9 +58,10 @@ module Z : S with type t = private Z.t = struct
   let all_until i = let x = i+1 in Z.(one lsl x - one)
 
   let is_empty n = Z.(n = zero)
-  let is_singleton n = Z.(n land (n-one) = zero)
+  let is_singleton_or_empty n = Z.(n land (n-one) = zero)
   let is_subset i b = (i && b) = i
-  let mem i b = is_subset (singleton i) b
+  let do_intersect i b = (i && b) <> Z.zero
+  let mem i b = ((singleton i) && b) <> Z.zero
 
   let pp = Z.pp_print
 end
diff --git a/lib/unification/Bitv.mli b/lib/unification/Bitv.mli
index 494f36a..f5f3ccb 100644
--- a/lib/unification/Bitv.mli
+++ b/lib/unification/Bitv.mli
@@ -11,7 +11,8 @@ module type S = sig
   val is_empty : t -> bool
   val mem : int -> t -> bool
   val is_subset : t -> t -> bool
-  val is_singleton : t -> bool
+  val do_intersect : t -> t -> bool
+  val is_singleton_or_empty : t -> bool
   val pp : Format.formatter -> t -> unit
 
   val capacity : int