liquid-fixpoint-0.1.0.0: external/ocamlgraph/src/gpath.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: path.ml,v 1.6 2005-07-18 07:10:35 filliatr Exp $ *)
module type WEIGHT = sig
type label
type t
val weight : label -> t
val zero : t
val add : t -> t -> t
val compare : t -> t -> int
end
module type G = sig
type t
module V : Sig.COMPARABLE
module E : sig
type t
type label
val label : t -> label
val dst : t -> V.t
end
val iter_succ_e : (E.t -> unit) -> t -> V.t -> unit
end
module Dijkstra
(G: G)
(W: WEIGHT with type label = G.E.label) =
struct
open G.E
module H = Hashtbl.Make(G.V)
module Elt = struct
type t = W.t * G.V.t * G.E.t list
(* weights are compared first, and minimal weights come first in the
queue *)
let compare (w1,v1,_) (w2,v2,_) =
let cw = W.compare w2 w1 in
if cw != 0 then cw else G.V.compare v1 v2
end
module PQ = Heap.Imperative(Elt)
let shortest_path g v1 v2 =
let visited = H.create 97 in
let q = PQ.create 17 in
let rec loop () =
if PQ.is_empty q then raise Not_found;
let (w,v,p) = PQ.pop_maximum q in
if G.V.compare v v2 = 0 then
List.rev p, w
else begin
if not (H.mem visited v) then begin
H.add visited v ();
G.iter_succ_e
(fun e -> PQ.add q (W.add w (W.weight (label e)), dst e, e :: p))
g v
end;
loop ()
end
in
PQ.add q (W.zero, v1, []);
loop ()
end
module Check
(G :
sig
type t
module V : Sig.COMPARABLE
val iter_succ : (V.t -> unit) -> t -> V.t -> unit
end) =
struct
module HV = Hashtbl.Make(G.V)
module HVV = Hashtbl.Make(Util.HTProduct(G.V)(G.V))
(* the cache contains the path tests already computed *)
type path_checker = { cache : bool HVV.t; graph : G.t }
let create g = { cache = HVV.create 97; graph = g }
let check_path pc v1 v2 =
try
HVV.find pc.cache (v1, v2)
with Not_found ->
(* the path is not in cache; we check it with Dijkstra *)
let visited = HV.create 97 in
let q = Queue.create () in
let rec loop () =
if Queue.is_empty q then begin
HVV.add pc.cache (v1, v2) false;
false
end else begin
let v = Queue.pop q in
HVV.add pc.cache (v1, v) true;
if G.V.compare v v2 = 0 then
true
else begin
if not (HV.mem visited v) then begin
HV.add visited v ();
G.iter_succ (fun v' -> Queue.add v' q) pc.graph v
end;
loop ()
end
end
in
Queue.add v1 q;
loop ()
end