Typed directed graphs

Preliminaries: setting up the Jupyter environment

If you have not already done so, please consult the Installation instructions chapter of the ReSMT documentation for information on how to install the necessary Python version, Python packages and the necessary additional shell scripts. You will also require a local copy of the ReSMT GitLab repository, which may be obtained as follows:

$ git clone https://gitlab.com/nicolasbehr/ReSMT.git <path-to-your-local-folder>

A convenient method to experiment with this document consists in starting up a Jupyter Lab instance: navigate to the docs/py_and_ipynb_examples folder of your local copy of the repository in a terminal session and execute the command

$ jupyter lab TypedDirectedGraphs-experiments.ipynb

This will open an interactive Jupyter session of the present notebook.

Assuming that the current working directory of the Python instance is the aforementioned docs/py_and_ipynb_examples sub-directory of the ReSMT package main directory, the package is loaded as follows:

import os
import timeit
import sys
sys.path.insert(0, os.path.abspath('../../'))
import resmt.datatypes as datatypes
import resmt.experiments as experiments
import resmt.visualizations as visualizations

import numpy
import networkx as nx
import z3

Note

If running the Python file from within an IDE such as e.g. PyCharm, it is alternatively possible to change the working directory to the docs/py_and_ipynb_examples folder manually before running the above code within the IDE, as in

$ os.chdir('/local/path/to/ReSMT/docs/py_and_ipynb_examples')

Overview of datatype design principles and first examples

The design philosophy of ReSMT consists in attempting a direct translation of the mathematical concepts developed in categorical rewriting theories into first order logic formulas amenable to be further analysed via an SMT solver or theorem prover. As such, every datatype in this library serves the dual purpose of faithfully encoding the category-theoretical datatypes as well as the encoding of the data into logical formulas. We exemplify this concept with two of the base datatypes. i.e. the classes Z3TypedSet of typed sets and Z3TypedFunction for functions of typed sets. Let us first set up some instances of these classes, highlighting in particular the special cases of empty sets and functions thereof. Note that all constructions require a Z3 solver instance, which may be set up as follows:

S = z3.Solver()

Typed sets

emptySet = datatypes.Z3TypedSet(S, 'emptySet', {})

It is important to note that an empty set for technical reasons still must contain a nil-element, and that (since all sets for this module must be typed) this nil-element is assigned a default type '_DEFAULT':

print(emptySet.els)             # returns {}, as the set has no elements
print(emptySet.sorts)           # the only sort is '_DEFAULT'
print(emptySet.nilEls)          # the sort '_DEFAULT' is inhabited by only the nil-element of that sort

We next consider an example of a non-empty typed set:

setA = datatypes.Z3TypedSet(S, 'setA', {'a':'elSort1', 'b':'elSort1', 'c':'elSort2'})

The following examples illustrate our datatypes API, demonstrating how the dictionary of elements with names as keys and sorts as values, the set of element sorts, the dictionary of nil-elements accessed by sorts as keys, and finally the direct access to elements by their names are accessible:

print(setA.els)             # element name:sort dictionary
print(setA.sorts)           # set of sorts in the set
print(setA.getEl('a'))      # retrieves the Z3 constant assigned to the element

A more subtle point of our implementation concerns the concrete encoding of the finite typed sets in terms of the Z3 API. Technically, a finite set is encoded as a z3.EnumSort, which entails in practice that for each subset of elements of a given sort, one such enumeration sort is instantiated, and for each of the elements plus for the nil-element of the sort, a special Z3 constant is instantiated as part of the z3.EnumSort instantiation. In effect, the Z3 enumeration sort permits to instantiate a Z3 constant (of that sort) that faithfully encodes the concept of “an element in the finite subset of the given sort”, which is a key concept in many of the algorithms of ReSMT. For this reason, this important notion of “one enumeration sort per element sort” is made accessible via the .subsets[srt] field of a Z3TypedSet instance, which stores the aforementioned instantiation of the enumeration sort, while the field .subsetEls[srt] stores all of the Z3 constants representing the elements of the finite subset of sort srt:

print(setA.subsets)                     # renders a dictionary with all enumeration sorts (by sort name)
print(setA.subsetEls['elSort1'])        # the Z3 constants [nil|elSort1, a, b] "inhabiting" the first sort
print(setA.subsetEls['elSort2'])        # the Z3 constants [nil|elSort2, c] "inhabiting" the second sort

Functions of typed sets

Given two typed sets setA and setB, a function between these two typed sets is effectively a collection of functions between the subsets induced by sorts of elements. For technical reasons, we currently only support one codomain sort per domain sort, i.e. we do not allow sort-signatures where elements of a given domain sort are mapped by the functions to codomain elements of more than one sort. Another fine-detail concerns the totality of functions: if a non-total function is specified, this is typically used to set up a “template” of a typed function, such as in cases where a given algorithm should construct a function via the Z3 methods. The nature of the function being initialized as non-total is also documented in the log file for the module. Let us first consider an example of a total typed function:

