Source code for resmt.visualizations

"""
visualizations.py
=================

This module contains some adaptations e.g. of the standard ``networkx`` drawing routines \
to the standard input data formats used in the ``datatypes`` sub-module of ``ReSMT``.


"""

#####################################################################################

# %% setup of logging tool for providing various level of feedback to the user:
import logging

# NOTE: in order to alter the behavior of the logging tool *after* having once
# executed the code below, it is necessary to restart Python and load the module
# again! (-> possibly find a nicer method to allow "on-the-fly" changes...)
from resmt import datatypes

logging.basicConfig(format='%(asctime)s.%(msecs)03d  %(message)s',
                    filename='visualizations.log',
                    # filemode='w',
                    # datefmt='%d/%m/%y %H:%M:%S',
                    datefmt='%H:%M:%S',
                    level=logging.INFO)  # set to logging.INFO for less verbose mode
# uncomment the following if an output to the console is also desired:
# logging.getLogger().addHandler(logging.StreamHandler())

logging.info('---------->visualizations.py module loaded<----------')

#####################################################################################

# %% Initialization:
# support for intelligent type-aliases
from typing import Any, Dict, List, Set, Tuple, NamedTuple, TypeVar, Type, Optional

import os
from pprint import pformat
from IPython.display import SVG, display, HTML

# set the interactive Python shell to recognize the current working directory:
import sys

sys.path.append(os.getcwd())

from collections import OrderedDict, Counter
import timeit
import numpy
import networkx as nx
import z3
import mpmath

import resmt.datatypes

from jinja2 import FileSystemLoader
from latex.jinja2 import make_env
from latex import build_pdf

import subprocess
import signal

from network2tikz import plot
import seaborn as sns

#### some nice available styles:
# 'seaborn-whitegrid', 'seaborn-pastel', 'seaborn'
####################################

# for plotting runtimes etc.:
import matplotlib
import matplotlib.pyplot as plt
from matplotlib import style
style.use('seaborn-white')
from mpl_toolkits.mplot3d import Axes3D

# allow for TeX forumlas in labels etc.:
# source: https://stackoverflow.com/questions/46259617/how-does-one-use-latex-amsmath-with-matplotlib
matplotlib.rc('text', usetex=True)
matplotlib.rc('font', **{'family': "sans-serif"})

# method compatible with matplotlib >= 3.3:
latexPreambleParams = [r'\usepackage{amsmath,amssymb}',
                                  r'\usepackage[english]{babel}',
                                  r'\usepackage[utf8]{inputenc}',
                                  r'\usepackage{sansmathfonts}',
                                  r'\usepackage[scaled=0.95]{helvet}',
                                  r'\renewcommand{\rmdefault}{\sfdefault}',
                                  r'\usepackage[T1]{fontenc}']

params = {'text.latex.preamble': '\n'.join(map(str, latexPreambleParams))}

plt.rcParams.update(params)
##########################################################################################################

# %%


