author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73360 | 4123fca23296 |
child 75394 | 42267c650205 |
permissions | -rw-r--r-- |
46611 | 1 |
/* Title: Pure/General/graph.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Directed graphs. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
10 |
import scala.collection.immutable.{SortedMap, SortedSet} |
46611 | 11 |
import scala.annotation.tailrec |
12 |
||
13 |
||
75393 | 14 |
object Graph { |
15 |
class Duplicate[Key](val key: Key) extends Exception { |
|
70651 | 16 |
override def toString: String = "Graph.Duplicate(" + key.toString + ")" |
17 |
} |
|
75393 | 18 |
class Undefined[Key](val key: Key) extends Exception { |
70651 | 19 |
override def toString: String = "Graph.Undefined(" + key.toString + ")" |
20 |
} |
|
75393 | 21 |
class Cycles[Key](val cycles: List[List[Key]]) extends Exception { |
70651 | 22 |
override def toString: String = cycles.mkString("Graph.Cycles(", ",\n", ")") |
23 |
} |
|
46611 | 24 |
|
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
25 |
def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] = |
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
26 |
new Graph[Key, A](SortedMap.empty(ord)) |
46667 | 27 |
|
75393 | 28 |
def make[Key, A]( |
29 |
entries: List[((Key, A), List[Key])], |
|
30 |
symmetric: Boolean = false)( |
|
31 |
implicit ord: Ordering[Key] |
|
32 |
): Graph[Key, A] = { |
|
49560 | 33 |
val graph1 = |
73359 | 34 |
entries.foldLeft(empty[Key, A](ord)) { |
35 |
case (graph, ((x, info), _)) => graph.new_node(x, info) |
|
36 |
} |
|
49560 | 37 |
val graph2 = |
73359 | 38 |
entries.foldLeft(graph1) { |
39 |
case (graph, ((x, _), ys)) => |
|
40 |
ys.foldLeft(graph) { |
|
41 |
case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) |
|
42 |
} |
|
43 |
} |
|
49560 | 44 |
graph2 |
45 |
} |
|
46 |
||
46667 | 47 |
def string[A]: Graph[String, A] = empty(Ordering.String) |
48 |
def int[A]: Graph[Int, A] = empty(Ordering.Int) |
|
49 |
def long[A]: Graph[Long, A] = empty(Ordering.Long) |
|
49560 | 50 |
|
51 |
||
52 |
/* XML data representation */ |
|
53 |
||
54 |
def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] = |
|
60215 | 55 |
(graph: Graph[Key, A]) => { |
49560 | 56 |
import XML.Encode._ |
57 |
list(pair(pair(key, info), list(key)))(graph.dest) |
|
60215 | 58 |
} |
49560 | 59 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59212
diff
changeset
|
60 |
def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])( |
59212 | 61 |
implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] = |
60215 | 62 |
(body: XML.Body) => { |
49560 | 63 |
import XML.Decode._ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59212
diff
changeset
|
64 |
make(list(pair(pair(key, info), list(key)))(body))(ord) |
60215 | 65 |
} |
46611 | 66 |
} |
67 |
||
68 |
||
75393 | 69 |
final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { |
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
70 |
type Keys = SortedSet[Key] |
46611 | 71 |
type Entry = (A, (Keys, Keys)) |
72 |
||
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
73 |
def ordering: Ordering[Key] = rep.ordering |
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
74 |
def empty_keys: Keys = SortedSet.empty[Key](ordering) |
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
75 |
|
46666
b01b6977a5e8
clarified signature -- avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset
|
76 |
|
b01b6977a5e8
clarified signature -- avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset
|
77 |
/* graphs */ |
46611 | 78 |
|
79 |
def is_empty: Boolean = rep.isEmpty |
|
48507 | 80 |
def defined(x: Key): Boolean = rep.isDefinedAt(x) |
68321 | 81 |
def domain: Set[Key] = rep.keySet |
46611 | 82 |
|
68496 | 83 |
def size: Int = rep.size |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
84 |
def iterator: Iterator[(Key, Entry)] = rep.iterator |
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
85 |
|
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
86 |
def keys_iterator: Iterator[Key] = iterator.map(_._1) |
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
87 |
def keys: List[Key] = keys_iterator.toList |
46611 | 88 |
|
49560 | 89 |
def dest: List[((Key, A), List[Key])] = |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
90 |
(for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList |
46611 | 91 |
|
46666
b01b6977a5e8
clarified signature -- avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset
|
92 |
override def toString: String = |
49560 | 93 |
dest.map({ case ((x, _), ys) => |
94 |
x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") }) |
|
46666
b01b6977a5e8
clarified signature -- avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset
|
95 |
.mkString("Graph(", ", ", ")") |
46611 | 96 |
|
97 |
private def get_entry(x: Key): Entry = |
|
98 |
rep.get(x) match { |
|
99 |
case Some(entry) => entry |
|
100 |
case None => throw new Graph.Undefined(x) |
|
101 |
} |
|
102 |
||
103 |
private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] = |
|
104 |
new Graph[Key, A](rep + (x -> f(get_entry(x)))) |
|
105 |
||
106 |
||
107 |
/* nodes */ |
|
108 |
||
109 |
def get_node(x: Key): A = get_entry(x)._1 |
|
110 |
||
111 |
def map_node(x: Key, f: A => A): Graph[Key, A] = |
|
112 |
map_entry(x, { case (i, ps) => (f(i), ps) }) |
|
113 |
||
114 |
||
115 |
/* reachability */ |
|
116 |
||
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
117 |
/*reachable nodes with length of longest path*/ |
70794 | 118 |
def reachable_length( |
70800 | 119 |
count: Key => Long, |
70794 | 120 |
next: Key => Keys, |
75393 | 121 |
xs: List[Key] |
122 |
): Map[Key, Long] = { |
|
70800 | 123 |
def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] = |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
124 |
if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs |
73359 | 125 |
else next(x).foldLeft(rs + (x -> length))(reach(length + count(x))) |
126 |
xs.foldLeft(Map.empty[Key, Long])(reach(0)) |
|
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
127 |
} |
70800 | 128 |
def node_height(count: Key => Long): Map[Key, Long] = |
71601 | 129 |
reachable_length(count, imm_preds, maximals) |
70800 | 130 |
def node_depth(count: Key => Long): Map[Key, Long] = |
71601 | 131 |
reachable_length(count, imm_succs, minimals) |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
132 |
|
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
133 |
/*reachable nodes with size limit*/ |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70764
diff
changeset
|
134 |
def reachable_limit( |
70800 | 135 |
limit: Long, |
136 |
count: Key => Long, |
|
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70764
diff
changeset
|
137 |
next: Key => Keys, |
75393 | 138 |
xs: List[Key] |
139 |
): Keys = { |
|
140 |
def reach(res: (Long, Keys), x: Key): (Long, Keys) = { |
|
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
141 |
val (n, rs) = res |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70764
diff
changeset
|
142 |
if (rs.contains(x)) res |
73359 | 143 |
else next(x).foldLeft((n + count(x), rs + x))(reach) |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
144 |
} |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
145 |
|
70800 | 146 |
@tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys = |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
147 |
rest match { |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70764
diff
changeset
|
148 |
case Nil => rs |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
149 |
case head :: tail => |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
150 |
val (size1, rs1) = reach((size, rs), head) |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70764
diff
changeset
|
151 |
if (size > 0 && size1 > limit) rs |
70764
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
152 |
else reachs(size1, rs1, tail) |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
153 |
} |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
154 |
|
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
155 |
reachs(0, empty_keys, xs) |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
156 |
} |
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
157 |
|
6d36b30fdd67
more operations -- incremental exploration of reachable nodes;
wenzelm
parents:
70699
diff
changeset
|
158 |
/*reachable nodes with result in topological order (for acyclic graphs)*/ |
75393 | 159 |
private def reachable( |
160 |
next: Key => Keys, |
|
161 |
xs: List[Key], |
|
162 |
rev: Boolean = false |
|
163 |
): (List[List[Key]], Keys) = { |
|
164 |
def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) = { |
|
46611 | 165 |
val (rs, r_set) = reached |
166 |
if (r_set(x)) reached |
|
167 |
else { |
|
72065
11dc8929832d
clarified order --- proper sorting of requirements;
wenzelm
parents:
71601
diff
changeset
|
168 |
val (rs1, r_set1) = |
73359 | 169 |
if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) } |
73360 | 170 |
else next(x).foldRight((rs, r_set + x))(reach) |
46611 | 171 |
(x :: rs1, r_set1) |
172 |
} |
|
173 |
} |
|
75393 | 174 |
def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = { |
46611 | 175 |
val (rss, r_set) = reached |
48350
09bf3b73e446
clarified topological ordering: preserve order of adjacency via reverse fold;
wenzelm
parents:
48348
diff
changeset
|
176 |
val (rs, r_set1) = reach(x, (Nil, r_set)) |
46611 | 177 |
(rs :: rss, r_set1) |
178 |
} |
|
73359 | 179 |
xs.foldLeft((List.empty[List[Key]], empty_keys))(reachs) |
46611 | 180 |
} |
181 |
||
182 |
/*immediate*/ |
|
183 |
def imm_preds(x: Key): Keys = get_entry(x)._2._1 |
|
184 |
def imm_succs(x: Key): Keys = get_entry(x)._2._2 |
|
185 |
||
186 |
/*transitive*/ |
|
72065
11dc8929832d
clarified order --- proper sorting of requirements;
wenzelm
parents:
71601
diff
changeset
|
187 |
def all_preds_rev(xs: List[Key]): List[Key] = |
11dc8929832d
clarified order --- proper sorting of requirements;
wenzelm
parents:
71601
diff
changeset
|
188 |
reachable(imm_preds, xs, rev = true)._1.flatten.reverse |
46611 | 189 |
def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten |
190 |
def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten |
|
191 |
||
46613 | 192 |
/*strongly connected components; see: David King and John Launchbury, |
193 |
"Structuring Depth First Search Algorithms in Haskell"*/ |
|
194 |
def strong_conn: List[List[Key]] = |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
195 |
reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse |
46613 | 196 |
|
46611 | 197 |
|
198 |
/* minimal and maximal elements */ |
|
199 |
||
200 |
def minimals: List[Key] = |
|
73359 | 201 |
rep.foldLeft(List.empty[Key]) { |
202 |
case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms |
|
203 |
} |
|
46611 | 204 |
|
205 |
def maximals: List[Key] = |
|
73359 | 206 |
rep.foldLeft(List.empty[Key]) { |
207 |
case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms |
|
208 |
} |
|
46611 | 209 |
|
210 |
def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty |
|
211 |
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty |
|
212 |
||
66830 | 213 |
def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x) |
214 |
||
46611 | 215 |
|
46668 | 216 |
/* node operations */ |
46611 | 217 |
|
75393 | 218 |
def new_node(x: Key, info: A): Graph[Key, A] = { |
48648 | 219 |
if (defined(x)) throw new Graph.Duplicate(x) |
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
220 |
else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys)))) |
46611 | 221 |
} |
222 |
||
46613 | 223 |
def default_node(x: Key, info: A): Graph[Key, A] = |
48648 | 224 |
if (defined(x)) this else new_node(x, info) |
46613 | 225 |
|
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
226 |
private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key) |
d2ac78ba805e
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset
|
227 |
: SortedMap[Key, Entry] = |
46611 | 228 |
map.get(y) match { |
229 |
case None => map |
|
230 |
case Some((i, (preds, succs))) => |
|
231 |
map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x))) |
|
232 |
} |
|
233 |
||
75393 | 234 |
def del_node(x: Key): Graph[Key, A] = { |
46611 | 235 |
val (preds, succs) = get_entry(x)._2 |
236 |
new Graph[Key, A]( |
|
73359 | 237 |
succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x))) |
46611 | 238 |
} |
239 |
||
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset
|
240 |
def restrict(pred: Key => Boolean): Graph[Key, A] = |
73359 | 241 |
iterator.foldLeft(this) { case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } |
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset
|
242 |
|
70699 | 243 |
def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name)) |
244 |
||
46611 | 245 |
|
46668 | 246 |
/* edge operations */ |
46611 | 247 |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59245
diff
changeset
|
248 |
def edges_iterator: Iterator[(Key, Key)] = |
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59245
diff
changeset
|
249 |
for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y) |
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59245
diff
changeset
|
250 |
|
46611 | 251 |
def is_edge(x: Key, y: Key): Boolean = |
48507 | 252 |
defined(x) && defined(y) && imm_succs(x)(y) |
46611 | 253 |
|
254 |
def add_edge(x: Key, y: Key): Graph[Key, A] = |
|
255 |
if (is_edge(x, y)) this |
|
256 |
else |
|
257 |
map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }). |
|
258 |
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) }) |
|
259 |
||
260 |
def del_edge(x: Key, y: Key): Graph[Key, A] = |
|
261 |
if (is_edge(x, y)) |
|
262 |
map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }). |
|
263 |
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) }) |
|
264 |
else this |
|
265 |
||
266 |
||
267 |
/* irreducible paths -- Hasse diagram */ |
|
268 |
||
75393 | 269 |
private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] = { |
46611 | 270 |
def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z |
271 |
@tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] = |
|
272 |
xs0 match { |
|
273 |
case Nil => xs1 |
|
274 |
case x :: xs => |
|
60215 | 275 |
if (!x_set(x) || x == z || path.contains(x) || |
46611 | 276 |
xs.exists(red(x)) || xs1.exists(red(x))) |
277 |
irreds(xs, xs1) |
|
278 |
else irreds(xs, x :: xs1) |
|
279 |
} |
|
280 |
irreds(imm_preds(z).toList, Nil) |
|
281 |
} |
|
282 |
||
75393 | 283 |
def irreducible_paths(x: Key, y: Key): List[List[Key]] = { |
46611 | 284 |
val (_, x_set) = reachable(imm_succs, List(x)) |
285 |
def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] = |
|
286 |
if (x == z) (z :: path) :: ps |
|
73359 | 287 |
else irreducible_preds(x_set, path, z).foldLeft(ps)(paths(z :: path)) |
46611 | 288 |
if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y) |
289 |
} |
|
290 |
||
291 |
||
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
292 |
/* transitive closure and reduction */ |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
293 |
|
75393 | 294 |
private def transitive_step(z: Key): Graph[Key, A] = { |
50447
2e22cdccdc38
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
wenzelm
parents:
50445
diff
changeset
|
295 |
val (preds, succs) = get_entry(z)._2 |
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
296 |
var graph = this |
50447
2e22cdccdc38
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
wenzelm
parents:
50445
diff
changeset
|
297 |
for (x <- preds; y <- succs) graph = graph.add_edge(x, y) |
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
298 |
graph |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
299 |
} |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
300 |
|
73359 | 301 |
def transitive_closure: Graph[Key, A] = keys_iterator.foldLeft(this)(_.transitive_step(_)) |
50447
2e22cdccdc38
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
wenzelm
parents:
50445
diff
changeset
|
302 |
|
75393 | 303 |
def transitive_reduction_acyclic: Graph[Key, A] = { |
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
304 |
val trans = this.transitive_closure |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
305 |
if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) })) |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50447
diff
changeset
|
306 |
error("Cyclic graph") |
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
307 |
|
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
308 |
var graph = this |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
309 |
for { |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50452
diff
changeset
|
310 |
(x, (_, (_, succs))) <- iterator |
50445
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
311 |
y <- succs |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
312 |
if trans.imm_preds(y).exists(z => trans.is_edge(x, z)) |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
313 |
} graph = graph.del_edge(x, y) |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
314 |
graph |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
315 |
} |
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
316 |
|
68c9a6538c0e
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm
parents:
49560
diff
changeset
|
317 |
|
46611 | 318 |
/* maintain acyclic graphs */ |
319 |
||
320 |
def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] = |
|
321 |
if (is_edge(x, y)) this |
|
322 |
else { |
|
323 |
irreducible_paths(y, x) match { |
|
324 |
case Nil => add_edge(x, y) |
|
325 |
case cycles => throw new Graph.Cycles(cycles.map(x :: _)) |
|
326 |
} |
|
327 |
} |
|
328 |
||
48348 | 329 |
def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] = |
73359 | 330 |
xs.foldLeft(this)(_.add_edge_acyclic(_, y)) |
46611 | 331 |
|
332 |
def topological_order: List[Key] = all_succs(minimals) |
|
333 |
} |