The unpac monorepo manager self-hosting as a monorepo using unpac

Merge pull request #152 from backtracking/bfs01

0-1 BFS

authored by

Jean-Christophe Filliatre and committed by
GitHub
5dcb7a4d 1b052ff2

+238 -2
+1
CHANGES.md
··· 1 1 2 + - [Path]: new module [Bfs01] to implement 0-1 BFS 2 3 - [Classic] new functions [kneser] and [petersen] to build Kneser's 3 4 graphs and the Petersen graph 4 5 - [Oper] fixed transitive reduction (#145, reported by sim642)
+108
src/lib/deque.ml
··· 1 + (**************************************************************************) 2 + (* *) 3 + (* Ocamlgraph: a generic graph library for OCaml *) 4 + (* Copyright (C) 2004-2010 *) 5 + (* Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles *) 6 + (* *) 7 + (* This software is free software; you can redistribute it and/or *) 8 + (* modify it under the terms of the GNU Library General Public *) 9 + (* License version 2.1, with the special exception on linking *) 10 + (* described in file LICENSE. *) 11 + (* *) 12 + (* This software is distributed in the hope that it will be useful, *) 13 + (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) 14 + (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) 15 + (* *) 16 + (**************************************************************************) 17 + 18 + (** Double-ended queue implemented with doubly-linked lists *) 19 + 20 + type 'a cell = 21 + | Null 22 + | Cell of { value: 'a; mutable prev: 'a cell; mutable next: 'a cell; } 23 + 24 + type 'a t = { 25 + mutable front: 'a cell; 26 + mutable back : 'a cell; 27 + mutable size : int; 28 + } 29 + (* invariant: size=0 && front=back == Null 30 + || size>0 && front,back != Null 31 + 32 + ----next---> 33 + front back 34 + <---prev---- 35 + *) 36 + 37 + let create () = 38 + { front = Null; back = Null; size = 0 } 39 + 40 + let length dq = 41 + dq.size 42 + 43 + let clear dq = 44 + dq.front <- Null; 45 + dq.back <- Null; 46 + dq.size <- 0 47 + 48 + let add_first dq x = 49 + let c = Cell { value = x; prev = Null; next = Null } in 50 + dq.front <- c; 51 + dq.back <- c; 52 + dq.size <- 1 53 + 54 + let push_front dq x = 55 + match dq.front with 56 + | Null -> 57 + add_first dq x 58 + | Cell f as cf -> 59 + let c = Cell { value = x; prev = Null; next = cf } in 60 + f.prev <- c; 61 + dq.front <- c; 62 + dq.size <- dq.size + 1 63 + 64 + let peek_front dq = 65 + match dq.front with 66 + | Null -> invalid_arg "peek_front" 67 + | Cell { value=v; _ } -> v 68 + 69 + let pop_front dq = 70 + match dq.front with 71 + | Null -> 72 + invalid_arg "pop_front" 73 + | Cell { value=v; next=Null; _} -> 74 + clear dq; 75 + v 76 + | Cell { value=v; next=Cell c as n; _} -> 77 + dq.front <- n; 78 + c.prev <- Null; 79 + dq.size <- dq.size - 1; 80 + v 81 + 82 + let push_back dq x = 83 + match dq.back with 84 + | Null -> 85 + add_first dq x 86 + | Cell b as cb -> 87 + let c = Cell { value = x; prev = cb; next = Null } in 88 + b.next <- c; 89 + dq.back <- c; 90 + dq.size <- dq.size + 1 91 + 92 + let peek_back dq = 93 + match dq.back with 94 + | Null -> invalid_arg "peek_back" 95 + | Cell { value=v; _ } -> v 96 + 97 + let pop_back dq = 98 + match dq.back with 99 + | Null -> 100 + invalid_arg "pop_back" 101 + | Cell { value=v; prev=Null; _} -> 102 + clear dq; 103 + v 104 + | Cell { value=v; prev=Cell c as p; _} -> 105 + dq.back <- p; 106 + c.next <- Null; 107 + dq.size <- dq.size - 1; 108 + v
+33
src/lib/deque.mli
··· 1 + (**************************************************************************) 2 + (* *) 3 + (* Ocamlgraph: a generic graph library for OCaml *) 4 + (* Copyright (C) 2004-2010 *) 5 + (* Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles *) 6 + (* *) 7 + (* This software is free software; you can redistribute it and/or *) 8 + (* modify it under the terms of the GNU Library General Public *) 9 + (* License version 2.1, with the special exception on linking *) 10 + (* described in file LICENSE. *) 11 + (* *) 12 + (* This software is distributed in the hope that it will be useful, *) 13 + (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) 14 + (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) 15 + (* *) 16 + (**************************************************************************) 17 + 18 + (** Double-ended queue *) 19 + 20 + type 'a t 21 + 22 + val create: unit -> 'a t 23 + val length: 'a t -> int 24 + 25 + val clear: 'a t -> unit 26 + 27 + val push_front: 'a t -> 'a -> unit 28 + val peek_front: 'a t -> 'a 29 + val pop_front: 'a t -> 'a 30 + 31 + val push_back: 'a t -> 'a -> unit 32 + val peek_back: 'a t -> 'a 33 + val pop_back: 'a t -> 'a
+3
src/pack.ml
··· 59 59 module BF = Path.BellmanFord(G)(W) 60 60 let bellman_ford = BF.find_negative_cycle_from 61 61 62 + module Bfs01 = Path.Bfs01(G) 63 + let bfs_0_1 = Bfs01.iter 64 + 62 65 module F = struct 63 66 type label = int 64 67 type t = int
+33
src/path.ml
··· 347 347 loop () 348 348 349 349 end 350 + 351 + (** 0-1 BFS 352 + 353 + When edge weights are limited to 0 or 1, this is more efficient than 354 + running Dijkstra's algorithm. *) 355 + 356 + module Bfs01(G: sig 357 + type t 358 + module V: Sig.COMPARABLE 359 + module E: sig type t val dst : t -> V.t end 360 + val iter_succ_e : (E.t -> unit) -> t -> V.t -> unit 361 + end) = struct 362 + 363 + module H = Hashtbl.Make(G.V) 364 + 365 + let iter f g ~zero s = 366 + let visited = H.create 16 in 367 + let d = Deque.create () in 368 + Deque.push_front d (s, 0); H.add visited s (); 369 + while Deque.length d > 0 do 370 + let v, n = Deque.pop_front d in 371 + f v n; 372 + G.iter_succ_e (fun e -> 373 + let w = G.E.dst e in 374 + if not (H.mem visited w) then ( 375 + H.add visited w (); 376 + if zero e then Deque.push_front d (w, n ) 377 + else Deque.push_back d (w, n+1) 378 + ) 379 + ) g v 380 + done 381 + 382 + end
+23 -2
src/path.mli
··· 15 15 (* *) 16 16 (**************************************************************************) 17 17 18 - (* $Id: path.mli,v 1.9 2005-07-18 07:10:35 filliatr Exp $ *) 19 - 20 18 (** Paths *) 21 19 22 20 (** Minimal graph signature for Dijkstra's algorithm. ··· 152 150 *) 153 151 154 152 end 153 + 154 + (** 0-1 BFS 155 + 156 + When edge weights are limited to 0 or 1, this is more efficient than 157 + running Dijkstra's algorithm. It runs in time and space O(E) in 158 + the worst case. *) 159 + 160 + module Bfs01(G: sig 161 + type t 162 + module V: Sig.COMPARABLE 163 + module E: sig type t val dst : t -> V.t end 164 + val iter_succ_e : (E.t -> unit) -> t -> V.t -> unit 165 + end) : sig 166 + 167 + val iter: (G.V.t -> int -> unit) -> 168 + G.t -> zero:(G.E.t -> bool) -> G.V.t -> unit 169 + (** [iter f g zero s] performs a 0-1 BFS on graph [g], from the 170 + source vertex [s], and applies [f] to each visited vertex and 171 + its distance from the source. Function [zero] indicates 0-edges. 172 + All reachable vertices are visited, in increasing order of 173 + distance to the source. *) 174 + 175 + end
+3
src/sig_pack.mli
··· 419 419 (** [bellman_ford g v] finds a negative cycle from [v], and returns it, 420 420 or raises [Not_found] if there is no such cycle *) 421 421 422 + val bfs_0_1: (V.t -> int -> unit) -> t -> zero:(E.t -> bool) -> V.t -> unit 423 + (** 0-1 BFS from a given source. Function [zero] indicates 0-edges. *) 424 + 422 425 (** Path checking *) 423 426 module PathCheck : sig 424 427 type path_checker
+5
tests/dune
··· 24 24 (modules test_topsort)) 25 25 26 26 (test 27 + (name test_bfs01) 28 + (libraries graph) 29 + (modules test_bfs01)) 30 + 31 + (test 27 32 (name test_check_path) 28 33 (libraries graph) 29 34 (modules test_check_path))
+29
tests/test_bfs01.ml
··· 1 + 2 + (* Test file for Path.Bfs01 *) 3 + 4 + open Graph 5 + open Pack.Digraph 6 + 7 + let zero e = 8 + E.label e = 0 9 + 10 + let test n = 11 + let g = create () in 12 + let nv = 2*n+2 in 13 + let v = Array.init nv V.create in 14 + Array.iter (add_vertex g) v; 15 + let edge i d j = add_edge_e g (E.create v.(i) d v.(j)) in 16 + for i = 1 to n do let i = 2*i in edge (i-2) 0 i done; edge (2*n) 1 (2*n+1); 17 + edge 0 1 1; for i = 0 to n-1 do let i = 2*i+1 in edge i 1 (i+2) done; 18 + let check v d = 19 + let i = V.label v in 20 + assert (d = if i mod 2 = 0 then 0 21 + else if i = 2*n+1 then 1 22 + else (i+1) / 2) in 23 + bfs_0_1 check g ~zero v.(0) 24 + 25 + let () = 26 + for n = 0 to 10 do test n done 27 + 28 + 29 +