refactor(pkg): change sets to hashsets

Signed-off-by: Rudi Grinberg <[email protected]>

<!-- ps-id: aec1d5e4-e558-49b4-87f4-3e45bd59b7ba -->

Signed-off-by: Rudi Grinberg <[email protected]>

src/0install-solver/hash_set.ml

@@ -0,0 +1,145 @@
+module List = Stdlib.ListLabels
+
+let ( = ) = Int.equal
+let ( < ) x y = Int.compare x y = -1
+let ( > ) x y = Int.compare x y = 1
+
+module Int = struct
+  let[@warning "-32"] hash (x : int) = Hashtbl.hash x
+
+  include Stdlib.Int
+end
+
+module Array = struct
+  type nonrec t = Bytes.t
+
+  let words = 8
+  let[@inline] length t = Bytes.length t / words
+  let[@inline] unsafe_get t i = Int64.to_int (Bytes.get_int64_ne t (i * words))
+  let[@inline] unsafe_set t i x = Bytes.set_int64_ne t (i * words) (Int64.of_int x)
+
+  let[@inline] make len x =
+    let t = Bytes.create (len * words) in
+    for i = 0 to length t - 1 do
+      unsafe_set t i x
+    done;
+    t
+  ;;
+
+  let[@inline] make_absent len = Bytes.make (len * words) '\255'
+  let clear t = Bytes.fill t 0 (Bytes.length t) '\255'
+end
+
+(* A specialized hash table that makes the following trade-offs:
+   - Open addresing. Bucketing is quite memory intensive and dune is already
+     a memory hog.
+   - No boxing for empty slots. We make use of the fact that id's are never
+     negative to achieve this.
+   - No saving of the hash. Recomputing the hash for id's is a no-op.
+*)
+
+type nonrec table =
+  { mutable table : Array.t
+  ; mutable size : int
+  }
+
+type t = table Option.t ref
+
+let init t =
+  if Option.is_none !t then t := Option.some { size = 0; table = Array.make 0 (-1) };
+  Option.get !t
+;;
+
+let[@inline] should_grow t =
+  let slots = Array.length t.table in
+  slots = 0 || (t.size > 0 && slots / t.size < 2)
+;;
+
+let absent = -1
+
+let () =
+  let x = Array.make_absent 1 in
+  assert (Array.unsafe_get x 0 = absent)
+;;
+
+let create () = ref Option.none
+
+let[@inline] index_of_offset slots index i =
+  let i = index + !i in
+  if i >= slots then i - slots else i
+;;
+
+let clear t =
+  match !t with
+  | None -> ()
+  | Some t ->
+    t.size <- 0;
+    Array.clear t.table
+;;
+
+let add t x =
+  let hash = Int.hash x in
+  let slots = Array.length t.table in
+  let index = hash land (slots - 1) in
+  let inserting = ref true in
+  let i = ref 0 in
+  while !inserting do
+    let idx = index_of_offset slots index i in
+    let elem = Array.unsafe_get t.table idx in
+    if elem = absent
+    then (
+      Array.unsafe_set t.table idx x;
+      inserting := false)
+    else incr i
+  done;
+  t.size <- t.size + 1
+;;
+
+let resize t =
+  let old_table = t.table in
+  let slots = Array.length old_table in
+  let table = Array.make_absent (if slots = 0 then 1 else slots lsl 1) in
+  t.table <- table;
+  for i = 0 to slots - 1 do
+    let elem = Array.unsafe_get old_table i in
+    if elem <> absent then add t elem
+  done
+;;
+
+let add t x =
+  let t = init t in
+  if should_grow t then resize t;
+  add t x
+;;
+
+let[@inline] is_empty t =
+  let t = !t in
+  if Option.is_none t
+  then true
+  else (
+    let t = Option.get t in
+    t.size = 0)
+;;
+
+let mem t x =
+  let t = !t in
+  if Option.is_none t || (Option.get t).size = 0
+  then false
+  else (
+    let t = Option.get t in
+    let hash = Int.hash x in
+    let slots = Array.length t.table in
+    let index = hash land (slots - 1) in
+    let i = ref 0 in
+    let found = ref false in
+    while (not !found) && !i < slots do
+      let idx = index_of_offset slots index i in
+      let elem = Array.unsafe_get t.table idx in
+      if Int.equal elem x
+      then found := true
+      else if Int.equal elem absent
+      then i := slots
+      else incr i
+    done;
+    !found)
+;;

src/0install-solver/hash_set.mli

@@ -0,0 +1,7 @@
+type t
+
+val create : unit -> t
+val is_empty : t -> bool
+val add : t -> int -> unit
+val mem : t -> int -> bool
+val clear : t -> unit

src/0install-solver/sat.ml

