Source code for resmt.experiments

"""
experiments.py
==============

This module contains methods that permit render execution time tests, visualizations \
and other experiments with routines included in ``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...)
logging.basicConfig(format='%(asctime)s.%(msecs)03d  %(message)s',
                    filename='experiments.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('Start of log for experiments.')

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

# %% 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

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

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

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

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]def genOverlaps(setBname: str, elsBnames: List[str], setAname: str, elsAnames: List[str], S: z3.Solver) -> Tuple[List[float], str]: """Experimental overlap finding routine. Given names of two sets and lists of strings for naming the set elements, the routine \ prints out all solutions that may be formed for injective overlaps between elements of the \ sets. .. note:: As per the usual, each set contains one nil element, which is automatically generated. \ Therefore, it is possible to let either of the sets be the empty sets via specifying empty \ element name lists accordingly. Args: setBname: name of set B elsBnames: list of names of elements of set B setAname: name of set A elsAnames: list of names of elements of set A S: a Z3 solver instance Returns: All possible injective overlap solutions are logged to the logfile, a list of computation times \ until each individual ``sat`` result (and with the last entry the time until ``unsat``) and a \ string containing Z3 solver statistics data is returned. """ # declare enumeration sorts for the two finite input sets: setB, elsB = z3.EnumSort(setBname, tuple([setBname+'|nil']+elsBnames)) setA, elsA = z3.EnumSort(setAname, tuple([setAname+'|nil']+elsAnames)) logging.info('-----START OF EXPERIMENT-----\n') logging.info('\tSet elements of set B:\n%s' % elsB) logging.info('\tSet elements of set A:\n%s' % elsA) logging.info('\n\n --> starting search for solutions...\n\n') # declare a predicate function LambdaF: LambdaF = z3.Function('LambdaF', setB, setA, z3.BoolSort()) # assert that the nil-elements (= 0th entries of elsB, elsA) must be mapped: astLFnil = [LambdaF(elsB[0], elsA[0]) == True] # assert that the predicate function is injective: # auxiliary variables: y1, y2 = z3.Consts('y1 y2', setB) x1, x2 = z3.Consts('x1 x2', setA) astLFinj = [z3.ForAll([y1, x1, x2], z3.Implies( z3.And( LambdaF(y1, x1) == True, LambdaF(y1, x2) == True ), x1 == x2 ) ), z3.ForAll([y1, y2, x1], z3.Implies( z3.And( LambdaF(y1, x1) == True, LambdaF(y2, x1) == True ), y1 == y2 ) ) ] # add the assertions to the solver S: S.add(astLFnil + astLFinj) # set up a list of computation times: cTimes = [] # very first check for solutions (must return 'sat', since there always exists the trivial mapping): start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [t] nSols = 0 while chk == z3.sat: nSols += 1 m = S.model() LambdaFVals = {(yB, xA): m.eval(LambdaF(yB, xA)) for yB in elsB for xA in elsA if m.eval(LambdaF(yB,xA)) == True} # print only 'True' parts of assignments logging.info("\t\tSolution #\t %s\t for LambdaF (time to sol:\t %s):\n %s" % (nSols, t, LambdaFVals)) # "block" the present solution: astBlockSol = [z3.Exists([y1, x1], LambdaF(y1, x1) != m.eval(LambdaF(y1, x1)))] logging.info('---Assertion for block of solution:\n%s' % astBlockSol) S.add(astBlockSol) # check for solution: start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [t] logging.info('\t\tTime needed to confirm unsat:\t %s\n\n' % t) logging.info('Final number of solutions found:\t %s' % nSols) logging.info('Total computation time:\t %s\n ------ END OF EXPERIMENT ------\n' % sum(cTimes)) statsStr = str(S.statistics())[1:-1] return cTimes, statsStr
[docs]def genOverlapsV2(setBname: str, elsBnames: List[str], setAname: str, elsAnames: List[str], S: z3.Solver) -> Tuple[List[float], str]: """Experimental overlap finding routine. Given names of two sets and lists of strings for naming the set elements, the routine \ prints out all solutions that may be formed for injective overlaps between elements of the \ sets. The routine uses a Z3 ``simplify`` command in computing the assertions for blocking \ solutions (i.e. in the search for all solutions). .. note:: As per the usual, each set contains one nil element, which is automatically generated. \ Therefore, it is possible to let either of the sets be the empty sets via specifying empty \ element name lists accordingly. Args: setBname: name of set B elsBnames: list of names of elements of set B setAname: name of set A elsAnames: list of names of elements of set A S: a Z3 solver instance Returns: All possible injective overlap solutions are logged to the logfile, and a list of computation times \ until each individual ``sat`` result (and with the last entry the time until ``unsat``) is returned. """ # declare enumeration sorts for the two finite input sets: setB, elsB = z3.EnumSort(setBname, tuple([setBname+'|nil']+elsBnames)) setA, elsA = z3.EnumSort(setAname, tuple([setAname+'|nil']+elsAnames)) logging.info('-----START OF EXPERIMENT-----\n') logging.info('\tSet elements of set B:\n%s' % elsB) logging.info('\tSet elements of set A:\n%s' % elsA) logging.info('\n\n --> starting search for solutions...\n\n') # declare a predicate function LambdaF: LambdaF = z3.Function('LambdaF', setB, setA, z3.BoolSort()) # assert that the nil-elements (= 0th entries of elsB, elsA) must be mapped: astLFnil = [LambdaF(elsB[0], elsA[0]) == True] # assert that the predicate function is injective: # auxiliary variables: y1, y2 = z3.Consts('y1 y2', setB) x1, x2 = z3.Consts('x1 x2', setA) astLFinj = [z3.ForAll([y1, x1, x2], z3.Implies( z3.And( LambdaF(y1, x1) == True, LambdaF(y1, x2) == True ), x1 == x2 ) ), z3.ForAll([y1, y2, x1], z3.Implies( z3.And( LambdaF(y1, x1) == True, LambdaF(y2, x1) == True ), y1 == y2 ) ) ] # add the assertions to the solver S: S.add(astLFnil + astLFinj) # set up a list of computation times: cTimes = [] # very first check for solutions (must return 'sat', since there always exists the trivial mapping): start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [t] nSols = 0 while chk == z3.sat: nSols += 1 m = S.model() LambdaFVals = {(yB, xA): m.eval(LambdaF(yB, xA)) for yB in elsB for xA in elsA if m.eval(LambdaF(yB,xA)) == True} # print only 'True' parts of assignments logging.info("\t\tSolution #\t %s\t for LambdaF (time to sol:\t %s):\n %s" % (nSols, t, LambdaFVals)) # "block" the present solution: astBlockSolV2 = [z3.Exists([y1, x1], z3.simplify(LambdaF(y1, x1) != m.eval(LambdaF(y1, x1))))] logging.info('---Assertion for block of solution w/ simplification:\n%s' % astBlockSolV2) S.add(astBlockSolV2) # check for solution: start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [t] logging.info('\t\tTime needed to confirm unsat:\t %s\n\n' % t) logging.info('Final number of solutions found:\t %s' % nSols) logging.info('Total computation time:\t %s\n ------ END OF EXPERIMENT ------\n' % sum(cTimes)) statsStr = str(S.statistics())[1:-1] return cTimes, statsStr
# %%
[docs]def genExecTimePlot(cTimes: List[float], statsInfo: str, titleStr: str, fName: str) -> None: """Generate execution time Log-bar plot with average time marked. Args: cTimes: list of computation times (with the last entry the time until ``unsat``) titleStr: string to be used for the title of the plot fName: filename Returns: Renders a bar Log-plot with a dotted horizontal line marking the average execution \ time, and with the last bar (highlighted in a different color) indicating the time \ until ``unsat``; the plot is saved into a PDF with filename ``fName``. """ # use the seaborn "dark" palette: # palette = sns.color_palette("dark") fig, ax = plt.subplots() fig.set_tight_layout(False) fig.subplots_adjust(right=0.75) # make bar plots for the individual sat computation timings: ax.bar(range(1, len(cTimes)), cTimes[:-1], align='center', color=(0.0, 0.11, 0.5), label='time until sat' ) # make individual bar for unsat time: rects = ax.bar(len(cTimes), cTimes[-1], width=0.025*len(cTimes), color=(0.03, 0.46, 0.09), align='edge', label='unsat run: %ss' % numpy.round(cTimes[-1], 8) ) # plot an average execution time dotted line into the plot: avgCt = sum(cTimes) / len(cTimes) ax.axhline(y=avgCt, linewidth=1, linestyle=':', color='k', # color black label='avg. = %ss' % numpy.round(avgCt, 8) ) # label the axes: ax.set_yscale('log') ax.set_xlabel('computations') ax.set_ylabel('computation time (in s)') ax.set_title(titleStr) leg = ax.legend(bbox_to_anchor=(1.05, 1), loc=2, borderaxespad=0) # ax.legend(loc='best') fig.canvas.draw() # this draws the figure # which allows reading final coordinates in pixels leg_pxls = leg.get_window_extent() ax_pxls = ax.get_window_extent() fig_pxls = fig.get_window_extent() # Converting back to figure normalized coordinates to create new axis: pad = 0.025 ax2 = fig.add_axes([leg_pxls.x0 / fig_pxls.width, ax_pxls.y0 / fig_pxls.height, leg_pxls.width / fig_pxls.width, (leg_pxls.y0 - ax_pxls.y0) / fig_pxls.height - pad]) # eliminating all the tick marks: ax2.axis('off') # adding some information on statistics of the Z3 solver run: ax2.text(0, 0, statsInfo, fontsize=4) # save plot to file: plt.savefig(fName + '.pdf', bbox_inches="tight") # plt.tight_layout() # plt.show() # Note: the variant below is optimized for IPython notebook/sphinx-gallery documentation output! plt.close() # crop teh whitespace from the PDF produced subprocess.run(['pdfcrop', '--margins', '\"10\"', '%s.pdf' % fName, '%s.pdf' % fName], capture_output=True) # render a SVG variant of the PDF (for viewing in Jupyter notebooks etc.): subprocess.run(['pdf2svg', '%s.pdf' % fName, '%s.svg' % fName], capture_output=True) # show the plot # plt.show() display(SVG('%s.svg' % fName))
# %%
[docs]def genSetOverlapExperiment(S: z3.Solver, nAels: int, nBels: int, tStrExtra: str = "", pathStr: str = "") -> Tuple[List[float], str]: """Generate a set overlap finding experiment. Args: S: a Z3 solver instance nAels: number of elements in set A nBels: number of elements in set B (by aesthetic convention, ``|B|>=|A|``) tStrExtra: (optional) addendum to title string (e.g. "opt") pathStr: (optional) path for the plot file to be generated Returns: Since quite likely one might wish to try alternative visualizations, the computationally \ expensive part of the experiment (producing the times it takes to render individual solutions \ and the summary Z3 solver statistics) is returned. """ # input data for two sets setBname = 'setB' elsBnames = ['b%s' % i for i in range(1, nBels + 1)] setAname = 'setA' elsAnames = ['a%s' % i for i in range(1, nAels + 1)] # test run: cTs, statsStr = genOverlaps(setBname, elsBnames, setAname, elsAnames, S) # render a plot (as PDF and as SVG) from the experimental data: if tStrExtra == "": extraStr = "" extraFNstr = "" else: extraStr = '(%s) ' % tStrExtra extraFNstr = '-(%s)' % tStrExtra tStr = 'Experiment %sfor |A| = %s and |B| = %s (total time: %ss)' % \ (extraStr, nAels, nBels, numpy.round(sum(cTs), 8)) fN = pathStr+('overlaps%s_nA=%s_nB=%s' % (extraFNstr, nAels, nBels)) logging.info('Filename:\t%s' % fN) genExecTimePlot(cTs, statsStr, tStr, fN) return cTs, statsStr
[docs]def genSetOverlapExperimentV2(S: z3.Solver, nAels: int, nBels: int, tStrExtra: str = "", pathStr: str = "") -> Tuple[List[float], str]: """Generate a set overlap finding experiment. Args: S: a Z3 solver instance nAels: number of elements in set A nBels: number of elements in set B (by aesthetic convention, ``|B|>=|A|``) tStrExtra: (optional) addendum to title string (e.g. "opt") pathStr: (optional) path for the plot file to be generated Returns: Since quite likely one might wish to try alternative visualizations, the computationally \ expensive part of the experiment (producing the times it takes to render individual solutions \ and the summary Z3 solver statistics) is returned. """ # input data for two sets setBname = 'setB' elsBnames = ['b%s' % i for i in range(1, nBels + 1)] setAname = 'setA' elsAnames = ['a%s' % i for i in range(1, nAels + 1)] # test run: cTs, statsStr = genOverlapsV2(setBname, elsBnames, setAname, elsAnames, S) # render a plot (as PDF and as SVG) from the experimental data: if tStrExtra == "": extraStr = "(V2)" extraFNstr = "-(V2)" else: extraStr = '(V2-%s) ' % tStrExtra extraFNstr = '-(V2-%s)' % tStrExtra tStr = 'Experiment %sfor |A| = %s and |B| = %s (total time: %ss)' % \ (extraStr, nAels, nBels, numpy.round(sum(cTs), 8)) fN = pathStr + ('overlaps%s_nA=%s_nB=%s' % (extraFNstr, nAels, nBels)) genExecTimePlot(cTs, statsStr, tStr, fN) return cTs, statsStr
# %%
[docs]def numSetInjectivePartialOverlaps(m: int, n: int) -> int: """Function to compute the number of injective partial set overlaps. Given a set ``A`` of cardinality ``m`` and a set ``B`` of cardinality ``m+n``, the exact formula \ for the number of injective partial overlaps of the two sets is given by .. math:: n_{sols} = \\sum_{k=0}^m k! \\binom{m}{k}\\binom{m+n}{k} = (-1)^m U(-m, n+1, -1)\\,. Args: m: cardinality of the smaller set n: number of additional elements (possibly 0) in the larger set Returns: Number of injective partial overlaps. """ return int((-1)**m * mpmath.hyperu(-m, n+1, -1))
[docs]def render3DplotsOfInjPartialObverlaps(mMax: int, nMax: int, fName: str) -> None: """Render a 3D plot of the numbers of injective partial overlaps between to (finite) sets. Args: mMax: the maximum size of the smaller set (w.l.o.g.) nMax: the maximum additional size of the larger set (i.e. the maximum difference in sizes) fName: a filename (including a path if necessary) for storing the rendered PDF figure Returns: A 3D bar log-plot will be rendered and (depending on the capabilities of the current Python \ interface) both displayed and stored to a PDF file. """ # setup the figure and axes fig = plt.figure() ax = fig.add_subplot(projection='3d') # set up data for x and y axes: _x = numpy.arange(1, mMax+1) _y = numpy.arange(nMax) _xx, _yy = numpy.meshgrid(_x, _y) x, y = _xx.ravel(), _yy.ravel() top = [numpy.log10(numSetInjectivePartialOverlaps(x[i], y[i])) for i in range(len(x))] bottom = numpy.zeros_like(x) width = depth = 1 ax.bar3d(x, y, bottom, width, depth, top, shade=True, zsort='min') ax.set_title(r'Number of injective partial overlaps ($n_{sols}$)') # label the axes: ax.zscale = 'log' ax.set_xlabel('m') ax.set_ylabel('n') ax.set_zlabel(r'$log_{10}(n_{sols})$') ax.text(-1.4, -1.5, 12, r'\begin{align*}n_{sols}&=\sum_{k=0}^{m^{\vphantom{X}}}k!\binom{m}{k}\binom{m+n}{k}\\' r'm&=|\mathbf{A}|\,,\; n=|\mathbf{B}|-|\mathbf{A}|' r'\quad(|\mathbf{B}|\geq |\mathbf{A}|)\end{align*}', horizontalalignment='left', bbox=dict(fill=True, pad=0.6, alpha=1.0, facecolor='white', edgecolor='c', boxstyle='round')) plt.savefig('%s.pdf' % fName) plt.close() # crop teh whitespace from the PDF produced subprocess.run(['pdfcrop', '--margins', '\"10\"', '%s.pdf' % fName, '%s.pdf' % fName], capture_output=True) # render a SVG variant of the PDF (for viewing in Jupyter notebooks etc.): subprocess.run(['pdf2svg', '%s.pdf' % fName, '%s.svg' % fName], capture_output=True) # show the plot # plt.show() display(SVG('%s.svg' % fName))
# %%
[docs]def generateForbiddenRelations(elsNames: List[str]) -> \ Tuple[List[Dict[str, str]], List[Tuple[float, str]], str]: """Generate forbidden relations from forbidden set pattern. Candidate pushout decompositions are computed, and candidates are iteratively tested \ for isomorphisms against previously found solutions (in a "greedy" search). Then a list \ of "forbidden relations" encoded as a dictionary (see below) is returned. Args: elsNames: list of set element names Returns: The routine returns two pieces of data: * A list of dictionaries, where each dictionary encodes one forbidden relation. Entries of the dictionary have keys element names and values either '<', '>' or '=' (element only in left/right part/in both parts). * A list of execution times of the Z3 solver for each of the individual runs (marked by \ the type of the run, where 'fr' for finding a forbidden relation, 'iso' for an iso-check \ and 'unsat' for the final ``unsat`` run. * A string with the statistics summary of the Z3 solver instance used. """ S = z3.Solver() setN, elsN = z3.EnumSort('setN', tuple(['setN|nil'] + elsNames)) # the set pattern Nels = OrderedDict(zip(['setN|nil'] + elsNames, elsN)) # for convenience (to access constants by name) logging.info('Nels dictionary generated:\n%s' % pformat(Nels)) indA = z3.Function('indA', setN, z3.BoolSort()) # "template" for left "leg" of cospan predicate indB = z3.Function('indB', setN, z3.BoolSort()) # "template" for right "leg" of cospan predicate # assert that the nil-element of setN (i.e. elsN[0]) must be part of both subsets: astNilMapping = [indA(elsN[0]) == True, indB(elsN[0]) == True] # assert that both subsets must be proper subsets: z = z3.Const('z', setN) astProperSubset = [z3.Exists(z, indA(z) != True), z3.Exists(z, indB(z) != True)] # assert that the union of both subsets must yield setN: astUnion = [z3.ForAll(z, z3.Or(indA(z) == True, indB(z) == True))] S.add(astNilMapping + astProperSubset + astUnion) frList = [] # list that will store forbidden relations # auxiliary isomorphism function Phi (to discard duplicates up to isomorphism): Phi = z3.Function('Phi', setN, setN) x, y = z3.Consts('x y', setN) astsPhi = [z3.ForAll([x, y], z3.Implies(Phi(x) == Phi(y), x == y)), # injectivity z3.ForAll(y, z3.Exists(x, y == Phi(x)))] # surjectivity # set up a list of computation times: cTimes = [] # first run of the Z3 solver: # very first check for solutions: start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [(t, 'fr')] while chk == z3.sat: M = S.model() logging.info('Candidate model found:\n\tindA =\t%s\n\tindB =\t%s\n' % (pformat({k: M.eval(indA(Nels[k])) for k in Nels.keys()}), pformat({k: M.eval(indB(Nels[k])) for k in Nels.keys()}))) # determine whether the solution found is isomorphic to any of the previous ones: isNewFR = True for (indC, indD) in frList: logging.info('indC and indD read in from frList:\n\tindC =\t%s\n\tindD =\t%s\n' % (pformat(indC), pformat(indD))) S.push() astIso = [z3.And([z3.And(M.eval(indA(Phi(Nels[k]))) == indC[k], M.eval(indB(Phi(Nels[k]))) == indD[k]) for k in Nels.keys()] ) ] S.add(astsPhi + astIso) start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start cTimes += [(t, 'iso')] S.pop() if chk == z3.sat: isNewFR = False logging.info('\n|||\tThe current model is not describing a new relation ' + 'and is thus discarded!\t|||\n') break # terminate the comparison (i.e. this implements a "greedy" search strategy) # if the forbidden relation is indeed not isomorphic to any of the ones in frList, add it to frList: if isNewFR is True: logging.info('\n|||\tModel added to frList!\t|||\n') frList += [({k: M.eval(indA(Nels[k])) for k in Nels.keys()}, {k: M.eval(indB(Nels[k])) for k in Nels.keys()})] # "block" the present solution for indA and indB for the next solver run: astBlock = [z3.Exists(z, z3.Or(indA(z) != M.eval(indA(z)), indB(z) != M.eval(indB(z))))] S.add(astBlock) # next solver run: start = timeit.default_timer() chk = S.check() t = timeit.default_timer() - start if chk == z3.sat: cTimes += [(t, 'fr')] else: cTimes += [(t, 'unsat')] # "compile" each forbidden relation in frList into a "</=/> indicator format": frListAlt = [] for (aInd, bInd) in frList: frListAlt += [{k: ('=' if (aInd[k] and bInd[k]) else '<' if (aInd[k]) else '>') for k in Nels.keys()}] # reading out some statistics about the Z3 solver run: statsStr = S.statistics() logging.info('\n|||||\tSolver statistics summary:\t|||||\n%s' % pformat(statsStr)) S.reset() # clear out the local solver instance to save memory etc. logging.info('\n|||||\tDecompositions produced:\t|||||\n%s' % pformat(frListAlt)) return frListAlt, cTimes, statsStr
[docs]def genFrExecTimePlot(cTimes: List[Tuple[float, str]], statsInfo: str, titleStr: str, fName: str) -> None: """Generate execution time Log-bar plot with average time marked. Args: cTimes: list of computation times (with the last entry the time until ``unsat``) statsInfo: the Z3 solver statistics info str titleStr: string to be used for the title of the plot fName: filename Returns: Renders a bar Log-plot with a dotted horizontal line marking the average execution \ time, and with the last bar (highlighted in a different color) indicating the time \ until ``unsat``; the plot is saved into a PDF with filename ``fName``. """ # use the seaborn "dark" palette: rgbPalette = sns.color_palette("dark") # colors in rgb format, i.e. 3-tuples w/ entries <1 fig, ax = plt.subplots() fig.set_tight_layout(False) fig.subplots_adjust(right=0.75) # make bar plots for the individual sat computation timings: # the solver runs for finding forbidden relations: xPositions = [i for i, x in enumerate(cTimes) if x[1] == 'fr'] yVals = [x[0] for x in cTimes if x[1] == 'fr'] ax.bar(xPositions, yVals, align='center', color=rgbPalette[0], label='time until sat (fr runs)' ) # the solver runs for doing isomorphism checks: xPositions = [i for i, x in enumerate(cTimes) if x[1] == 'iso'] yVals = [x[0] for x in cTimes if x[1] == 'iso'] ax.bar(xPositions, yVals, align='center', color=rgbPalette[8], label='time until sat (iso runs)' ) # make individual bar for unsat time: ax.bar(len(cTimes), cTimes[-1][0], width=0.025*len(cTimes), color=rgbPalette[2], align='edge', label='unsat run: %ss' % numpy.round(cTimes[-1][0], 8) ) # plot an average execution time dotted line into the plot: cTimesVals = [x[0] for x in cTimes] avgCt = sum(cTimesVals) / len(cTimesVals) ax.axhline(y=avgCt, linewidth=1, linestyle=':', color='k', # color black label='avg. = %ss' % numpy.round(avgCt, 8) ) # label the axes: ax.set_yscale('log') ax.set_xlabel('computations') ax.set_ylabel('computation time (in s)') ax.set_title(titleStr) leg = ax.legend(bbox_to_anchor=(1.05, 1), loc=2, borderaxespad=0) # ax.legend(loc='best') fig.canvas.draw() # this draws the figure # which allows reading final coordinates in pixels leg_pxls = leg.get_window_extent() ax_pxls = ax.get_window_extent() fig_pxls = fig.get_window_extent() # Converting back to figure normalized coordinates to create new axis: pad = 0.025 ax2 = fig.add_axes([leg_pxls.x0 / fig_pxls.width, ax_pxls.y0 / fig_pxls.height, leg_pxls.width / fig_pxls.width, (leg_pxls.y0 - ax_pxls.y0) / fig_pxls.height - pad]) # eliminating all the tick marks: ax2.axis('off') # adding some statistics info from the Z3 solver run: ax2.text(0, 0, statsInfo, fontsize=4) # save plot to file: plt.savefig(fName + '.pdf', bbox_inches="tight") # plt.tight_layout() # plt.show() # Note: the variant below is optimized for IPython notebook/sphinx-gallery documentation output! plt.close() # crop teh whitespace from the PDF produced subprocess.run(['pdfcrop', '--margins', '\"10\"', '%s.pdf' % fName, '%s.pdf' % fName], capture_output=True) # render a SVG variant of the PDF (for viewing in Jupyter notebooks etc.): subprocess.run(['pdf2svg', '%s.pdf' % fName, '%s.svg' % fName], capture_output=True) # show the plot # plt.show() display(SVG('%s.svg' % fName))
# %%
[docs]def renderVisualization( frListInput: List[Dict[str, str]], workDir: str, plotFN: str, templateDir: str, plotLayout: str = '2:1') -> None: """Render the forbidden relations as a grid of graphics. Args: frListInput: a list of forbidden relations workDir: directory into which to put the rendered PDF files plotFN: name of the plot file (final tableaux presentation will be called ``plotFN+'-tableaux.pdf'``) templateDir: directory containing the LaTeX preamble and Jinja2 template files \ (default: ``os.getcwd()+'/jinja2-templates'``) plotLayout: (optional) choice of layout option (``'2:1'`` or ``'1:1'``; default: ``'2:1'``) Returns: Renders PDFs ``plotFN+'.pdf'`` and ``plotFN+'-tableaux.pdf`` with vizualizations of the \ forbidden relations (individual plots and tableaux of plots, respectively). The latter PDF \ will then be opened in the system's default PDF viewer. """ rgbPalette = sns.color_palette("dark") # colors in rgb format, i.e. 3-tuples w/ entries <1 RGBpalette = [(a * 256, b * 256, c * 256) for a, b, c in rgbPalette] # entries rescaled va *256 # create a jinja2 environment with latex-compatible markup and instantiate a template env = make_env(loader=FileSystemLoader(templateDir)) # aesthetical and other parameters for the individual plots: tplChild = env.get_template('nt-child.latex') childParams = {'layer_distance': '-3.5', 'setupXAngle': '-10', 'setupYAngle': '-10', 'setupXLength': '1', 'setupYLength': '1' } # for aesthetical purposes, sort the forbidden relations by number of '=' in increasing order frListSorted = sorted(frListInput, key=lambda fR: len([el for el, val in fR.items() if val == '='])) # the main figure generation loop: all info will be stored in the tikzFigures string tikzFigures = '' for k in range(len(frListSorted)): # ignore nil-element! frLst = {key: val for key, val in frListSorted[k].items() if '|nil' not in key} # step 1: initialize a graph with all nodes in order to generate the layout: G = nx.Graph() G.add_nodes_from([key for key in frLst]) # Step 1a: render a layout of the graph via the spring layout method: # NOTE: we could of course use any other layout routine provided by networkx! pos = nx.fruchterman_reingold_layout(G) # some aesthetic fixes (to center all points within a square with some margins): xVals = [x for x, y in pos.values()] yVals = [y for x, y in pos.values()] planeXmin = min(xVals) planeXmax = max(xVals) planeYmin = min(yVals) planeYmax = max(yVals) planeLraw = max(planeXmax - planeXmin, planeYmax - planeYmin) planeOffSet = 0.5 * planeLraw # change to aesthetic values as desired! # Here are the parameters passed on to the template: planeL = planeLraw + 2 * planeOffSet planeXpos = planeXmin - planeOffSet planeYpos = planeYmin - planeOffSet # Step 1b: for some weird reason, the positions are stored as arrays, but we need tuples # instead for use with network2tikz: tPos = {key: tuple(val) for key, val in pos.items()} # Step 2: for the vertices of label '=', render a copy (for later use in layers): extraVkeys = [key for key, val in frLst.items() if val == '='] # for convenience: augment the varuous dictionaries by the extra vertices: G.add_nodes_from([key + 'L2' for key in extraVkeys]) tPosAugmented = {**tPos, **{key + 'L2': tPos[key] for key in extraVkeys}} frLstAugmented = {**frLst, **{key + 'L2': frLst[key] for key in extraVkeys}} # render a string containing the commands for the vertex drawing on the bottom layer: vBottom = '' bottomLayerVkeys = [key for key in G.nodes if 'L2' in key or frLstAugmented[key] == '>'] for key in bottomLayerVkeys: xCoord, yCoord = tPosAugmented[key][0:2] vBottom += '\\Vertex[x=%s,y=%s,layer=2, style={vLayerTwo}]{%s}\n' % (xCoord, yCoord, key) # render a string containing the commands for the vertex drawing on the top layer: vTop = '' topLayerVkeys = [key for key in G.nodes if 'L2' not in key and frLstAugmented[key] != '>'] for key in topLayerVkeys: xCoord, yCoord = tPosAugmented[key][0:2] vTop += '\\Vertex[x=%s,y=%s,layer=1, style={vLayerOne}]{%s}\n' % (xCoord, yCoord, key) # render a string containing the commands for the edges linking vertices between the two layers: eLink = '' for key in extraVkeys: eLink += '\\Edge[lw=0.5,color=black,style=dashed](%s)(%s)\n' % (key, key + 'L2') # assemble all of the data into the parameter dictionary for the template: plotParams = {**childParams, **{'verticesBottomLayer': vBottom, 'verticesTopLayer': vTop, 'edgesLinkLayers': eLink, 'planeL': planeL, 'planeX': planeXpos, 'planeY': planeYpos} } # render the tikz info: tikzFigures += '\n\n' + tplChild.render(plotParams) + '\n\n' # aesthetical and other parameters for the main file: tplMain = env.get_template('nt-parent.latex') mainParams = { 'colorsVLayerOne': str(RGBpalette[0])[1:-1], 'colorsVLayerTwo': str(RGBpalette[1])[1:-1], 'TiKZpictures': tikzFigures } mainPlotsFile = tplMain.render(mainParams) with open('%s.tex' % (workDir + plotFN), 'w') as output: output.write(mainPlotsFile) # build_pdf's source parameter can be a file-like object or a string pdf = build_pdf(mainPlotsFile, texinputs=[templateDir, '']) pdf.save_to('%s.pdf' % (workDir + plotFN)) # assemble everything into a nice tableau of results: tplTableau = env.get_template('tableauTemplate.latex') # automatic layouts (change to your aesthetic preferences!): if plotLayout == '2:1': # 2:1 layout (i.e. two times more columns than rows): x = int(numpy.ceil(numpy.sqrt(len(frListInput)/2))) NupFormatStr = '%(w)sx%(h)s' % {'w': str(2 * x), 'h': str(x)} elif plotLayout == '1:1': # square layout: Ntiles = int(numpy.ceil(numpy.sqrt(len(frListInput)))) NupFormatStr = '%(s)sx%(s)s' % {'s': str(Ntiles)} tableauVar = {'fName': (workDir + plotFN), 'nup': NupFormatStr } # build_pdf's source parameter can be a file-like object or a string pdf = build_pdf(tplTableau.render(tableauVar), texinputs=[templateDir, '']) tableauxFn = '%s-tableaux.pdf' % (workDir + plotFN) pdf.save_to(tableauxFn) # crop teh whitespace from the PDF produced subprocess.run(['pdfcrop', '--margins', '\"10\"', tableauxFn, tableauxFn], capture_output=True) # render a SVG variant of the PDF (for viewing in Jupyter notebooks etc.): tableauxSVGfn = '%s-tableaux.svg' % (workDir + plotFN) subprocess.run(['pdf2svg', tableauxFn, tableauxSVGfn], capture_output=True) # open the figure in the standard PDF viewer: # subprocess.Popen("open '%s'" % tableauxFn, shell=True) # optimized for IPython/Jupyter notebooks: vie SVG inline: display(SVG(tableauxSVGfn))