pytact.graph_visualize_browse

  1from dataclasses import dataclass, field
  2import os
  3import graphviz
  4from collections import defaultdict
  5from abc import ABC, abstractmethod
  6from pathlib import Path
  7from typing import Union, List, Dict, Set, Tuple, Sequence
  8from pytact.data_reader import Dataset, Definition, Node, ProofState, Original, Discharged, Substituted
  9import html
 10import inflection
 11import capnp
 12import pytact.graph_api_capnp as graph_api_capnp
 13import pytact.graph_api_capnp_cython as apic
 14
 15class UrlMaker(ABC):
 16
 17    @abstractmethod
 18    def definition(self, fname: Path, defid: int) -> str:
 19        pass
 20    @abstractmethod
 21    def proof(self, fname: Path, defid: int) -> str:
 22        pass
 23    @abstractmethod
 24    def outcome(self, fname: Path, defid: int, stepi: int, outcomei: int) -> str:
 25        pass
 26    @abstractmethod
 27    def global_context(self, fname: Path) -> str:
 28        pass
 29    @abstractmethod
 30    def folder(self, path: Path) -> str:
 31        pass
 32    @abstractmethod
 33    def root_folder(self) -> str:
 34        pass
 35
 36@dataclass
 37class Settings:
 38    no_defaults: bool = False # Should we use default settings?
 39    ignore_edges: List[int] = field(default_factory=lambda: [])
 40    unshare_nodes: List[int] = field(default_factory=lambda: [])
 41    show_trivial_evar_substs: bool = False
 42    hide_proof_terms: bool = False
 43    show_edge_labels: bool = False
 44    order_edges: bool = False
 45    concentrate_edges: bool = False
 46    show_non_anonymized_tactics: bool = False
 47    max_depth: int = 0
 48    max_size: int = 100
 49
 50    def __post_init__(self):
 51        if not self.no_defaults:
 52            self.ignore_edges = [graph_api_capnp.EdgeClassification.schema.enumerants['constOpaqueDef']]
 53            label = graph_api_capnp.Graph.Node.Label
 54            self.unshare_nodes = [label.definition.value, label.sortSProp.value,
 55                                  label.sortProp.value, label.sortSet.value, label.sortType.value]
 56
 57@dataclass
 58class GraphVisualizationData:
 59    data: Dict[Path, Dataset]
 60    trans_deps: Dict[Path, Set[Path]] = field(init=False)
 61    graphid2path: List[Path] = field(init=False)
 62
 63    def __post_init__(self):
 64        self.trans_deps = transitive_closure({d.filename: list(d.dependencies)
 65                                              for d in self.data.values()})
 66        self.graphid2path = [d.filename for d in sorted(self.data.values(), key=lambda d: d.graph)]
 67
 68@dataclass
 69class GraphVisualizationOutput:
 70    svg: str
 71    location: List[Tuple[str, str]] # tuple[Name, URL]
 72    active_location: int
 73    text: List[str] = field(default_factory=lambda: [])
 74    popups: List[Tuple[str, str]] = field(default_factory=lambda: []) # DOM id, text
 75
 76def node_label_map(node: Node) -> Tuple[str, str, str]:
 77    enum = apic.Graph_Node_Label_Which
 78    label = node.label
 79    if d := node.definition:
 80        name = d.name
 81        return (
 82            'box', name.split('.')[-1],
 83            f"{inflection.camelize(node.label.definition.which.name.lower())} {d.name}"
 84        )
 85    which = label.which
 86    if which == enum.SORT_PROP:
 87        return 'ellipse', 'Prop', 'SortProp'
 88    elif which == enum.SORT_S_PROP:
 89        return 'ellipse', 'SProp', 'SortSProp'
 90    elif which == enum.SORT_SET:
 91        return 'ellipse', 'Set', 'SortSet'
 92    elif which == enum.SORT_TYPE:
 93        return 'ellipse', 'Type', 'SortType'
 94    elif which == enum.REL:
 95        return 'circle', '↑', 'rel'
 96    elif which == enum.PROD:
 97        return 'circle', '∀', 'prod'
 98    elif which == enum.LAMBDA:
 99        return 'circle', 'λ', 'lambda'