@@ -34,6 +34,15 @@ module VarID : sig
   val compare : t -> t -> Ordering.t
   val make_mint : unit -> mint
   val issue : mint -> t
+
+  module Hash_set : sig
+    type id := t
+    type t
+
+    val create : unit -> t
+    val mem : t -> id -> bool
+    val add : t -> id -> unit
+  end
 end = struct
   type t = int
   type mint = int ref
@@ -47,6 +56,8 @@ end = struct
     incr mint;
     i
   ;;
+
+  module Hash_set = Hash_set
 end
 
 module Var_value = struct
@@ -134,27 +145,26 @@ module Make (User : USER) = struct
   let lit_equal (s1, v1) (s2, v2) = s1 == s2 && v1 == v2
 
   module C = Comparable.Make (VarID)
-  module VarSet = C.Set
 
   module LitSet = struct
-    module C = Comparable.Make (struct
-        type t = lit
-
-        let to_dyn = Dyn.opaque
-
-        let compare (s1, v1) (s2, v2) =
-          match VarID.compare v1.id v2.id with
-          | Eq ->
-            (match s1, s2 with
-             | Pos, Pos -> Eq
-             | Pos, _ -> Gt
-             | _, Pos -> Lt
-             | Neg, Neg -> Eq)
-          | x -> x
-        ;;
-      end)
-
-    include C.Set
+    type t =
+      { pos : VarID.Hash_set.t
+      ; neg : VarID.Hash_set.t
+      }
+
+    let create () = { pos = VarID.Hash_set.create (); neg = VarID.Hash_set.create () }
+
+    let mem { pos; neg } (sign, lit) =
+      match sign with
+      | Pos -> VarID.Hash_set.mem pos lit.id
+      | Neg -> VarID.Hash_set.mem neg lit.id
+    ;;
+
+    let add { pos; neg } (sign, lit) =
+      match sign with
+      | Pos -> VarID.Hash_set.add pos lit.id
+      | Neg -> VarID.Hash_set.add neg lit.id
+    ;;
   end
 
   type solution = lit -> bool
@@ -184,12 +194,12 @@ module Make (User : USER) = struct
   ;;
 
   let remove_duplicates lits =
-    let seen = ref LitSet.empty in
+    let seen = LitSet.create () in
     let rec find_unique = function
       | [] -> []
-      | x :: xs when LitSet.mem !seen x -> find_unique xs
+      | x :: xs when LitSet.mem seen x -> find_unique xs
       | x :: xs ->
-        seen := LitSet.add !seen x;
+        LitSet.add seen x;
         x :: find_unique xs
     in
     find_unique lits
@@ -576,15 +586,15 @@ module Make (User : USER) = struct
     then (* Trivially true already if any literal is True. *)
       ()
     else (
-      let seen = ref LitSet.empty in
+      let seen = LitSet.create () in
       let rec simplify unique = function
         | [] -> Some unique
-        | x :: _ when LitSet.mem !seen (neg x) -> None (* X or not(X) is always True *)
-        | x :: xs when LitSet.mem !seen x -> simplify unique xs (* Skip duplicates *)
+        | x :: _ when LitSet.mem seen (neg x) -> None (* X or not(X) is always True *)
+        | x :: xs when LitSet.mem seen x -> simplify unique xs (* Skip duplicates *)
         | x :: xs when lit_value x = False ->
           simplify unique xs (* Skip values known to be False *)
         | x :: xs ->
-          seen := LitSet.add !seen x;
+          LitSet.add seen x;
           simplify (x :: unique) xs
       in
       (* At this point, [unique] contains only [Undefined] literals. *)
@@ -674,7 +684,7 @@ module Make (User : USER) = struct
     (* The general rule we're learning *)
     let btlevel = ref 0 in
     (* The deepest decision in learnt *)
-    let seen = ref VarSet.empty in
+    let seen = VarID.Hash_set.create () in
     (* The variables involved in the conflict *)
     let counter = ref 0 in
     (* The number of pending variables to check *)
@@ -699,9 +709,9 @@ module Make (User : USER) = struct
          - otherwise, add it to learnt *)
       List.iter p_reason ~f:(fun lit ->
         let var = var_of_lit lit in
-        if not (VarSet.mem !seen var.id)
+        if not (VarID.Hash_set.mem seen var.id)
         then (
-          seen := VarSet.add !seen var.id;
+          VarID.Hash_set.add seen var.id;
           let var_info = var_of_lit lit in
           if var_info.level = get_decision_level problem
           then
@@ -741,7 +751,7 @@ module Make (User : USER) = struct
         let var = var_of_lit lit in
         let reason = var.reason in
         undo_one problem;
-        if VarSet.mem !seen var.id
+        if VarID.Hash_set.mem seen var.id
         then reason, lit
         else
           (* if debug then log_debug "(irrelevant: %s)" (name_lit lit); *)