2 (***********************************************************************)
4 (* Copyright (C) Jean-Christophe Filliatre *)
6 (* This software is free software; you can redistribute it and/or *)
7 (* modify it under the terms of the GNU Library General Public *)
8 (* License version 2.1, with the special exception on linking *)
9 (* described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
11 (* This software is distributed in the hope that it will be useful, *)
12 (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
13 (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
15 (***********************************************************************)
17 (* Modified by Kim Nguyen *)
18 (* The Patricia trees are themselves deeply hash-consed. The module
19 provides a Make (and Weak) functor to build hash-consed patricia
20 trees whose elements are Abstract hash-consed values.
27 module type HConsBuilder =
28 functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
30 module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
31 S with type elt = H.t =
38 | Branch of int * int * 'a * 'a
40 module rec Node : Hcons.S with type data = Data.t = HCB(Data)
41 and Data : Common_sig.HashedType with type t = Node.t set =
47 | Leaf k1, Leaf k2 -> k1 == k2
48 | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
49 b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
51 | (Empty|Leaf _|Branch _), _ -> false
55 | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
57 HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
62 let empty = Node.make Empty
64 let is_empty s = s.Node.node == Empty
66 let branch p m l r = Node.make (Branch(p,m,l,r))
68 let leaf k = Node.make (Leaf k)
70 (* To enforce the invariant that a branch contains two non empty
72 let branch_ne p m t0 t1 =
73 if (is_empty t0) then t1
74 else if is_empty t1 then t0 else branch p m t0 t1
76 (******** from here on, only use the smart constructors ************)
78 let singleton k = leaf k
81 match n.Node.node with
83 | Branch _ | Empty -> false
86 let kid = (H.uid k :> int) in
87 let rec loop n = match n.Node.node with
90 | Branch (p, _, l, r) -> loop (if kid <= p then l else r)
93 let rec min_elt n = match n.Node.node with
94 | Empty -> raise Not_found
96 | Branch (_,_,s,_) -> min_elt s
98 let rec max_elt n = match n.Node.node with
99 | Empty -> raise Not_found
101 | Branch (_,_,_,t) -> max_elt t
104 let rec elements_aux acc n = match n.Node.node with
107 | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
112 let zero_bit k m = (k land m) == 0
114 let mask k m = (k lor (m-1)) land (lnot m)
116 external int_of_bool : bool -> int = "%identity"
119 let v = v0 lor (v0 lsr 1) in
120 let v = v lor (v lsr 2) in
121 let v = v lor (v lsr 4) in
122 let v = v lor (v lsr 8) in
123 let v = v lor (v lsr 16) in
124 ((v + 1) lsr 1) + (int_of_bool (v0 == 0))
127 let v = v0 lor (v0 lsr 1) in
128 let v = v lor (v lsr 2) in
129 let v = v lor (v lsr 4) in
130 let v = v lor (v lsr 8) in
131 let v = v lor (v lsr 16) in
132 let v = v lor (v lsr 32) in
133 ((v + 1) lsr 1) + (int_of_bool (v0 == 0))
136 let branching_bit p0 p1 = hb64 (p0 lxor p1)
138 let join p0 t0 p1 t1 =
139 let m = branching_bit p0 p1 in
140 let msk = mask p0 m in
141 if zero_bit p0 m then
142 branch_ne msk m t0 t1
144 branch_ne msk m t1 t0
146 let match_prefix k p m = (mask k m) == p
149 let kid = Uid.to_int (H.uid k) in
150 let rec ins n = match n.Node.node with
152 | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
153 | Branch (p,m,t0,t1) ->
154 if match_prefix kid p m then
155 if zero_bit kid m then
156 branch_ne p m (ins t0) t1
158 branch_ne p m t0 (ins t1)
160 join kid (leaf k) p n
165 let kid = (H.uid k :> int) in
166 let rec rmv n = match n.Node.node with
168 | Leaf j -> if k == j then empty else n
169 | Branch (p,m,t0,t1) ->
170 if match_prefix kid p m then
171 if zero_bit kid m then
172 branch_ne p m (rmv t0) t1
174 branch_ne p m t0 (rmv t1)
180 (* should run in O(1) thanks to hash consing *)
182 let equal a b = a == b
184 let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
187 if equal s t (* This is cheap thanks to hash-consing *)
190 match s.Node.node, t.Node.node with
193 | Leaf k, _ -> add k t
194 | _, Leaf k -> add k s
195 | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
196 if m == n && match_prefix q p m then
197 branch p m (merge s0 t0) (merge s1 t1)
198 else if m > n && match_prefix q p m then
200 branch_ne p m (merge s0 t) s1
202 branch_ne p m s0 (merge s1 t)
203 else if m < n && match_prefix p q n then
205 branch_ne q n (merge s t0) t1
207 branch_ne q n t0 (merge s t1)
209 (* The prefixes disagree. *)
215 let rec subset s1 s2 = (equal s1 s2) ||
216 match s1.Node.node, s2.Node.node with
219 | Leaf k1, _ -> mem k1 s2
220 | Branch _, Leaf _ -> false
221 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
222 if m1 == m2 && p1 == p2 then
223 subset l1 l2 && subset r1 r2
224 else if m1 < m2 && match_prefix p1 p2 m2 then
225 if zero_bit p1 m2 then
226 subset l1 l2 && subset r1 l2
228 subset l1 r2 && subset r1 r2
233 let union s1 s2 = merge s1 s2
234 (* Todo replace with e Memo Module *)
236 let rec inter s1 s2 =
240 match s1.Node.node, s2.Node.node with
243 | Leaf k1, _ -> if mem k1 s2 then s1 else empty
244 | _, Leaf k2 -> if mem k2 s1 then s2 else empty
245 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
246 if m1 == m2 && p1 == p2 then
247 merge (inter l1 l2) (inter r1 r2)
248 else if m1 > m2 && match_prefix p2 p1 m1 then
249 inter (if zero_bit p2 m1 then l1 else r1) s2
250 else if m1 < m2 && match_prefix p1 p2 m2 then
251 inter s1 (if zero_bit p1 m2 then l2 else r2)
259 match s1.Node.node, s2.Node.node with
262 | Leaf k1, _ -> if mem k1 s2 then empty else s1
263 | _, Leaf k2 -> remove k2 s1
264 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
265 if m1 == m2 && p1 == p2 then
266 merge (diff l1 l2) (diff r1 r2)
267 else if m1 > m2 && match_prefix p2 p1 m1 then
268 if zero_bit p2 m1 then
269 merge (diff l1 s2) r1
271 merge l1 (diff r1 s2)
272 else if m1 < m2 && match_prefix p1 p2 m2 then
273 if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
278 (*s All the following operations ([cardinal], [iter], [fold], [for_all],
279 [exists], [filter], [partition], [choose], [elements]) are
280 implemented as for any other kind of binary trees. *)
282 let rec cardinal n = match n.Node.node with
285 | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
287 let rec iter f n = match n.Node.node with
290 | Branch (_,_,t0,t1) -> iter f t0; iter f t1
292 let rec fold_left f s accu = match s.Node.node with
295 | Branch (_,_,t0,t1) -> fold_left f t1 (fold_left f t0 accu)
297 let rec fold_right f s accu = match s.Node.node with
300 | Branch (_,_,t0,t1) -> fold_right f t0 (fold_right f t1 accu)
302 let fold f s accu = fold_left f s accu
304 let rec for_all p n = match n.Node.node with
307 | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
309 let rec exists p n = match n.Node.node with
312 | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
314 let rec filter pr n = match n.Node.node with
316 | Leaf k -> if pr k then n else empty
317 | Branch (p,m,t0,t1) -> let n0 = filter pr t0 in
318 let n1 = filter pr t1 in
322 let rec part (t,f as acc) n = match n.Node.node with
324 | Leaf k -> if p k then (add k t, f) else (t, add k f)
325 | Branch (_,_,t0,t1) -> part (part acc t0) t1
327 part (empty, empty) s
329 let rec choose n = match n.Node.node with
330 | Empty -> raise Not_found
332 | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
336 let coll k (l, b, r) =
337 if k < x then add k l, b, r
338 else if k > x then l, b, add k r
341 fold coll s (empty, false, empty)
343 (*s Additional functions w.r.t to [Set.S]. *)
345 let rec intersect s1 s2 = (equal s1 s2) ||
346 match s1.Node.node, s2.Node.node with
349 | Leaf k1, _ -> mem k1 s2
350 | _, Leaf k2 -> mem k2 s1
351 | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
352 if m1 == m2 && p1 == p2 then
353 intersect l1 l2 || intersect r1 r2
354 else if m1 > m2 && match_prefix p2 p1 m1 then
355 intersect (if zero_bit p2 m1 then l1 else r1) s2
356 else if m1 < m2 && match_prefix p1 p2 m2 then
357 intersect s1 (if zero_bit p1 m2 then l2 else r2)
362 let from_list l = List.fold_left (fun acc e -> add e acc) empty l
367 module Make = Builder(Hcons.Make)
368 module Weak = Builder(Hcons.Weak)
373 include Make(Hcons.PosInt)
375 Format.pp_print_string ppf "{ ";
376 iter (fun i -> Format.fprintf ppf "%i " i) s;
377 Format.pp_print_string ppf "}";
378 Format.pp_print_flush ppf ()