packages feed

liquid-fixpoint-0.1.0.0: external/ocamlgraph/src/minsep.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.                  *)
(*                                                                        *)
(**************************************************************************)

(*i $Id: minsep.ml,v 1.7 2004-10-25 15:46:16 signoles Exp $ i*)

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

module type MINSEP = sig
  module G : G
  module Vertex_Set : Set.S with type elt = G.V.t
  module VSetset : Set.S with type elt = Vertex_Set.t
  val allminsep : G.t -> Vertex_Set.t list
  val list_of_allminsep : G.t -> G.V.t list list
  val set_of_allminsep : G.t -> VSetset.t
end

module Make
  (G : sig 
     include G
     val cc: t -> V.t list -> V.t list list 
       (** compute the set of connected components of G(V \ l) *)
   end) =
struct

  module N = Oper.Neighbourhood(G)
  module Vertex_Set = N.Vertex_Set
  module VSetset = Set.Make(Vertex_Set)

  let initialisation g =
    let cc = G.cc g in
    let neighbourhood = N.list_from_vertex g in
    let neighbourhoods = N.set_from_vertices g in
    G.fold_vertex
      (fun v s -> 
	 List.fold_left 
	   (fun s l -> neighbourhoods l :: s)
	   s (cc (v :: neighbourhood v)))
      g []

  let generation g =
    let neighbourhood = N.list_from_vertex g in
    let neighbourhoods = N.set_from_vertices g in
    let cc = G.cc g in
    let rec gen_aux seen bigs = function
      | [] -> bigs
      | s :: tl ->
	  let l = Vertex_Set.elements s in
	  let seen = VSetset.add s seen in
	  let bigs, tl =
	    Vertex_Set.fold 
	      (fun v c ->
		 let add_neighbourhoods (bigs, tl) l = 
		   let s = neighbourhoods l in
		   s :: bigs, if VSetset.mem s seen then tl else s :: tl
		 in
		 List.fold_left 
		   add_neighbourhoods
		   (bigs, tl) (cc (l @ neighbourhood v)))
	      s (bigs, tl)
	  in
	  gen_aux seen bigs tl
    in
    fun bigs -> gen_aux VSetset.empty bigs bigs

  let allminsep g = generation g (initialisation g)

  let set_of_allminsep g = 
    List.fold_left 
      (fun bigs s -> VSetset.add s bigs) VSetset.empty (allminsep g)

  let list_of_allminsep g = List.map Vertex_Set.elements (allminsep g)

end

module P(G : sig include G val remove_vertex : t -> V.t -> t end) = struct
  module G = G
  include Make(struct
		 include G
		 let cc =
		   let module CC = Components.Make(G) in
		   fun g l ->
		     let g = List.fold_left remove_vertex g l in
		     CC.scc_list g
	       end)
end

module I(G : sig 
	   include G 
	   module Mark : Sig.MARK with type graph = t and type vertex = V.t 
	 end) =  
struct
  module G = G
  include Make(struct
		 include G
		 let cc = 
		   let module CC = 
		     Components.Make
		       (struct 
			  include G 
			  let iter_vertex f = 
			    iter_vertex (fun v -> if Mark.get v=0 then f v)
			end) 
		   in
		   fun g l ->
		     G.Mark.clear g;
		     List.iter (fun v -> G.Mark.set v 1) l;
		     CC.scc_list g
	       end)
end