100    elif which == enum.LET_IN:
101        return 'ellipse', 'let', 'LetIn'
102    elif which == enum.APP:
103        return 'circle', '@', 'app'
104    elif which == enum.CASE_BRANCH:
105        return 'ellipse', 'branch', 'CaseBranch'
106    else:
107        name = inflection.camelize(label.which.name.lower())
108        return 'ellipse', name, name
109
110def truncate_string(data, maximum):
111    return data[:(maximum-2)] + '..' if len(data) > maximum else data
112
113def make_label(context, name):
114    name_split = name.split('.')
115    common = os.path.commonprefix([name_split, context.split('.')])
116    return '.'.join(name_split[len(common):])
117
118def graphviz_escape(s):
119    return s.replace('\\', '\\\\')
120
121def make_tooltip(d):
122    return f"{inflection.camelize(d.node.label.definition.which.name.lower())} {d.name}"
123
124def render_proof_state_text(ps: ProofState):
125    return ('<br>'.join(ps.context_text) +
126            '<br>----------------------<br>' + ps.conclusion_text +
127            '<br><br>Raw: ' + ps.text)
128
129class GraphVisualizator:
130    def __init__(self, data: GraphVisualizationData, url_maker: UrlMaker, settings: Settings = Settings()):
131        self.data = data.data
132        self.trans_deps = data.trans_deps
133        self.graphid2path = data.graphid2path
134        self.url_maker = url_maker
135        self.settings = settings
136        self.node_counter = 0
137
138
139        arrow_heads = [ "dot", "inv", "odot", "invdot", "invodot" ]
140        edge_arrow_map = {}
141        for group in graph_api_capnp.groupedEdges:
142            for i, sort in enumerate(group.conflatable):
143                edge_arrow_map[sort.raw] = arrow_heads[i]
144        self.edge_arrow_map = edge_arrow_map
145
146    def url_for_path(self, r: Path):
147        if r in self.data:
148            return r.with_suffix('').parts[-1], self.url_maker.global_context(r)
149        elif len(r.parts) > 0:
150            return r.parts[-1], self.url_maker.folder(r)
151        else:
152            return 'dataset', self.url_maker.root_folder()
153
154    def path2location(self, path: Path):
155        return [self.url_for_path(parent) for parent in list(reversed(path.parents)) + [path]]
156
157    def dot_apply_style(self, dot):
158        dot.attr('node', fontsize='11', fontname="Helvetica", margin='0', height='0.3',
159                 style="rounded, filled", penwidth="0")
160        dot.attr('edge', fontsize='11', fontname="Helvetica", arrowsize='0.5', penwidth="0.6")
161        dot.attr('graph', fontsize='11', fontname="Helvetica", penwidth="0.6", ranksep='0.3')
162        if self.settings.order_edges:
163            dot.attr('graph', ordering='out')
164        if self.settings.concentrate_edges:
165            dot.attr('graph', concentrate='true')
166
167
168    def render_node(self, dot, node: Node, shape: str, label: str, id: Union[str, None] = None,
169                    tooltip: Union[str, None] = None):
170        if not id:
171            id = str(node)
172        if not tooltip:
173            tooltip = label
174        url = None
175        if node.definition:
176            url = self.url_maker.definition(self.graphid2path[node.graph], node.nodeid)
177        dot.node(id, label, URL = url, shape = shape, tooltip = tooltip)
178        return id
179
180    def render_file_node(self, dot, f: Path):
181        label = f"File: {f.with_suffix('')}"
182        node_id = f"file-{f}"
183        dot.node(node_id, label, URL = self.url_maker.global_context(f), shape='box')
184        return node_id
185
186    def global_context(self, fname: Path):
187        dot = graphviz.Digraph(format='svg')
188        self.dot_apply_style(dot)
189        dot.attr('graph', compound="true")
190
191        dataset = self.data[fname]
192        representative = dataset.representative
193        module_name = dataset.module_name
194
195        def render_def(dot2, d: Definition):
196            label = make_label(module_name, d.name)
197            if representative and representative.node == d.node:
198                label = "Representative: " + label
199            tooltip = make_tooltip(d)
200            if isinstance(d.status, Original):
201                id = self.render_node(dot2, d.node, 'box', label, tooltip=tooltip)
202            elif isinstance(d.status, Discharged):
203                id = self.render_node(dot2, d.node, 'box', label, tooltip=tooltip)
204                target = d.status.original
205                dot.edge(id, repr(target.node),
206                         arrowtail="inv", dir="both", constraint="false", style="dashed")
207            elif isinstance(d.status, Substituted):
208                target = d.status.original
209                if d.node.graph == target.node.graph:
210                    id = self.render_node(dot2, d.node, 'box', label, tooltip=tooltip)
211                    dot.edge(id, str(target.node),
212                             arrowtail="odot", dir="both", constraint="false", style="dashed")
213                else:
214                    with dot2.subgraph() as dot3:
215                        dot3.attr(rank='same')
216                        id = self.render_node(dot3, d.node, 'box', label, tooltip=tooltip)
217                        id2 = self.render_node(dot3, target.node, 'box',
218                                               make_label(module_name, target.name),
219                                               tooltip=make_tooltip(target))
220                        dot.edge(id, id2,
221                                 arrowtail="odot", dir="both", constraint="false", style="dashed")
222
223        for cluster in dataset.clustered_definitions():
224
225            start = str(cluster[0].node)
226            ltail = None
227            if len(cluster) == 1:
228                render_def(dot, cluster[0])
229            else:
230                ltail = "cluster_"+start
231                with dot.subgraph(name=ltail) as dot2:
232                    dot2.attr('graph', style='rounded')
233                    last = None
234                    for d in cluster:
235                        render_def(dot2, d)
236                        if last:
237                            dot2.edge(str(last.node), str(d.node), style="invis")
238                        last = d
239
240            if prev := cluster[-1].previous:
241                target = str(prev.node)
242                lhead = None
243                if len(list(prev.cluster)) > 1:
244                    lhead = "cluster_"+target
245                dot.edge(str(cluster[-1].node), target, lhead = lhead, ltail = ltail)
246            for fi in cluster[-1].external_previous:
247                fid = self.render_file_node(dot, self.graphid2path[fi.node.graph])
248                dot.edge(str(cluster[-1].node), fid, ltail = ltail)
249
250        location = self.path2location(fname)
251        return GraphVisualizationOutput(dot.source, location, len(location) - 1)
252
253    def visualize_term(self, dot, start: Node, depth, depth_ignore: Set[Node] = set(),
254                       max_nodes=100, seen: Union[Dict[str, str], None]=None,
255                       node_label_map=node_label_map,
256                       prefix='', before_prefix='', proof_state_prefix: Dict[int, str] = {}
257                       ) -> str:
258        if seen == None:
259            seen = {}
260        nodes_left = max_nodes
261        def recurse(node: Node, depth, context_prefix):
262            nonlocal seen
263            nonlocal nodes_left
264
265            enum = graph_api_capnp.Graph.Node.Label
266            which = node.label.which
267            if which == enum.proofState:
268                node_prefix = context_prefix
269            elif which == enum.contextAssum:
270                node_prefix = context_prefix
271            elif which == enum.contextDef:
272                node_prefix = context_prefix
273            elif which == enum.evarSubst:
274                node_prefix = prefix + context_prefix
275            else:
276                node_prefix = prefix
277            id = node_prefix + str(node)
278            if id in seen:
279                return seen[id]
280            dot_id = f"c{self.node_counter}-{id}"
281            seen[id] = dot_id
282            nodes_left -= 1
283            self.node_counter += 1
284            if nodes_left < 0:
285                id = 'trunc' + str(self.node_counter)
286                dot.node(id, 'truncated')
287                return id
288
289            shape, label, tooltip = node_label_map(node)
290            self.render_node(dot, node, shape, label, id=dot_id, tooltip=tooltip)
291            if node.definition and not node in depth_ignore:
292                depth -= 1
293            if depth >= 0:
294                if node.label.which == graph_api_capnp.Graph.Node.Label.evar:
295                    # Find the evar-id
296                    evarid = [c.label.proof_state.value for _, c in node.children
297                              if c.label.which == graph_api_capnp.Graph.Node.Label.proofState][0]
298                    context_prefix = proof_state_prefix.get(evarid, context_prefix)
299
300                for edge, child in node.children:
301                    if edge in self.settings.ignore_edges:
302                        continue
303                    if child.label.which == graph_api_capnp.Graph.Node.Label.evarSubst:
304                        substs = [s for _, s in child.children]
305                        if not self.settings.show_trivial_evar_substs and substs[0] == substs[1]:
306                            continue
307                    cid = recurse(child, depth,
308                                    before_prefix if edge == graph_api_capnp.EdgeClassification.evarSubstTerm
309                                    else context_prefix)
310                    edge_name = inflection.camelize(apic.EdgeClassification(edge).name.lower())
311                    if self.settings.show_edge_labels:
312                        label = edge_name
313                    else:
314                        label = ""
315                    dot.edge(dot_id, cid, label=label, tooltip=edge_name, labeltooltip=edge_name,
316                                arrowtail=self.edge_arrow_map[edge], dir="both")
317            if node.label.which_raw in self.settings.unshare_nodes:
318                del seen[id]
319            return dot_id
320        id = recurse(start, depth, before_prefix)
321        return id
322
323    def definition(self, fname: Path, definition: int):
324        dot = graphviz.Digraph(format='svg')
325        self.dot_apply_style(dot)
326
327        start = self.data[fname].node_by_id(definition)
328        depth_ignore = set()
329        if d := start.definition:
330            depth_ignore = {d.node for d in start.definition.cluster}
331        depth = self.settings.max_depth
332        max_nodes = self.settings.max_size
333
334        self.visualize_term(dot, start, depth=depth, depth_ignore=depth_ignore,
335                            max_nodes=max_nodes)
336
337        location = self.path2location(fname)
338        ext_location = location
339        label = "[not a definition]"
340        text = []
341        proof = []
342        if d := start.definition:
343            label = d.name
344            text = [f"Type: {d.type_text}"]
345            if term := d.term_text:
346                text.append(f"Term: {term}")
347            if d.proof:
348                proof = [("Proof", self.url_maker.proof(fname, definition))]
349        ext_location = (
350            location +
351            [(make_label(self.data[fname].module_name, label),
352              self.url_maker.definition(fname, definition))] +
353            proof)
354        return GraphVisualizationOutput(dot.source, ext_location, len(location), text)
355
356    def proof(self, fname: Path, definition: int):
357        node = self.data[fname].node_by_id(definition)
358        d = node.definition
359        if not d:
360            assert False
361        proof = d.proof
362        if not proof:
363            assert False
364
365        dot = graphviz.Digraph(format='svg')
366        self.dot_apply_style(dot)
367        dot.attr('node', style="filled", fillcolor="white", penwidth="0.6")
368        dot.attr('graph', ordering="out")
369        surrogates = set()
370        outcome_to_id = {}
371        for i, step in enumerate(proof):
372            for j, outcome in enumerate(step.outcomes):
373                id = str(outcome.before.id)
374                while id in surrogates:
375                    id = id + '-s'
376                surrogates.add(id)
377                outcome_to_id[(i, j)] = id
378        for i, step in enumerate(proof):
379            with dot.subgraph(name='cluster_' + str(i)) as dot2:
380                dot2.attr('graph', labelloc="b", style="rounded")
381                if tactic := step.tactic:
382                    if self.settings.show_non_anonymized_tactics:
383                        tactic_text = tactic.text_non_anonymous
384                    else:
385                        tactic_text = tactic.text
386                else:
387                    tactic_text = 'unknown'
388                dot2.attr(label=tactic_text)
389                for j, outcome in enumerate(step.outcomes):
390                    before_id = outcome_to_id[(i, j)]
391                    dot2.node(before_id, label='⬤', shape='circle', fontsize="7", height="0.25pt",
392                              URL = self.url_maker.outcome(fname, definition, i, j))
393                    for after in outcome.after:
394                        if outcome.before.id == after.id:
395                            after_id = before_id + '-s'
396                            style = 'dashed'
397                        else:
398                            after_id = str(after.id)
399                            style = 'solid'
400                        dot.edge(before_id, after_id, style=style)
401                    if not outcome.after:
402                        qedid = str('qed-'+str(i)+'-'+str(j))
403                        dot2.node(qedid, label='', shape='point', height='0.05', fillcolor='black')
404                        dot.edge(before_id, qedid)
405
406        location = (self.path2location(fname) +
407                    [(make_label(self.data[fname].module_name, d.name),
408                      self.url_maker.definition(fname, definition)),
409                     ("Proof", self.url_maker.proof(fname, definition))])
410        return GraphVisualizationOutput(dot.source, location, len(location) - 1)
411
412    def outcome(self, fname: Path, definition: int, stepi: int, outcomei: int):
413        depth = self.settings.max_depth
414        max_nodes = self.settings.max_size
415        node = self.data[fname].node_by_id(definition)
416        d = node.definition
417        if not d:
418            assert False
419        proof = d.proof
420        if not proof:
421            assert False
422
423        dot = graphviz.Digraph(format='svg')
424        self.dot_apply_style(dot)
425
426        outcome = proof[stepi].outcomes[outcomei]
427        seen = {}
428
429        def node_label_map_with_ctx_names(context: Sequence[Node],
430                                          context_text: Sequence[str]):
431            mapping = {n: s for n, s in zip(context, context_text)}
432            def nlm(node: Node):
433                enum = graph_api_capnp.Graph.Node.Label
434                which = node.label.which
435                if which == enum.contextAssum:
436                    name = graphviz_escape(mapping[node])
437                    return 'ellipse', truncate_string(name, 20), f"ContextAssum {name}"
438                elif which == enum.contextDef:
439                    name = graphviz_escape(mapping[node])
440                    return 'ellipse', truncate_string(name, 20), f"ContextDef {name}"
441                else:
442                        return node_label_map(node)
443            return nlm
444
445        popups = []
446
447        with dot.subgraph(name='cluster_before') as dot2:
448            ps = outcome.before
449            dot2.attr('graph',
450                      label=f"Before state\n{graphviz_escape(truncate_string(ps.conclusion_text, 70))}",
451                      tooltip=f"Before state {graphviz_escape(ps.conclusion_text)}",
452                      id='before-state')
453            popups.append(('before-state', render_proof_state_text(ps)))
454            prefix = 'before'
455            self.visualize_term(dot2, ps.root, depth=depth, prefix=prefix, before_prefix=prefix,
456                                max_nodes=max_nodes, seen=seen,
457                                node_label_map=node_label_map_with_ctx_names(ps.context, ps.context_text))
458
459        with dot.subgraph(name='cluster_tactic') as dot2:
460            prefix = 'before'
461            tactic_text = 'unknown'
462            tactic_base_text = 'unknown'
463            if t := outcome.tactic:
464                tactic_text = t.text
465                tactic_base_text = (t.base_text.replace('__argument_marker__', '_')
466                                    .replace('private_constant_placeholder', '_'))
467            dot2.attr('graph', label=f"Tactic\n{tactic_text}")
468            dot2.node('tactic', label = tactic_base_text)
469            for i, arg in enumerate(outcome.tactic_arguments):
470                if arg is None:
471                    dot2.node(f"tactic-arg{i}", label=f"arg {i}: unknown")
472                else:
473                    id = self.visualize_term(dot2, arg, depth=depth, prefix=prefix, before_prefix=prefix,
474                                        max_nodes=max_nodes, seen=seen)
475                    dot2.node(f"tactic-arg{i}", label=f"arg {i}")
476                    dot2.edge(f"tactic-arg{i}", id)
477                dot2.edge('tactic', f"tactic-arg{i}")
478
479
480        for ai, after in enumerate(outcome.after):
481            with dot.subgraph(name='cluster_after' + str(ai)) as dot2:
482                dot2.attr('graph',
483                          label=f"After state {ai}\n{graphviz_escape(truncate_string(after.conclusion_text, 70))}",
484                          tooltip=f"After state {ai} {graphviz_escape(after.conclusion_text)}",
485                          id=f'after-state{ai}')
486                popups.append((f'after-state{ai}', render_proof_state_text(after)))
487                prefix = f'after{ai}'
488                self.visualize_term(dot2, after.root, depth=depth, prefix=prefix, before_prefix=prefix,
489                                    max_nodes=max_nodes, seen=seen,
490                                    node_label_map=node_label_map_with_ctx_names(after.context, after.context_text))
491
492        if not self.settings.hide_proof_terms:
493            with dot.subgraph(name='cluster_term') as dot2:
494                dot2.attr('graph',
495                          label=f"Proof term\n{graphviz_escape(truncate_string(outcome.term_text, 70))}",
496                          tooltip=f"Proof term {graphviz_escape(outcome.term_text)}",
497                          id='proof-term')
498                popups.append(('proof-term', outcome.term_text))
499                prefix = 'term'
500                proof_state_prefix = {after.id: f'after{ai}' for ai, after in enumerate(outcome.after)}
501                id = self.visualize_term(dot2, outcome.term, depth=depth, prefix=prefix, before_prefix='before',
502                                    proof_state_prefix=proof_state_prefix,
503                                    max_nodes=max_nodes, seen=seen)
504                # Sometimes the subgraph is completely empty because the term is contained in another subgraph.
505                # Therefore, we artificially add a extra root node
506                dot2.node('artificial-root', 'TermRoot')
507                dot2.edge('artificial-root', id)
508
509        location = (self.path2location(fname) +
510                    [(make_label(self.data[fname].module_name, d.name),
511                      self.url_maker.definition(fname, definition)),
512                     ("Proof", self.url_maker.proof(fname, definition)),
513                     (f"Step {stepi} outcome {outcomei}",
514                      self.url_maker.outcome(fname, definition, stepi, outcomei))])
515        return GraphVisualizationOutput(dot.source, location, len(location) - 1, [], popups)
516
517    def folder(self, expand_path: Path) -> GraphVisualizationOutput:
518        expand_parts = expand_path.parts
519
520        dot = graphviz.Digraph(engine='dot', format='svg')
521        self.dot_apply_style(dot)
522
523        hierarchy = {'files': [], 'subdirs': {}}
524        for f in self.data:
525            dirs = f.parent.parts
526            leaf = hierarchy
527            for d in dirs:
528                leaf['subdirs'].setdefault(d, {'files': [], 'subdirs': {}})
529                leaf = leaf['subdirs'][d]
530            leaf['files'].append(f)
531        def common_length(p1, p2):
532            return len(os.path.commonprefix([p1, p2]))
533        def retrieve_edges(rel, h, depth: int):
534            for n in h['files']:
535                deps = {Path(*d.parts[:depth+1]) for d in self.trans_deps[n]
536                        if common_length(d.parts, expand_parts) == depth}
537                rel[Path(*n.parts[:depth+1])] |= deps
538            for d in h['subdirs']:
539                retrieve_edges(rel, h['subdirs'][d], depth)
540            return rel
541        def tunnel_hierarchy(dot, h, depth):
542            if depth == len(expand_parts):
543                rel = retrieve_edges(defaultdict(set), h, depth)
544                (rel, repr) = transitive_reduction(rel)
545                for n in rel:
546                    if len(repr[n]) == 1:
547                        label, url = self.url_for_path(n)
548                        shape = 'box'
549                    else:
550                        label = '<<table border="0" cellborder="0" cellpadding="7">'
551                        for r in repr[n]:
552                            slabel, surl = self.url_for_path(r)
553                            label += f'<tr><td href="{html.escape(surl)}">{slabel}</td></tr>'
554                        label += "</table>>"
555                        url = None
556                        shape = 'plaintext'
557                    dot.node(str(n), label, URL = url, shape = shape)
558                for n, deps in rel.items():
559                    for d in deps:
560                        dot.edge(str(n), str(d))
561            else:
562                for d in h['subdirs']:
563                    cur_path: Path = Path(*expand_parts[:depth]) / d
564                    if depth < len(expand_parts) and d == expand_parts[depth]:
565                        cluster_name = 'cluster_' + str(cur_path)
566                        with dot.subgraph(name=cluster_name) as dot2:
567                            dot2.attr('graph', style="filled", fillcolor="white", label=d,
568                                      URL = self.url_maker.folder(Path(*expand_parts[:depth+1])))
569                            tunnel_hierarchy(dot2, h['subdirs'][d], depth+1)
570
571        with dot.subgraph(name='cluster_root') as dot2:
572            dot2.attr('graph', style="filled", fillcolor="white", label='dataset',
573                      URL = self.url_maker.root_folder())
574            tunnel_hierarchy(dot2, hierarchy, 0)
575
576        location = self.path2location(expand_path)
577        return GraphVisualizationOutput(dot.source, location, len(location) - 1)
578
579def transitive_closure(rel):
580    trans_deps = defaultdict(set)
581    def calc_trans_deps(a, n):
582        for d in rel[n]:
583            if d not in trans_deps[a]:
584                trans_deps[a].add(d)
585                calc_trans_deps(a, d)
586    for n in list(rel.keys()):
587        calc_trans_deps(n, n)
588    return trans_deps
589
590def transitive_reduction(rel):
591    """This is not a real transitive reduction (NP-hard when it needs to be a subgraph).
592    This is an approximation where all strongly connected components are smashed together
593    in one node.
594    """
595    trans_deps = transitive_closure(rel)
596    repr_items = defaultdict(set)
597    representative = {}
598    def calc_components(n):
599        if n in representative:
600            return
601        repr_items[n].add(n)
602        representative[n] = n
603        for d in trans_deps[n]:
604            if n in trans_deps[d]:
605                repr_items[n].add(d)
606                representative[d] = n
607    for n in list(rel.keys()):
608        calc_components(n)
609    repr_trans_rel = defaultdict(set)
610    def calc_new_trans_deps(n):
611        for d in trans_deps[n]:
612            if n not in trans_deps[d]:
613                repr_trans_rel[n].add(representative[d])
614    for n in list(rel.keys()):
615        calc_new_trans_deps(n)
616    def calc_sparse_deps(n):
617        res = set()
618        for d in repr_trans_rel[n]:
619            k = [d2 for d2 in repr_trans_rel[n]
620                 if d != d2 and d in trans_deps[d2]]
621            if not k:
622                res.add(d)
623        return res
624    k = {n: calc_sparse_deps(n) for n in repr_items}
625    return (k, repr_items)