Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(pkg): change sets to hashsets #11300

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
145 changes: 145 additions & 0 deletions src/0install-solver/hash_set.ml
Original file line number Diff line number Diff line change
@@ -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)
;;
7 changes: 7 additions & 0 deletions src/0install-solver/hash_set.mli
Original file line number Diff line number Diff line change
@@ -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
70 changes: 40 additions & 30 deletions src/0install-solver/sat.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -47,6 +56,8 @@ end = struct
incr mint;
i
;;

module Hash_set = Hash_set
end

module Var_value = struct
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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 *)
Expand All @@ -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
Expand Down Expand Up @@ -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); *)
Expand Down
Loading