setD = datatypes.Z3TypedSet(S, 'domSet', {'a1': 'sortX', 'a2': 'sortX', 'a3': 'sortY'})
setC = datatypes.Z3TypedSet(S, 'codomSet', {'b1': 'sortX', 'b2': 'sortX', 'b3': 'sortY', 'b4': 'sortZ'})
f = datatypes.Z3TypedFunction(S,'f', setD, setC, {'a1': 'b2', 'a2': 'b1', 'a3': 'b4'}, isInjective = True)

The sort maps of f are accessible via the field f.srtMaps:

print(f.srtMaps)

Subfunctions are stored in the field .subFunctions as a dictionary with keys the sort names and values the Z3 function instances for the subfunctions:

print(f.subFunctions)

Most importantly, the instantiation of a Z3TypedFunction has the side-effect of uploading logical assertions to the chosen Z3 solver instance that encode the properties of the typed function, such as in particular the consistent sort-wise mapping of nil-elements, the injectivity or surjectivity (if specified) and any concrete mapping that was specified in the fData part of the input data. This information may also be accessed directly via the .asts field:

for ast in f.asts:
    print(ast)

As a special case, consider below as another example a function of empty sets:

emptySet = datatypes.Z3TypedSet(S, 'emptySet', {})
g = datatypes.Z3TypedFunction(S,'g', emptySet, emptySet, {})

One may verify that indeed the carrier sets are just the nil-elements of '_DEFAULT' sort, and that the assertions made are purely the nil-element mappings:

print(g.domSet.els)
print(g.domSet.nilEls)
print(g.codomSet.els)
print(g.codomSet.nilEls)
for ast in g.asts:
    print(ast)

Predicates over typed sets

For several of our algorithms, we need to define predicates over typed sets. The first kind of predicate is a simple Boolean predicate, which internally is implemented as a collection of Boolean predicates (one for each subset induced by element sorts). Note that this type of object inherits the Z3 solver instance from its domain set upon instantiation! Note also that strictly speaking the instantiation given below does not fully specify a Boolean predicate beyond some elementary consistency assertions (asserting that the nil-elements are always carrying the predicate True), since in the use cases present in ReSMT the predicates will be further refinedd as part of certain Z3-based search algorithms. As a somewhat counter-intuitive consequence, an instance of such a predicate is not “functional” per se, in that only upon rendering a model for the assertions that encode the predicate can one evaluate it in the form of this model on concrete elements.

setD = datatypes.Z3TypedSet(S, 'domSet', {'a1': 'sortX', 'a2': 'sortX', 'a3': 'sortY'})
predD = datatypes.Z3TypedSetPredicate('predD', setD)

for ast in predD.asts:
    print(ast)

The second type of predicate implemented in ReSMT is that of a typed span predicates, or, more precisely, templates thereof. The idea of this construction is that these predicates encode partial overlaps of typed sets, and that the ternary predicate functions encode which elements are in “partial overlap” via the span.

setA = datatypes.Z3TypedSet(S, 'setA', {'a1':'sortX', 'a2':'sortX', 'a3': 'sortY'})
setB = datatypes.Z3TypedSet(S, 'setB', {'b1':'sortX', 'b2':'sortX', 'b3': 'sortY', 'b4':'sortZ'})

Note that one must ensure that both sets have the exact same sort content, which may be achieved via “patching” suitable nil-elements if necessary as follows:

setA.patchNilElements(setB)
setB.patchNilElements(setA)

spanPredAB = datatypes.Z3TypedSetSpanPredicateTemplate('predAB', setA, setB, isMonic=True)

Postponing an in-detail discussion of this concept to a later point (i.e. when discussing the TDG overlap finding routines), suffice it here to illustrate the assertions instantiated for a typed set span predicate template, which encode consistent nil-element mapping as well as “bi-injectivity” in case of monic span predicates:

for ast in spanPredAB.asts:
    print(ast)

Finally, we will need a form of template for automorphisms of typed sets, which again will serve in later algorithms to search for such automorphisms via Z3 (rather than specifying such automorphisms manually).

setD = datatypes.Z3TypedSet(S, 'domSet', {'a1': 'sortX', 'a2': 'sortX', 'a3': 'sortY'})  # the domain set
autD = datatypes.Z3TypedSetAutomorphismTemplate('autD', setD)        # the automorphism template

print('\n Assertions encoding the automorphism property:\n')
for ast in autD.asts:
    print(ast)

Introducing typed directed graphs

A typed directed graph (TDG) is the following collection of data:

  1. A set of vertices V and a set of edges E.

  2. Source and target functions s,t: E\rightarrow V.

  3. Typing functions \tau_V:V\rightarrow T_V and \tau_E:E\rightarrow T_E.

Note: For technical reasons, at the moment we have not yet implemented the most general possible form of typing as described above, but only a variant where a given edge type is equipped with a fixed type-signature, i.e. all edges of a given type have a particular source- and target-type. This feature may be changed in a future version of the code. Concretely, this entails the following statement:

\forall e\in E: \tau_E(e) &= t_e\,,\; \tau_V(s(e))= t_{s(e)}\,. \; \tau_V(t(e)) = t_{t(e)}\\
\Rightarrow \quad \forall e'\in E:\tau_E(e')&=t_e: \tau_V(s(e'))=t_{s(e)} \land \tau_V(t(e'))=t_{t(e)}\,.

Let us first experiment with the API provided in the datatypes.py in order to set up a typed directed graph, en passent also illustrating the data format for entering TDGs. We first demonstrate how to set up an empty TDG.

Gempty = datatypes.Z3TypedDirectedGraph(S, 'gEmpty', {}, {}, {})

As expected, this graph only contains nil-elements of the '_DEFAULT' sort for the vertex and for the edge carrier sets, and just an assertion that the nil-edge has the nil-vertex as both its source and target:

print(Gempty.vertices.els)
print(Gempty.vertices.nilEls)
print(Gempty.edges.els)
print(Gempty.edges.nilEls)

print(Gempty.src.asts)
print(Gempty.trgt.asts)

Next, let us instantiate a non-empty typed directed graph:

vDictA = {'v1': 'sortX', 'v2': 'sortX', 'v3': 'sortY'}                       # the vertex carrier set
eDictA = {'e1': 'sortW', 'e2': 'sortT'}                                      # the edge carrier set
stDictA = {'e1': ('v1', 'v2'), 'e2': ('v3', 'v1')}                              # source/target incidence data
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

Here is an overview of how this data is encoded:

print('\n Vertex carrier set:\n')
print(graphA.vertices.els)
print(graphA.vertices.nilEls)
print('\n Edge carrier set:\n')
print(graphA.edges.els)
print(graphA.edges.nilEls)
print('\n Source function assertions:\n')
for ast in graphA.src.asts:
    print(ast)
print('\n Target function assertions:\n')
for ast in graphA.trgt.asts:
    print(ast)

Methods for visualization of TDGs are provided in the visualizations sub-module of ReSMT. The following code will both render a visualization of the TDG graphA from the above example and also save the plot to an SVG gile:

vis = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='graphA.svg',
                                    gLayout='neato')

visualizations.displaySVGtable({'graphA': ['images/graphA.svg']}, width="100%")

For certain operations such as determining whether two typed directed graphs can be isomorphic, it is important to verify first that the two TDGs are sort compatible, in the sense that their underlying vertex and edge carrier sets have the same sorts, and that the source/target maps have the same sort-signatures in both graphs. Compared to a full isomorphism check, this operation merely checks for sort compatibility, which is in particular only a look-up operation on the Python-parts of the data, and thus very efficient as compared to a more in-depth comparison opeeration. Let us define another TDG, and then compare a number of TDGs to each other:

vDictB = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortZ', 'v4': 'sortZ'}        # the vertex carrier set
eDictB = {'e1':'sortW', 'e2': 'sortT'}                                      # the edge carrier set
stDictB = {'e1':('v1','v2'), 'e2':('v3','v1')}                              # source/target incidence data
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

print('\ngraphA is sort-compatible with Gempty:\t %s' % graphA.isSortCompatibleWith(Gempty))    # returns False, as the sorts do not match of course
print('\ngraphA is sort-compatible with graphA:\t %s' % graphA.isSortCompatibleWith(graphA))    # returns True
print('\ngraphB is sort-compatible with graphA:\t %s' %graphB.isSortCompatibleWith(graphA))     # returns False

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='graphB.svg',
                                    gLayout='neato')

visualizations.displaySVGtable({'graphB': ['images/graphB.svg']}, width="100%")

(Templates of) boolean predicates over TDGs

Just as for typed sets, we will need to construct boolean predicates over TDGs, where again only certain sets of assertions made for consistency are instantiated (such as the consistent mapping of nil-elements etc.), while the main structure of the predicate is to be instantiated in search algorithms via Z3. Suffice it here to provide a concrete coding example for such a predicate, illustrating in particular the set of assertions rendered:

vDictA = {'v1': 'sortX', 'v2': 'sortX', 'v3': 'sortY'}
eDictA = {'e1': 'sortW', 'e2': 'sortT'}
stDictA = {'e1': ('v1', 'v2'), 'e2': ('v3', 'v1')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)
predGraphA = datatypes.Z3TDGpredicate('predGraphA', graphA)

for ast in predGraphA.asts:
    print(ast)

(Templates of) boolean span predicates over TDGs

In our main algorithms for searching for overlaps between typed directed graphs, we need to be able to set up templates for (monic) boolean span predicates over TDGs. Each such predicate consists of a collection of bi-variate functions (one per sort of vertices and of edges), which encodes the membership of the elements in its first and second arguments as a True or False boolean value. We present here a concrete example of such a TDG boolean span predicate instance, and also highight the assertions rendered at its instantiation:

S = z3.Solver()

# Definition of first TDG:
vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY', 'v4': 'sortZ'}
eDictA = {'e1':'sortW', 'e2': 'sortT'}
stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