[docs]class nxTypedDirectedGraph: """Networkx representation of typed directed graphs."""
[docs] def __init__(self, G: datatypes.Z3TypedDirectedGraph, drawGraph: bool = True, writeGraph: bool = False, fileName: str = None, gLayout: str = 'neato') -> None: """Instantiating a Networkx representation of a Z3TypedDirectedGraph. Args: G: a ``Z3TypedDirectedGraph`` instance drawGraph: (optional) a boolean controlling whether or not to draw the graph \ via the matplotlib plot commands after instantiation (default: ``True``) writeGraph: (optional) controls whether or not the graph should be written \ to a file (default: False) fileName: (optional) a filename for the graph, where the extension controls \ the output format (default: None) gLayout: (optional) a string controlling the graph layout for the interactive \ display (default: 'neato'; alternative options are those of ``GraphViz``, e.g. \ ``dot``, ``twopi``, ``fdp``, ``sfdp`` and ``circo``). .. note:: The available file-formats for the graph visualizations are those supported \ by the ``GraphViz`` package, i.e. either of the following ones: bmp canon cgimage cmap cmapx cmapx_np dot dot_json eps exr fig gd gd2 gif gv icns ico imap imap_np ismap jp2 jpe jpeg jpg json json0 mp pct pdf pic pict plain plain-ext png pov ps ps2 psd sgi svg svgz tga tif tiff tk vdx vml vmlz vrml wbmp webp xdot xdot1.2 xdot1.4 xdot_json """ # vertex and edge sets (in format of dictionaries of the format 'elName':'elSrt') self.vertices = G.vertices.els self.edges = G.edges.els # determine the number of vertex and edge sorts, and render suitable color palettes: vSorts = list(set(G.vertices.els.values())) eSorts = list(set(G.edges.els.values())) vertexColors = sns.color_palette("dark", len(vSorts)).as_hex() # render a version with alpha value of 0.5 for the node labels: alphaVL = 0.5 vertexLabelColors = sns.color_palette( [tuple(x + (1 - x) * (1 - alphaVL) for x in c) for c in sns.color_palette("dark", len(vSorts))] ).as_hex() edgeColors = sns.color_palette("dark", len(eSorts)).as_hex() vSrtToColor = {vSorts[i]: vertexColors[i] for i in range(len(vSorts))} vSrtToLabelColor = {vSorts[i]: vertexLabelColors[i] for i in range(len(vSorts))} eSrtToColor = {eSorts[i]: edgeColors[i] for i in range(len(eSorts))} # the incidence data: # NOTE: we filter out any potential nil-element mappings! self.stDict = {e:vs for e, vs in G.stDict.items() if e[:3] != 'nil'} # instantiate an empty multidigraph: self.graph = nx.MultiDiGraph() self.graph.nodes(data=True) # render the node sets from self.vertices and node color lists: nodeColors = [] nodeLabelColors = [] for vName, vSrt in self.vertices.items(): if vName[:3] != 'nil': self.graph.add_node(vName, sort=vSrt) nodeColors += [vSrtToColor[vSrt]] nodeLabelColors += [vSrtToLabelColor[vSrt]] self.nodeLabels = {vName: vName for vName in self.graph.nodes()} # render the edges from self.edges and self.stDict: edgeColors = [] edgeNames = [] for eName, eSrt in self.edges.items(): if eName[:3] != 'nil': vSrc, vTrgt = self.stDict[eName] self.graph.add_edge(vSrc, vTrgt, sort=eSrt) edgeColors += [eSrtToColor[eSrt]] edgeNames += [eName] self.edgeLabels = {self.stDict[eName]: eName for eName in self.edges.keys() if eName[:3] != 'nil'} self.pos = nx.fruchterman_reingold_layout(self.graph) # render a pydot visualization of the graph self.pydot = nx.drawing.nx_pydot.to_pydot(self.graph) # adjust the node styles: for n in self.pydot.get_nodes(): vSrt = n.get('sort') # Note: pydot requests rgb colors as a string with all three # subcolor values separated by a space, hence the conversion below: vColor = vSrtToColor[vSrt] vLabelColor = vSrtToLabelColor[vSrt] n.set_color('white') n.set_fontcolor(vLabelColor) n.set_fillcolor(vColor) n.set_shape('circle') n.set_style('filled') n.set_fontsize('6pt') n.set_fontname('Lato') n.set_margin('0.05') n.set_height('0.3') n.set_width('0.3') n.set_penwidth('0') n.set_fixedsize('True') # adjust the edge styles: for idx, e in enumerate(self.pydot.get_edges()): e.set_arrowsize('0.5') eSrt = e.get('sort') # Note: pydot requests rgb colors as a string with all three # subcolor values separated by a space, hence the conversion below: eColor = eSrtToColor[eSrt] e.set_color(eColor) e.set_fontcolor(eColor) e.set_fontsize('6pt') e.set_fontname('Lato') # read out the edge name by edge index: e.set_label(edgeNames[idx]) # write the graph to a file (if writeGraph == True and a non-empty filename is given): if writeGraph: if fileName is None: raise ValueError('Please specify a filename!') else: # write the SVG image to a file: fmt = fileName[-3:].lower() # format string # NOTE: the following call will automatically raise a value-error if a # format not supported by GraphViz is required (i.e. with supported formats # possibly evolving via the updates to that package) self.pydot.write(fileName, format=fmt, prog=gLayout) # draw the graph to the interactive plot console (if drawGraph == True) if drawGraph: # if drawGraph == True self.display = SVG(self.pydot.create(prog=gLayout, format='svg')) else: self.display = None
[docs]def displaySVGtable(tabData: Dict[str, List[str]], width:str ="100%") -> None: """"Display a set of SVG images in an HTML table. This method is adapted from code by \ `Brian Naughton <http://blog.booleanbiotech.com/ipython_notebook_tips.html)>`_. \ It allows to render a table of SVG images (with table headers), which provides \ a nice extension to the funcitonalities of ``Jupyter`` notebooks (since the default \ SVG image display would only permit a sequential output of SVG images). Args: tabData: a dictionary with entries of the form ``'header entry': ['SVG filename 1',...]``, \ i.e. the data necessary to fill a column of the table width: (optional) a string of the form ``"x%"``, with ``x`` an integer between ``0`` and ``100`` \ (default value: ``"100%"``) """ # initialize a HTML table specification: html = ["<table width:{}'><tr>".format(width)] # render the header entries: html += ["<th style=\"text-align:center\">{}</th>".format(h) for h in tabData.keys()] + ["</tr>"] # determine the maximal length of the columns: numRows = max([len(val) for key, val in tabData.items()]) for r in range(numRows): html += ["<tr>"] for hStr, cList in tabData.items(): if (r + 1) <= len(cList): html += ["<td style=\"align:center\"><img src='{}' /></td>".format(cList[r])] else: html += ["<td></td>"] html += ["</tr>"] html += ["</table>"] display(HTML(''.join(html)))