packages feed

liquid-fixpoint-0.1.0.0: external/ocamlgraph/src/traverse.ml

(**************************************************************************)
(*                                                                        *)
(*  Ocamlgraph: a generic graph library for OCaml                         *)
(*  Copyright (C) 2004-2007                                               *)
(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2, with the special exception on linking              *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* $Id: traverse.ml,v 1.17 2004-11-04 13:10:28 filliatr Exp $ *)

(* Graph traversal *)

module type G = sig
  type t
  module V : Sig.COMPARABLE
  val iter_vertex : (V.t -> unit) -> t -> unit
  val fold_vertex : (V.t -> 'a -> 'a) -> t  -> 'a -> 'a
  val iter_succ : (V.t -> unit) -> t -> V.t -> unit
  val fold_succ : (V.t -> 'a -> 'a) -> t -> V.t -> 'a -> 'a
end

(* depth-first search *)
module Dfs(G : G) = struct
  module H = Hashtbl.Make(G.V)

  let iter ?(pre=fun _ -> ()) ?(post=fun _ -> ()) g = 
    let h = H.create 65537 in
    let rec visit v =
      if not (H.mem h v) then begin
	H.add h v ();
	pre v;
	G.iter_succ visit g v;
	post v
      end
    in
    G.iter_vertex visit g

  let postfix post g = iter ~post g

  let iter_component ?(pre=fun _ -> ()) ?(post=fun _ -> ()) g v = 
    let h = H.create 65537 in
    let rec visit v =
      H.add h v ();
      pre v;
      G.iter_succ (fun w -> if not (H.mem h w) then visit w) g v;
      post v
    in
    visit v

  let prefix_component pre g = iter_component ~pre g
  let postfix_component post g = iter_component ~post g

  (* invariant: not in [h] means not visited at all; [h v = true] means
     already visited in the current component; [h v = false] means
     already visited in another tree *)
  let has_cycle g =
    let h = H.create 65537 in
    let rec visit v =
      H.add h v true;
      G.iter_succ 
	(fun w -> try if H.find h w then raise Exit with Not_found -> visit w) 
	g v;
      H.replace h v false
    in
    try G.iter_vertex (fun v -> if not (H.mem h v) then visit v) g; false 
    with Exit -> true

  module Tail = struct

    let iter f g = 
      let h = H.create 65537 in
      let stack = Stack.create () in
      (* invariant: [h] contains exactly the vertices which have been pushed *)
      let push v = 
	if not (H.mem h v) then begin H.add h v (); Stack.push v stack end
      in
      let loop () =
	while not (Stack.is_empty stack) do
	  let v = Stack.pop stack in
	  f v;
	  G.iter_succ push g v
	done
      in
      G.iter_vertex (fun v -> push v; loop ()) g

    let iter_component f g v0 = 
      let h = H.create 65537 in
      let stack = Stack.create () in
      (* invariant: [h] contains exactly the vertices which have been pushed *)
      let push v = 
	if not (H.mem h v) then begin H.add h v (); Stack.push v stack end
      in
      push v0;
      while not (Stack.is_empty stack) do
	let v = Stack.pop stack in
	f v;
	G.iter_succ push g v
      done

  end

  let prefix = Tail.iter
  let prefix_component = Tail.iter_component

  (* step-by-step iterator *)
  module S = Set.Make(G.V)

  (* state is [(s,st,g)] : [s] contains elements never been pushed in [st] *)
  type iterator = S.t * G.V.t list * G.t

  let start g =
    let s = G.fold_vertex S.add g S.empty in
    s, [], g

  let get (s,st,_) = match st with
    | [] -> if S.is_empty s then raise Exit else S.choose s
    | v :: _ -> v

  let step (s,st,g) =
    let push v (s,st as acc) = 
      if S.mem v s then 
	S.remove v s, v :: st
      else
	acc 
    in
    let v,s',st' = match st with
      | [] ->
	  if S.is_empty s then raise Exit;
	  let v = S.choose s in
	  (v, S.remove v s, [])
      | v :: st' ->
	  (v, s, st')
    in
    let s'',st'' = G.fold_succ push g v (s',st') in
    (s'',st'',g)

end

(* breadth-first search *)
module Bfs(G : G) = struct
  module H = Hashtbl.Make(G.V)

  let iter f g = 
    let h = H.create 65537 in
    let q = Queue.create () in
    (* invariant: [h] contains exactly the vertices which have been pushed *)
    let push v = 
      if not (H.mem h v) then begin H.add h v (); Queue.add v q end 
    in
    let loop () =
      while not (Queue.is_empty q) do
	let v = Queue.pop q in
	f v;
	G.iter_succ push g v
      done
    in
    G.iter_vertex (fun v -> push v; loop ()) g

  let iter_component f g v0 = 
    let h = H.create 65537 in
    let q = Queue.create () in
    (* invariant: [h] contains exactly the vertices which have been pushed *)
    let push v = 
      if not (H.mem h v) then begin H.add h v (); Queue.add v q end 
    in
    push v0;
    while not (Queue.is_empty q) do
      let v = Queue.pop q in
      f v;
      G.iter_succ push g v
    done

  (* step-by-step iterator *)

  (* simple, yet O(1)-amortized, persistent queues *)
  module Q = struct
    type 'a t = 'a list * 'a list
    exception Empty
    let empty = [], []
    let is_empty = function [], [] -> true | _ -> false
    let push x (i,o) = (x :: i, o)
    let pop = function 
      | i, y :: o -> y, (i,o) 
      | [], [] -> raise Empty
      | i, [] -> match List.rev i with 
	  | x :: o -> x, ([], o) 
	  | [] -> assert false
    let peek q = fst (pop q)
  end

  module S = Set.Make(G.V)

  (* state is [(s,q,g)] : [s] contains elements never been pushed in [q] *)
  type iterator = S.t * G.V.t Q.t * G.t

  let start g =
    let s = G.fold_vertex S.add g S.empty in
    s, Q.empty, g

  let get (s,q,g) = 
    if Q.is_empty q then
      if S.is_empty s then raise Exit else S.choose s
    else
      Q.peek q

  let step (s,q,g) =
    let push v (s,q as acc) = 
      if S.mem v s then 
	S.remove v s, Q.push v q
      else
	acc 
    in
    let v,s',q' = 
      if Q.is_empty q then begin
	if S.is_empty s then raise Exit;
	let v = S.choose s in
	v, S.remove v s, q
      end else
	let v,q' = Q.pop q in 
	v, s, q'
    in
    let s'',q'' = G.fold_succ push g v (s',q') in
    (s'',q'',g)

end


(* Graph traversal with marking. *)

module type GM = sig
  type t
  module V : sig type t end
  val iter_vertex : (V.t -> unit) -> t -> unit
  val iter_succ : (V.t -> unit) -> t -> V.t -> unit
  module Mark : sig
    val clear : t -> unit
    val get : V.t -> int
    val set : V.t -> int -> unit
  end
end

module Mark(G : GM) = struct

  let dfs g =
    G.Mark.clear g;
    let n = ref 0 in
    let rec visit v =
      if G.Mark.get v = 0 then begin
	incr n;
	G.Mark.set v !n;
	G.iter_succ visit g v
      end
    in
    G.iter_vertex visit g

  (* invariant: [h v = 0] means not visited at all; [h v = 1] means
     already visited in the current component; [h v = 2] means
     already visited in another tree *)
  let has_cycle g =
    G.Mark.clear g;
    let rec visit v =
      G.Mark.set v 1;
      G.iter_succ 
	(fun w -> 
	   let m = G.Mark.get w in
	   if m = 1 then raise Exit;
	   if m = 0 then visit w) 
	g v;
      G.Mark.set v 2
    in
    try G.iter_vertex (fun v -> if G.Mark.get v = 0 then visit v) g; false 
    with Exit -> true

end