# Definition of second TDG:
vDictB = {'v1': 'sortX', 'v2': 'sortX', 'v3': 'sortX', 'v4': 'sortY'}
eDictB = {'e1': 'sortW', 'e2': 'sortT', 'e3': 'sortT'}
stDictB = {'e1': ('v2', 'v1'), 'e2': ('v4', 'v3'), 'e3': ('v4', 'v1')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

# Patching of nil-elements in order to render the sorts of the TDGs compatible:
graphA.patchNilElements(graphB)
graphB.patchNilElements(graphA)

# Instantiate the boolean span predicate:
spanPredAB = datatypes.Z3TDGspanPredicateTemplate('spanPredAB', graphA, graphB)

The structure of the boolean span predicate (template) is best understood via the set of assertions that encode it:

for ast in spanPredAB.asts:
    print(ast)

Finding forbidden TDG relations

A core computational tool for the static analysis of rewriting systems over typed directed graphs that are restricted to not contain certain “forbidden patterns” is the notion of “forbidden relations”. We introduced this novel approach in our GCM 2020 workshop contribution “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping” (which contains also the full theoretical derivation of the relevant concepts). Intuitively, given a “forbidden pattern” N (which is itself some typed directed multigraph), the computation of the set of all “forbidden relations” may be performed as follows:

  1. Determine those monic spans of subgraphs (A \hookleftarrow M \hookrightarrow B) such that

    1. none of the three subgraphs of N contans N as a subgraph themselves, and

    2. the pushout (“the gluing of A with B along overlap M”) is isomorphic to N.

  2. Only retain one representative per isomorphism class of “forbidden relations”, where the relevant isomorphisms are those induced by automorphisms of N.

Reference: N. Behr, M. Ghaffari Saadat and R. Heckel, “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping” (contained in the pre-proceedings of the GCM 2020: Eleventh International Workshop on Graph Computation Models)

Let us first set up a “forbidden pattern”, e.g. as a first simple example a “star graph” with a number nLegs of outwards-pointing edges (with all vertices and edges of the same type):

Case nLegs = 2:

nLegs = 2

# Definition of a "forbidden" TDG pattern:

S = z3.Solver()

vDictN = {'v'+str(i): 'sortX' for i in range(nLegs + 1)}
eDictN = {'e'+str(i): 'sortX' for i in range(1, nLegs + 1)}
stDictN = {'e'+str(i): ('v0', 'v'+str(i)) for i in range(1, nLegs + 1)}
graphN = datatypes.Z3TypedDirectedGraph(S, 'gN', vDictN, eDictN, stDictN)

vis = visualizations.nxTypedDirectedGraph(graphN,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/graphN-nLegs=%s.svg' % nLegs,
                                    gLayout='neato')

visualizations.displaySVGtable(
    {('graphN-nLegs=%s' % nLegs): [('images/graphN-nLegs=%s.svg' % nLegs)]},
    width="100%")

Running the forbidden relation search itself:

FRs, execTimes, solverStats = datatypes.genForbiddenTDGrelations(graphN)

The routine detected the following forbidden relations:

for fr in FRs:
    print(fr)

The execution times of the Z3 solver for each run (until the last unsat run) are plotted below:

totalTime = numpy.round(sum([x[0] for x in execTimes]), 8)
titleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \
           + 'for nLegs = %s (total time: %ss)' % (nLegs, totalTime)
fN = 'images/fr-nLegs=%s-Z3-timings' % nLegs
statStr = str(solverStats)[1:-1]
experiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)
../_images/graphN-nLegs=2.svg../_images/fr-nLegs=2-Z3-timings.svg

Case nLegs = 3:

nLegs = 3

# Definition of a "forbidden" TDG pattern:

S = z3.Solver()

vDictN = {'v'+str(i): 'sortX' for i in range(nLegs + 1)}
eDictN = {'e'+str(i): 'sortX' for i in range(1, nLegs + 1)}
stDictN = {'e'+str(i): ('v0', 'v'+str(i)) for i in range(1, nLegs + 1)}
graphN = datatypes.Z3TypedDirectedGraph(S, 'gN', vDictN, eDictN, stDictN)

vis = visualizations.nxTypedDirectedGraph(graphN,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/graphN-nLegs=%s.svg' % nLegs,
                                    gLayout='neato')

visualizations.displaySVGtable(
    {('graphN-nLegs=%s' % nLegs): [('images/graphN-nLegs=%s.svg' % nLegs)]},
    width="100%")

Running the forbidden relation search itself:

FRs, execTimes, solverStats = datatypes.genForbiddenTDGrelations(graphN)

The routine detected the following forbidden relations:

for fr in FRs:
    print(fr)

The execution times of the Z3 solver for each run (until the last unsat run) are plotted below:

totalTime = numpy.round(sum([x[0] for x in execTimes]), 8)
titleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \
           + 'for nLegs = %s (total time: %ss)' % (nLegs, totalTime)
