MinaProtocol / mina / 507

Committed 19 Aug 2025 11:53PM UTC coverage: 33.38% (-28.0%) from 61.334%

Build # 507

Build Type

push

buildkite

Committed by

web-flow

Commit Message

Merge pull request #17640 from MinaProtocol/georgeee/compatible-to-develop-2025-08-19

Merge `compatible` to `develop` (19 August 2025, pt. 2)

Run Details

24170 of 72408 relevant lines covered (33.38%)

24770.87 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

7.69

/src/lib/mina_stdlib/graph_algorithms.ml

module Nat = Nat
open Core_kernel

type 'a adjacency_list = ('a * 'a list) list

module Make (V : Comparable.S) = struct
  module G = struct
    type t = V.Set.t V.Map.t
  end

  let connected_component (g : G.t) v0 =
    let rec go seen next =
      match next with
      | [] ->
          seen
      | v :: next ->
          go (Set.add seen v)
            ( Option.value_map ~default:[]
                ~f:(fun neighbors -> Set.to_list (Set.diff neighbors seen))
                (Map.find g v)
            @ next )
    in
    go V.Set.empty [ v0 ]

  let choose (g : G.t) : V.t option =
    with_return (fun { return } ->
        Map.iteri g ~f:(fun ~key ~data:_ -> return (Some key)) ;
        None )

  let connected (g : G.t) : bool =
    match choose g with
    | None ->
        (* G is empty *)
        true
    | Some v ->
        Int.equal (Map.length g) (Set.length (connected_component g v))

  let remove_vertex (g : G.t) v : G.t =
    Map.remove g v |> Map.map ~f:(Fn.flip Set.remove v)

  (* Naive algorithm for computing the minimum number of vertices required to disconnect
     a graph as
     connectivity G =
      if not (connected G)
      then 0
      else 1 + min_{v in V(G)} connectivity (G - v)
     The function returns a lazy nat, because the algorithm naturally can
     be seen as a search over sequences of vertices of increasing length,
     and upon finishing examining all sequences of a given length, we learn
     one more piece of information about the return value (i.e., whether it
     is bigger than that length or equal to it.)
     This means that the caller of this function can control how far this
     search goes based on how much information they need. For example, if
     they just want to know whether the graph is connected, they only need
     to force the outermost constructor. In general, if they want to know
     whether the connectivity is >= n, they only need to force the first
     n + 1 constructors.
  *)

  let rec connectivity (g : G.t) : Nat.t =
    lazy
      ( if not (connected g) then Z
      else
        S
          ( lazy
            (Nat.min
               (List.map (Map.keys g) ~f:(fun v ->
                    connectivity (remove_vertex g v) ) ) ) ) )
end

let connectivity (type a) (module V : Comparable.S with type t = a)
    (adj : V.t adjacency_list) =
  let module M = Make (V) in
  let g : M.G.t =
    V.Map.of_alist_exn (List.map adj ~f:(fun (x, xs) -> (x, V.Set.of_list xs)))
  in
  M.connectivity g

1	module Nat = Nat	7✔
2	open Core_kernel
3
4	type 'a adjacency_list = ('a * 'a list) list
5
6	module Make (V : Comparable.S) = struct
7	module G = struct
8	type t = V.Set.t V.Map.t
9	end
10
11	let connected_component (g : G.t) v0 =
12	let rec go seen next =	×
13	match next with	×
14	\| [] ->	×
15	seen
16	\| v :: next ->	×
17	go (Set.add seen v)	×
18	( Option.value_map ~default:[]	×
19	~f:(fun neighbors -> Set.to_list (Set.diff neighbors seen))	×
20	(Map.find g v)	×
21	@ next )
22	in
23	go V.Set.empty [ v0 ]
24
25	let choose (g : G.t) : V.t option =
26	with_return (fun { return } ->	×
27	Map.iteri g ~f:(fun ~key ~data:_ -> return (Some key)) ;	×
28	None )	×
29
30	let connected (g : G.t) : bool =
31	match choose g with	×
32	\| None ->	×
33	(* G is empty *)
34	true
35	\| Some v ->	×
36	Int.equal (Map.length g) (Set.length (connected_component g v))	×
37
38	let remove_vertex (g : G.t) v : G.t =
39	Map.remove g v \|> Map.map ~f:(Fn.flip Set.remove v)	×
40
41	(* Naive algorithm for computing the minimum number of vertices required to disconnect
42	a graph as
43	connectivity G =
44	if not (connected G)
45	then 0
46	else 1 + min_{v in V(G)} connectivity (G - v)
47	The function returns a lazy nat, because the algorithm naturally can
48	be seen as a search over sequences of vertices of increasing length,
49	and upon finishing examining all sequences of a given length, we learn
50	one more piece of information about the return value (i.e., whether it
51	is bigger than that length or equal to it.)
52	This means that the caller of this function can control how far this
53	search goes based on how much information they need. For example, if
54	they just want to know whether the graph is connected, they only need
55	to force the outermost constructor. In general, if they want to know
56	whether the connectivity is >= n, they only need to force the first
57	n + 1 constructors.
58	*)
59
60	let rec connectivity (g : G.t) : Nat.t =
61	lazy	×
62	( if not (connected g) then Z	×
63	else
64	S	×
65	( lazy
66	(Nat.min	×
67	(List.map (Map.keys g) ~f:(fun v ->	×
68	connectivity (remove_vertex g v) ) ) ) ) )	×
69	end
70
71	let connectivity (type a) (module V : Comparable.S with type t = a)
72	(adj : V.t adjacency_list) =
73	let module M = Make (V) in	×
74	let g : M.G.t =
75	V.Map.of_alist_exn (List.map adj ~f:(fun (x, xs) -> (x, V.Set.of_list xs)))	×
76	in
77	M.connectivity g	14✔

MinaProtocol / mina / 507

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous