X-Git-Url: http://git.hcoop.net/bpt/coccinelle.git/blobdiff_plain/755320b0f64ab4fe487507104d2929cfb19dcee1..abad11c5570b7b9bbae5ff92b3050cf68fe3fd14:/bundles/menhirLib/menhir-20120123/src/nonpositiveCycles.ml

diff --git a/bundles/menhirLib/menhir-20120123/src/nonpositiveCycles.ml b/bundles/menhirLib/menhir-20120123/src/nonpositiveCycles.ml
deleted file mode 100644
index efb4aec..0000000
--- a/bundles/menhirLib/menhir-20120123/src/nonpositiveCycles.ml
+++ /dev/null
@@ -1,130 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  Menhir                                                                *)
-(*                                                                        *)
-(*  François Pottier, INRIA Rocquencourt                                  *)
-(*  Yann Régis-Gianas, PPS, Université Paris Diderot                      *)
-(*                                                                        *)
-(*  Copyright 2005-2008 Institut National de Recherche en Informatique    *)
-(*  et en Automatique. All rights reserved. This file is distributed      *)
-(*  under the terms of the Q Public License version 1.0, with the change  *)
-(*  described in file LICENSE.                                            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This module uses Floyd and Warshall's algorithm to detect whether a graph
-   with integer-weighted edges contains a simple cycle of negative weight. *)
-
-(* The algorithm runs in cubic time in the number of vertices. It may be
-   worthwhile to first use Tarjan's algorithm to obtain the graph's strongly
-   connected components, and use Floyd and Warshall's algorithm only on each
-   component. *)
-
-module Run (G : sig
-
-  type node
-
-  (* We assume each node has a unique index. Indices must range from
-     $0$ to $n-1$, where $n$ is the number of nodes in the graph. *)
-
-  val n: int
-  val index: node -> int
-
-  (* Iterating over a node's immediate successors. Edges are weighted. *)
-
-  val successors: (int -> node -> unit) -> node -> unit
-
-  (* Iterating over all nodes. *)
-
-  val iter: (node -> unit) -> unit
-
-end) = struct
-
-  open G
-
-  (* Integers with infinity. *)
-
-  type distance =
-    | Infinity
-    | Finite of int
-
-  let add d1 d2 =
-    match d1, d2 with
-    | Infinity, _
-    | _, Infinity ->
-	Infinity
-    | Finite i1, Finite i2 ->
-	Finite (i1 + i2)
-
-  let min d1 d2 =
-    match d1, d2 with
-    | Infinity, d
-    | d, Infinity ->
-	d
-    | Finite i1, Finite i2 ->
-	Finite (min i1 i2)
-
-  let le d1 d2 =
-    match d1, d2 with
-    | Infinity, Infinity ->
-	true
-    | Infinity, Finite _ ->
-	false
-    | Finite _, Infinity ->
-	true
-    | Finite i1, Finite i2 ->
-	i1 <= i2
-
-  (* Allocate and initialize a distance matrix. At allocation time, every entry
-     is initialized to infinity. Then, we iterate over all edges, and copy them
-     into the distance matrix. *)
-
-  (* Note that, by default, [d.(i).(i)] is not initialized to zero: it is 
-     initialized to infinity. This is because we are looking for paths of
-     non-zero length. In other words, we are computing a transitive closure,
-     not a reflexive, transitive closure. *)
-
-  let d =
-    Array.init n (fun i ->
-      Array.init n (fun j ->
-	Infinity
-      )
-    )
-
-  let () =
-    iter (fun source ->
-      successors (fun weight target ->
-	(* We use a min operation, so the graph may be a multi-graph, that is,
-	   multiple edges between two nodes are permitted. *)
-	let i = index source
-	and j = index target in
-	d.(i).(j) <- min (Finite weight) d.(i).(j)
-      ) source
-    )
-
-  (* The algorithm. *)
-
-  (* Stefan Hougardy notes that, in the presence of negative cycles, distances
-     can grow exponentially fast (towards minus infinity), so there is a risk
-     of overflow. To avoid this, one must check for negative cycles during the
-     computation -- as opposed to waiting until the end. *)
-
-  exception Detection
-
-  let graph_has_nonpositive_simple_cycle : bool =
-    try
-      for k = 0 to n-1 do
-	for i = 0 to n-1 do
-	  for j = 0 to n-1 do
-	    d.(i).(j) <- min d.(i).(j) (add d.(i).(k) d.(k).(j));
-	    if i = j && le d.(i).(j) (Finite 0) then
-	      raise Detection
-	  done
-	done
-      done;
-      false
-    with Detection ->
-      true
-
-end
-