fN = 'images/fr-nLegs=%s-Z3-timings' % nLegs
statStr = str(solverStats)[1:-1]
experiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)
../_images/graphN-nLegs=3.svg../_images/fr-nLegs=3-Z3-timings.svg

Case nLegs = 4:

nLegs = 4

# Definition of a "forbidden" TDG pattern:

S = z3.Solver()

vDictN = {'v'+str(i): 'sortX' for i in range(nLegs + 1)}
eDictN = {'e'+str(i): 'sortX' for i in range(1, nLegs + 1)}
stDictN = {'e'+str(i): ('v0', 'v'+str(i)) for i in range(1, nLegs + 1)}
graphN = datatypes.Z3TypedDirectedGraph(S, 'gN', vDictN, eDictN, stDictN)

vis = visualizations.nxTypedDirectedGraph(graphN,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/graphN-nLegs=%s.svg' % nLegs,
                                    gLayout='neato')

visualizations.displaySVGtable(
    {('graphN-nLegs=%s' % nLegs): [('images/graphN-nLegs=%s.svg' % nLegs)]},
    width="100%")

Running the forbidden relation search itself:

FRs, execTimes, solverStats = datatypes.genForbiddenTDGrelations(graphN)

The routine detected the following forbidden relations:

for fr in FRs:
    print(fr)

The execution times of the Z3 solver for each run (until the last unsat run) are plotted below:

totalTime = numpy.round(sum([x[0] for x in execTimes]), 8)
titleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \
           + 'for nLegs = %s (total time: %ss)' % (nLegs, totalTime)
fN = 'images/fr-nLegs=%s-Z3-timings' % nLegs
statStr = str(solverStats)[1:-1]
experiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)
../_images/graphN-nLegs=4.svg../_images/fr-nLegs=4-Z3-timings.svg

Overlaps of typed graphs modulo forbidden relations

One of the core functionalities of this package in view of analyzing rewriting systems consists in finding all possible overlaps of two typed graphs (which will be the input and output graphs of two rewriting rules) module a given set of forbidden relations. As it is typically computationally expensive to (statically) render the forbidden relations, the typical workflow would amount to first rendering the forbidden relations for the given type of graphs, store these into some string data files, and only then render the possible overlaps. We will exemplify the procedure via the case of so-called rigid graphs, i.e. a variant of directed simple (loopless) graphs obtained via forbidding the following three patterns:

# Definition of the four "forbidden" TDG patterns:

Saux = z3.Solver()

vDictN1 = {'v'+str(i): 'sortX' for i in range(3)}
eDictN1 = {'e'+str(i): 'sortX' for i in range(1, 3)}
stDictN1 = {'e'+str(i): ('v0', 'v'+str(i)) for i in range(1, 3)}
graphN1 = datatypes.Z3TypedDirectedGraph(Saux, 'gN1', vDictN1, eDictN1, stDictN1)

visN1 = visualizations.nxTypedDirectedGraph(graphN1,
                                            drawGraph=True,
                                            writeGraph=True,
                                            fileName='images/graphN1.svg',
                                            gLayout='neato')

vDictN2 = {'v'+str(i): 'sortX' for i in range(3)}
eDictN2 = {'e'+str(i): 'sortX' for i in range(1, 3)}
stDictN2 = {'e'+str(i): ('v'+str(i), 'v0') for i in range(1, 3)}
graphN2 = datatypes.Z3TypedDirectedGraph(Saux, 'gN2', vDictN2, eDictN2, stDictN2)

visN2 = visualizations.nxTypedDirectedGraph(graphN2,
                                            drawGraph=True,
                                            writeGraph=True,
                                            fileName='images/graphN2.svg',
                                            gLayout='neato')

vDictN3 = {'v1': 'sortX', 'v2': 'sortX'}
eDictN3 = {'e1': 'sortX', 'e2': 'sortX'}
stDictN3 = {'e1': ('v1', 'v2'), 'e2': ('v1', 'v2')}
graphN3 = datatypes.Z3TypedDirectedGraph(Saux, 'gN3', vDictN3, eDictN3, stDictN3)

visN3 = visualizations.nxTypedDirectedGraph(graphN3,
                                            drawGraph=True,
                                            writeGraph=True,
                                            fileName='images/graphN3.svg',
                                            gLayout='neato')

vDictN4 = {'v1': 'sortX'}
eDictN4 = {'e1': 'sortX', 'e2': 'sortX'}
stDictN4 = {'e1': ('v1', 'v1'), 'e2': ('v1', 'v1')}
graphN4 = datatypes.Z3TypedDirectedGraph(Saux, 'gN4', vDictN4, eDictN4, stDictN4)

visN4 = visualizations.nxTypedDirectedGraph(graphN4,
                                            drawGraph=True,
                                            writeGraph=True,
                                            fileName='images/graphN4.svg',
                                            gLayout='neato')


# display the forbidden graph patterns:
visualizations.displaySVGtable({
    'gN1': ['images/graphN1.svg'],
    'gN2': ['images/graphN2.svg'],
    'gN3': ['images/graphN3.svg'],
    'gN4': ['images/graphN4.svg'],
}, width="100%")

Next, we generate all the forbidden relation data from the forbidden patterns:

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

S = z3.Solver()

frsN1 = datatypes.Z3TDGfrContainer(S, graphN1)
frsN1.genTDGfrData()

frsN2 = datatypes.Z3TDGfrContainer(S, graphN2)
frsN2.genTDGfrData()

frsN3 = datatypes.Z3TDGfrContainer(S, graphN3)
frsN3.genTDGfrData()

frsN4 = datatypes.Z3TDGfrContainer(S, graphN4)
frsN4.genTDGfrData()

frLists = [frsN1.frData, frsN2.frData, frsN3.frData, frsN4.frData]

for n in range(4):
    print("\nForbidden relation data from pattern N%s:\n" % (n+1))
    for fr in frLists[n]:
        print("\t--|\t %s\n" % fr)

Let us set up two TDGs between which we wish to find all possible monic overlaps whose pushouts do not violate the forbidden patterns. We start with a small example for illustration, and will later scale the example up in order to access the performance of our overlap-finding algorithm.

vDictA = {'vA1': 'sortX', 'vA2': 'sortX'}
eDictA = {'eA1': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                           drawGraph=True,
                                           writeGraph=True,
                                           fileName='images/gA.svg',
                                           gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX'}
eDictB = {'eB1': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                           drawGraph=True,
                                           writeGraph=True,
                                           fileName='images/gB.svg',
                                           gLayout='neato')

# Patching of nil-elements in order to render the sorts of the TDGs compatible:
# (not strictly necessary here of course, since the sorts already match)
graphA.patchNilElements(graphB)
graphB.patchNilElements(graphA)

# display the graphs:
visualizations.displaySVGtable({'gA': ['images/gA.svg'], 'gB': ['images/gB.svg']}, width="100%")

Before turning towards the overlap search routine itself, let us briefly illustrate some core aspects of the algorithm implementation, one of which consists of instantiating a span predicate template for the two graphs:

spAB = datatypes.Z3TDGspanPredicateTemplate('spAB', graphA, graphB)

Assertions present in the Z3 solver instance S up to this point:

print(S.assertions())

Next, we will need to render the assertions from each of the forbidden relation data containers, and add them to one large container block:

frsN1.genFRasts(spAB)
frsN2.genFRasts(spAB)
frsN3.genFRasts(spAB)
frsN4.genFRasts(spAB)

# example for assertions originating from forbidden pattern N1:
for ast in frsN1.asts:
    print(ast.sexpr())

# the full solver state after rendering the forbidden relations:
for ast in S.assertions():
    print(ast)

All requisite assertions are rendered now, comprising the Z3 representations of the input graphs and the forbidden relation non-DPE assertions. For illustration, we may now run the solver in order to obtain a first overlap solution:

S.check()
M = S.model()

print(M)

Let us now run the overlap search routine itself:

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1, frsN2, frsN3, frsN4]

# trigger the overlap searching routine with the DPE strategy:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out the overlaps found:
for o in overlaps:
    print(o)

# render a plot of the execution times:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for gA = gB = o->o (total computation time:\t%ss)' % round(sum(cTimes), 6)
fName = 'images/overlaps-Experiment1'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

To test for the scaling of the code complexity ad run times, we now consider a slightly larger example.

Note: We will en passent demonstrate how to re-use the statically computed forbidden relations data (albeit in the present example the cost for the computation of this data is rather moderate).

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

S = z3.Solver()   # the target Z3 sovler instance for all further computations

frsN1Reused = datatypes.Z3TDGfrContainer(S, graphN1, frsN1.frData)
frsN2Reused = datatypes.Z3TDGfrContainer(S, graphN2, frsN2.frData)
frsN3Reused = datatypes.Z3TDGfrContainer(S, graphN3, frsN3.frData)
frsN4Reused = datatypes.Z3TDGfrContainer(S, graphN4, frsN4.frData)

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1Reused, frsN2Reused,
           frsN3Reused, frsN4Reused]

for n in range(4):
    print("\nForbidden relation data from pattern N%s:\n" % (n+1))
    for fr in frClist[n].frData:
        print("\t--|\t %s\n" % fr)
vDictA = {'vA1': 'sortX', 'vA2': 'sortX', 'vA3': 'sortX'}
eDictA = {'eA1': 'sortX', 'eA2': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2'), 'eA2': ('vA2', 'vA3')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gA2.svg',
                                    gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX'}
eDictB = {'eB1': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gB.svg',
                                    gLayout='neato')

# display the graphs:
visualizations.displaySVGtable({'gA': ['images/gA.svg'], 'gB': ['images/gB.svg']}, width="100%")
# trigger the overlap searching routine with the DPE strategy:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out each overlap found:
for ol in overlaps:
    print(ol)

# render the execution time plot:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for gA = o->o->o, gB = o->o (total computation time:\t%ss)' % round(
    sum(cTimes), 6)
fName = 'images/overlaps-Experiment2'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

The polymer model examples presented at GCM 2020

Consider the following rewriting rules, for which only the “plain” rule parts are explicitly depicted, and which should be considered in the context of rewriting over rigid graphs (i.e. graphs respecting the constraints of not containing any of the “forbidden patterns” mentioned in the previous examples):

../_images/rGraphRules.svg

Based upon these rules, consider the following three overlap search examples, where we denote for a given linear rewriting rule r=(O\leftharpoonup I) by out(r):=O and in(r):=I the out- and input interfaces of the rule r, respectively:

  • Example P1: g_A = out(r_{create-edge}), g_B = in(r_{delete-edge})

  • Example P2: g_A = out(r_{c-c_2}), g_B = in(r_{b-c_2})

  • Example P3: g_A = out(r_{c-c_4}), g_B = in(r_{b-c_4})

  • Example P4: g_A = out(r_{c-c_7}), g_B = in(r_{b-c_7})

Example P1

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

S = z3.Solver()   # the target Z3 sovler instance for all further computations
# alternative (by far the best combination of tactics thus far, but uses much more memory):
# S = z3.Then('snf', 'aig', 'smt').solver()


frsN1Reused = datatypes.Z3TDGfrContainer(S, graphN1, frsN1.frData)
frsN2Reused = datatypes.Z3TDGfrContainer(S, graphN2, frsN2.frData)
frsN3Reused = datatypes.Z3TDGfrContainer(S, graphN3, frsN3.frData)
frsN4Reused = datatypes.Z3TDGfrContainer(S, graphN4, frsN4.frData)

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1Reused, frsN2Reused,
           frsN3Reused, frsN4Reused]

vDictA = {'vA1': 'sortX', 'vA2': 'sortX'}
eDictA = {'eA1': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gA-P1.svg',
                                    gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX'}
eDictB = {'eB1': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gB-P1.svg',
                                    gLayout='neato')

# display the graphs:
visualizations.displaySVGtable({'gA-P1': ['images/gA-P1.svg'], 'gB-P1': ['images/gB-P1.svg']}, width="100%")
# trigger the overlap searching routine:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out each overlap found:
for ol in overlaps:
    print(ol)

# render the execution time plot:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for example P1 (total computation time:\t%ss)' % round(sum(cTimes), 6)
fName = 'images/overlaps-Experiment-P1'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

Example P2

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

# the target Z3 sovler instance for all further computations
# S = z3.Solver()
# alternative (by far the best combination of tactics thus far, but uses much more memory):
S = z3.Then('snf', 'aig', 'smt').solver()

frsN1Reused = datatypes.Z3TDGfrContainer(S, graphN1, frsN1.frData)
frsN2Reused = datatypes.Z3TDGfrContainer(S, graphN2, frsN2.frData)
frsN3Reused = datatypes.Z3TDGfrContainer(S, graphN3, frsN3.frData)
frsN4Reused = datatypes.Z3TDGfrContainer(S, graphN4, frsN4.frData)

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1Reused, frsN2Reused,
           frsN3Reused, frsN4Reused]

vDictA = {'vA1': 'sortX', 'vA2': 'sortX', 'vA3': 'sortX'}
eDictA = {'eA1': 'sortX', 'eA2': 'sortX', 'eA3': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2'), 'eA2': ('vA2', 'vA3'), 'eA3': ('vA3', 'vA1')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gA-P2.svg',
                                    gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX', 'vB3': 'sortX'}
eDictB = {'eB1': 'sortX', 'eB2': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2'), 'eB2': ('vB2', 'vB3')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gB-P2.svg',
                                    gLayout='neato')

# display the graphs:
visualizations.displaySVGtable({'gA-P2': ['images/gA-P2.svg'], 'gB-P2': ['images/gB-P2.svg']}, width="100%")
# trigger the overlap searching routine:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out each overlap found:
for ol in overlaps:
    print(ol)

# render the execution time plot:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for example P2 (total computation time:\t%ss)' % round(sum(
    cTimes), 6)
fName = 'images/overlaps-Experiment-P2'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

Example P3

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

S = z3.Solver()   # the target Z3 sovler instance for all further computations

frsN1Reused = datatypes.Z3TDGfrContainer(S, graphN1, frsN1.frData)
frsN2Reused = datatypes.Z3TDGfrContainer(S, graphN2, frsN2.frData)
frsN3Reused = datatypes.Z3TDGfrContainer(S, graphN3, frsN3.frData)
frsN4Reused = datatypes.Z3TDGfrContainer(S, graphN4, frsN4.frData)

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1Reused, frsN2Reused,
           frsN3Reused, frsN4Reused]

vDictA = {'vA1': 'sortX', 'vA2': 'sortX', 'vA3': 'sortX', 'vA4': 'sortX', 'vA5': 'sortX'}
eDictA = {'eA1': 'sortX', 'eA2': 'sortX', 'eA3': 'sortX', 'eA4': 'sortX', 'eA5': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2'), 'eA2': ('vA2', 'vA3'), 'eA3': ('vA3', 'vA4'),
           'eA4': ('vA4', 'vA5'), 'eA5': ('vA5', 'vA1')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gA-P3.svg',
                                    gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX', 'vB3': 'sortX', 'vB4': 'sortX', 'vB5': 'sortX'}
eDictB = {'eB1': 'sortX', 'eB2': 'sortX', 'eB3': 'sortX', 'eB4': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2'), 'eB2': ('vB2', 'vB3'), 'eB3': ('vB3', 'vB4'), 'eB4': ('vB4', 'vB5')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gB-P3.svg',
                                    gLayout='neato')

# display the graphs:
visualizations.displaySVGtable({'gA-P3': ['images/gA-P3.svg'], 'gB-P3': ['images/gB-P3.svg']}, width="100%")
# trigger the overlap searching routine:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out each overlap found:
for ol in overlaps:
    print(ol)

# render the execution time plot:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for example P3 (total computation time:\t%ss)' % round(sum(cTimes), 6)
fName = 'images/overlaps-Experiment-P3'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

Example P4

# set up a "container object" for each of the three forbidden relations, and populate it via the
# forbidden relation data generation method:

S = z3.Solver()   # the target Z3 sovler instance for all further computations

frsN1Reused = datatypes.Z3TDGfrContainer(S, graphN1, frsN1.frData)
frsN2Reused = datatypes.Z3TDGfrContainer(S, graphN2, frsN2.frData)
frsN3Reused = datatypes.Z3TDGfrContainer(S, graphN3, frsN3.frData)
frsN4Reused = datatypes.Z3TDGfrContainer(S, graphN4, frsN4.frData)

# collect all pre-computed forbidden relation data containers into one list:
frClist = [frsN1Reused, frsN2Reused,
           frsN3Reused, frsN4Reused]

vDictA = {'vA1': 'sortX', 'vA2': 'sortX', 'vA3': 'sortX', 'vA4': 'sortX',
          'vA5': 'sortX', 'vA6': 'sortX', 'vA7': 'sortX', 'vA8': 'sortX'}
eDictA = {'eA1': 'sortX', 'eA2': 'sortX', 'eA3': 'sortX', 'eA4': 'sortX',
          'eA5': 'sortX', 'eA6': 'sortX', 'eA7': 'sortX', 'eA8': 'sortX'}
stDictA = {'eA1': ('vA1', 'vA2'), 'eA2': ('vA2', 'vA3'), 'eA3': ('vA3', 'vA4'), 'eA4': ('vA4', 'vA5'),
           'eA5': ('vA5', 'vA6'), 'eA6': ('vA6', 'vA7'), 'eA7': ('vA7', 'vA8'), 'eA8': ('vA8', 'vA1')}
graphA = datatypes.Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)

visA = visualizations.nxTypedDirectedGraph(graphA,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gA-P4.svg',
                                    gLayout='neato')

vDictB = {'vB1': 'sortX', 'vB2': 'sortX', 'vB3': 'sortX', 'vB4': 'sortX',
          'vB5': 'sortX', 'vB6': 'sortX', 'vB7': 'sortX', 'vB8': 'sortX'}
eDictB = {'eB1': 'sortX', 'eB2': 'sortX', 'eB3': 'sortX', 'eB4': 'sortX',
          'eB5': 'sortX', 'eB6': 'sortX', 'eB7': 'sortX'}
stDictB = {'eB1': ('vB1', 'vB2'), 'eB2': ('vB2', 'vB3'), 'eB3': ('vB3', 'vB4'), 'eB4': ('vB4', 'vB5'),
           'eB5': ('vB5', 'vB6'), 'eB6': ('vB6', 'vB7'), 'eB7': ('vB7', 'vB8')}
graphB = datatypes.Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)

visB = visualizations.nxTypedDirectedGraph(graphB,
                                    drawGraph=True,
                                    writeGraph=True,
                                    fileName='images/gB-P4.svg',
                                    gLayout='neato')

# display the graphs:
visualizations.displaySVGtable({'gA-P4': ['images/gA-P4.svg'], 'gB-P4': ['images/gB-P4.svg']}, width="100%")
# trigger the overlap searching routine:
experimentDPEstrategy = datatypes.generateTDGoverlapsDPEstrategy(graphA, graphB, frClist)
cTimes = experimentDPEstrategy.cTimes
statsStr = experimentDPEstrategy.statsStr
overlaps = experimentDPEstrategy.overlapsData.overlaps

# print out each overlap found:
for ol in overlaps:
    print(ol)

# render the execution time plot:
titleStr = 'Experiment (Python 3.8.2, Z3 4.8.8) for example P4 (total computation time:\t%ss)' % round(sum(cTimes), 6)
fName = 'images/overlaps-Experiment-P4'
experiments.genExecTimePlot(cTimes, statsStr, titleStr, fName)

Gallery generated by Sphinx-Gallery