API reference¶
datatypes.py¶
This module contains the core classes and methods for defining Z3 representations of datatypes for which rewriting is possible in ReSMT
(with typed directed graphs currently the main datatype implemented).

class
resmt.datatypes.
ExperimentSpec
(expName: str, graphDataFname: str, forbiddenPatternDataFname: str, strategyName: str, numReps: int, expsData: List[Tuple[str, str]], maxRunTime: int = 0)[source]¶ Bases:
object
“Auxiliary data class to collect parameters for experiments with the overlap finding methods.

__init__
(expName: str, graphDataFname: str, forbiddenPatternDataFname: str, strategyName: str, numReps: int, expsData: List[Tuple[str, str]], maxRunTime: int = 0) → None[source]¶ Initialize a specification of experimental data.
 Parameters
expName – a string containing the name of the experiment
graphDataFname – filename (possibly including a path) of a JSON file containing data defining TDGs
forbiddenPatternDataFname – filename (possibly including a path) of a JSON file containing data defining forbidden patterns (plus potentially also forbidden relation data)
strategyName – a string that evaluates to one of
'direct'
,'DPE'
,'implicit'
or'noConstraints'
(encoding the strategy to be utilized in the given subexperiment)numReps – an integer denoting the number of repetitions of the subexperiment
expsData – a list of tuples of the form
(gAname, gBname)
, withgAname
andgBname
the names of TDGs ingraphDataFname
whose overlaps should be computedmaxRunTime – (optional) an integer encoding a limit (in s) for the individual run times (default:
0
, encoding no limit on the run times)

storeExpsDataToJSONfile
(fName: str) → None[source]¶ Log the info of a given set of experiments to the file that will hold the results data.
The method logs all input data specifying the experiment to the JSON file identified via
resultsFname
, i.e. it adds to the keyexpName
a new field'expSpecs'
containing a dictionary containing all data necessary to specify the given experiment. Parameters
fName – the file name (possibly including a path) to a JSON file


class
resmt.datatypes.
Z3TDGautomorphismTemplate
(aName: str, domG: resmt.datatypes.Z3TypedDirectedGraph)[source]¶ Bases:
object
Automorphism template for
Z3TypedDirectedGraph
instances.

class
resmt.datatypes.
Z3TDGfrContainer
(solv: z3.z3.Solver, N: resmt.datatypes.Z3TypedDirectedGraph, frData: List[Dict[str, str]] = None)[source]¶ Bases:
object
An auxiliary class to render forbidden TDG relation data more accessible.

__init__
(solv: z3.z3.Solver, N: resmt.datatypes.Z3TypedDirectedGraph, frData: List[Dict[str, str]] = None) → None[source]¶ The container initialization.
Note
Since the search for forbidden TDG relations is computationally intensive, the container class initialization is designed such that the forbidden relation data may be specified directly (e.g. from stored data), or alternatively without the optional
frData
parameter. In the latter case, one may then in a second step trigger the class methodgenTDGfrData
to generate the forbidden relation data for the specified forbidden TDG patternN
.

genFRasts
(P: resmt.datatypes.Z3TDGspanPredicateTemplate) → None[source]¶ Method to render the nonDPE assertions generated from the forbidden TDG relations.


class
resmt.datatypes.
Z3TDGmorphism
(mName: str, domG: resmt.datatypes.Z3TypedDirectedGraph, codomG: resmt.datatypes.Z3TypedDirectedGraph, vMap: Dict[str, str], eMap: Dict[str, str], isInjective: bool = False, isSurjective: bool = False)[source]¶ Bases:
object
(Template of) a TDG homomorphism.
Note that if besides nilelement mappings no mapping data is provided during the initialization of an instance of this class, the instance in effect encodes a template of a TDG morphism.

__init__
(mName: str, domG: resmt.datatypes.Z3TypedDirectedGraph, codomG: resmt.datatypes.Z3TypedDirectedGraph, vMap: Dict[str, str], eMap: Dict[str, str], isInjective: bool = False, isSurjective: bool = False) → None[source]¶ Initialization of a TDG morphism (template).
Note
Especially for the purpose of instantiating templates of TDGs, it is possible to utilize
Z3TDGtemplate
instances fordomG
and/orcodomG
(which typechecks due to the fact that the classZ3TDGtemplate
is a subclass of the classZ3TypedDirectedGraph
). Parameters
mName – a string encoding the name of the morphism
domG – a
Z3TypedDirectedGraph
instance encoding the domain graphcodomG – a
Z3TypedDirectedGraph
instance encoding the codomain graphvMap – a dictionary encoding the vertexmapping
eMap – a dictionary encoding the edgemapping
isInjective – (optional) a boolean value encoding whether or not the morphism is injective
isSurjective – (optional) a boolean value encoding whether or not the morphism is surjective
Examples
Case 1: instantiating a concrete morphism between two fully specified TDGs:
>>> S = z3.Solver() >>> gA = Z3TypedDirectedGraph(S, 'gA', {'a1':'X', 'a2':'Y'}, {'e1':'Z'}, {'e1':('a1','a2')}) >>> gB = Z3TypedDirectedGraph(S, 'gB', {'b1':'X', 'b2':'Y', 'b3':'Y'}, {'f1':'Z'}, {'f1':('b1','b3')}) >>> mAB = Z3TDGmorphism('mAB', gA, gB, {'a1':'b1', 'a2':'b3'}, {'e1':'f1'})
Case 2: instantiating an injective morphism template between two TDG templates:
>>> S = z3.Solver() >>> tgA = Z3TDGtemplate(S, 'tgA', {'X', 'Y'}, {'Z'}, {'Z':('X','Y')}) >>> tgB = Z3TDGtemplate(S, 'tgB', {'X', 'Y'}, {'Z'}, {'Z':('X','Y')}) >>> mABtempl = Z3TDGmorphism('mAB', tgA, tgB, {'nilX':'nilX', 'nilY':'nilY'}, {'nilZ':'nilZ'})
Case 3: instantiating an injective morphism template between two fully specified TDGs for the purpose of using
Z3
to search for subgraph embeddings; to this end, the TDG morphism template has to be specified with nilelement mappings only:>>> S = z3.Solver() >>> gA = Z3TypedDirectedGraph(S, 'gA', {'a1':'X', 'a2':'Y'}, {'e1':'Z'}, {'e1':('a1','a2')}) >>> gB = Z3TypedDirectedGraph(S, 'gB', {'b1':'X', 'b2':'Y', 'b3':'Y'}, {'f1':'Z', 'f2':'Z'}, ... {'f1':('b1','b2'), 'f2':('b1','b3')}) >>> mAB = Z3TDGmorphism('mAB', gA, gB, {'nilX':'nilX', 'nilY':'nilY'}, {'nilZ':'nilZ'}) >>> chk = S.check() >>> if chk == z3.sat: ... print(S.model())


class
resmt.datatypes.
Z3TDGpredicate
(pName: str, domG: resmt.datatypes.Z3TypedDirectedGraph)[source]¶ Bases:
object
A (template for a) predicate for
Z3TypedDirectedGraphs
.For each vertex and edge sort, the predicate contains a boolean subpredicate, and moreover assertions are included to ensure that an edge with predicate
True
also has its endpoints carrying the predicatesTrue
.
__init__
(pName: str, domG: resmt.datatypes.Z3TypedDirectedGraph) → None[source]¶ Instantiation of a template of a boolean predicate over a typed directed graph.
 Parameters
pName – the name of the predicate
domG – a typed directed graph over which the predicate is to be constructed
Example
>>> S = z3.Solver() >>> vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY'} >>> eDictA = {'e1':'sortW', 'e2': 'sortT'} >>> stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')} >>> graphA = Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA) >>> predGraphA = Z3TDGpredicate('predGraphA', graphA)


class
resmt.datatypes.
Z3TDGspanPredicateTemplate
(sName: str, gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph)[source]¶ Bases:
object
A class for TDG monic span predicate templates to search for spans of TDGs.
Note
The typing of vertices and edges implies that the monic span must be “sortcompatible”, i.e. encodes a sortpreserving injective partial function.

__init__
(sName: str, gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph) → None[source]¶ Initialization of a boolean span predicate template.
It is important to note that the two input TDGs must be sortcompatible, i.e. if the input graphs do not satisfy this property a priori, one must invoke the
.patchNilElements
method in order to fix the sortmatching. Parameters
sName – the name of the boolean span predicate
gA – the first
Z3TypedDirectedGraph
instnce (“left leg” of the span)gB – the second
Z3TypedDirectedGraph
instnce (“right leg” of the span)
Example
>>> S = z3.Solver() >>> vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY', 'v4': 'sortZ'} >>> eDictA = {'e1':'sortW', 'e2': 'sortT'} >>> stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')} >>> graphA = Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA) >>> 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 = Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)
Next, we must adapt the sorts suitably via patching of nilelements: >>> graphA.patchNilElements(graphB) >>> graphB.patchNilElements(graphA)
Finally, we may instantiate the
Z3TDGspanPredicateTemplate
for the two TDGs: >>> spanPredAB = Z3TDGspanPredicateTemplate(‘spanPredAB’, graphA, graphB)

evaluateModel
(M: z3.z3.ModelRef) → Tuple[Set[Tuple[str, str]], Set[Tuple[str, str]]][source]¶ Evaluate the structure of a model for a TDG overlap.
 Parameters
M – a Z3 model reference (whose context must coincide with
self.solv.ctx
) Returns
A pair of sets of tuples of element names encoding the overlap structure, with the first set for the vertices and the second one for the edges.

genModelBlockingAsts
(M: z3.z3.ModelRef) → z3.z3.BoolRef[source]¶ Generate assertions to block a given model.
 Parameters
M – a Z3 model instance (whose context must coincide with
self.solv.ctx
) Returns
A
z3.Or
expression over a list of assertions of inequality of the predicate values and the model values over the range of all nonnil elements.


class
resmt.datatypes.
Z3TDGtemplate
(solv: z3.z3.Solver, gName: str, vSorts: Set[str], eSorts: Set[str], stSortsDict: Dict[str, Tuple[str, str]])[source]¶ Bases:
resmt.datatypes.Z3TypedDirectedGraph
Representation of templates of typed directed graphs in Z3.
Much as in the case of templates for typed sets, this class permits to encode templates of typed directed graphs for algorithms such as the pushout construction where the concrete elements of the graph and its source and target functions will only be fully instantiated at runtime of the algorithm. Technically, this feature is achieved by utilizing
Z3TypedSetTemplate
instances in lieu ofZ3TypedSet
instances at initialization of instance of the template class. The input data necessary for TDG templates is comprised ofSets of vertex and edgesorts, and
a dictionary of edgesort to edge source/target vertex sorts.
Examples
>>> S = z3.Solver() >>> vSrts = {'sortX', 'sortY'} >>> eSrts = {'sortW', 'sortT'} >>> stSrtsDict = {'sortX':('sortW','sortT'), 'sortY':('sortT','sortT')} >>> graphA = Z3TDGtemplate(S, 'gA', vSrts, eSrts, stSrtsDict)

solv
¶ a
Z3
solver instance

name
¶ the name of the TDG instance

stDict
¶ the source/target vertex incidence dictionary

vertices
¶ a
Z3TypedSet
instances representing the vertex set

edges
¶ a
Z3TypedSet
instance representing the edge set

src
¶ a
Z3TypedFunction
representing the source function

trgt
¶ a
Z3TypedFunction
representing the targetß function

stSortsDct
¶ a dictionary with edgesorts as keys and tuples of source/target vertex sorts as values

__init__
(solv: z3.z3.Solver, gName: str, vSorts: Set[str], eSorts: Set[str], stSortsDict: Dict[str, Tuple[str, str]]) → None[source]¶ Initialization of a
Z3TDGtemplate
object. Parameters
solv – Z3 solver instance
gName – the name of the graph
vSorts – a set of vertex sort names
eSorts – a set of edge sort names
stSortsDict – a dictionary with entries of the form
eSrt: (sSrt, tSrt)
, whereeSrt
is the name of an edge sort, whilesSrt
andtSrt
are the names of the source/target vertex sort names for edges of sorteSrt

display
(graphLayout: str = 'neato') → IPython.core.display.SVG¶ Display a rendering of the TDG in the current IPython or Jupyter lab interactive session.
 Parameters
graphLayout – (optional) a string with the name of a graph layouting mehtod (default: ‘neato’; alternative options are those provided by the
GraphViz
package, e.g.dot
,twopi
,fdp
,sfdp
andcirco
) Returns
An
IPython
SVG display instance.

isSortCompatibleWith
(gB: resmt.datatypes.Z3TypedDirectedGraph) → bool¶ Compare two
Z3TypedDirectedGraph
instances for sort compatibility.Two TDGs are defined to be sortcompatible if and only if they have precisely the same vertex and edgesorts, and if in addition their edgetosource/target sort “signatures” coincide.
 Parameters
gB – a second
Z3TypedDirectedGraph
instance to compare with Returns
A boolean value (with
True
indicating sortcompatibility).

patchNilElements
(gB: resmt.datatypes.Z3TypedDirectedGraph) → None¶ Patch nilelements for vertex and edge sorts not in original graph.
As an additional effect to merely adding the nilelements to the vertex and edge sets, the method also updates the source and target functions (s.th. the new niledges have source and target as nilelements of the sort “signature” of edges as in
gB
). Parameters
gB – a
Z3TypedDirectedGraph
instance from which to determine the additional sorts
Example
We first set up a
Z3
solver instance and two TDGs:>>> S = z3.Solver() >>> vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY'} >>> eDictA = {'e1':'sortW', 'e2': 'sortT'} >>> stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')} >>> graphA = Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA) >>> vDictB = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortZ'} >>> eDictB = {'e1':'sortW', 'e2': 'sortT', 'e3': 'sortU'} >>> stDictB = {'e1':('v1','v3'), 'e2':('v2','v3'), 'e3':('v1','v3')} >>> graphB = Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)
Then the mutual nilelement patching is performed as follows:
>>> graphA.patchNilElements(graphB) >>> graphB.patchNilElements(graphA)
Indeed, one may verify that now e.g.
graphA
has all the sorts it had before plus the new sorts ofgraphB
:>>> graphA.vertices.sorts >>> graphA.edges.sorts

renderNonEmbeddingAssertion
(gN: resmt.datatypes.Z3TypedDirectedGraph) → List[z3.z3.BoolRef]¶ Render assertions of a TDG not containing a forbidden pattern as a subgraph.
 Parameters
gN – a
Z3TypedDirectedGraph
instance encoding the forbidden pattern Returns
A list of Z3 assertions expressing the nonembedding constraint.

renderVisualization
(fName: str, graphLayout: str = 'neato') → IPython.core.display.SVG¶ Display and write to disk a rendering of the TDG.
 Parameters
fName – a filename (possibly with a path), where the suffix controls the output format
graphLayout – (optional) a string with the name of a graph layouting mehtod (default: ‘neato’; alternative options are those provided by the
GraphViz
package, e.g.dot
,twopi
,fdp
,sfdp
andcirco
)
..note :: Any format accessible for the
pydot
package is permitted (including e.g. PDF, SVG, JPG, …). Returns
An
IPython
SVG display instance.

writeTDGdataToJSONfile
(fName: str) → None¶ Routine to write the defining data of a
Z3TypedDirectedGraph
instance to a JSON file.The purpose of this routine is to permit a convenient way to store all information necessary to instantiate a
Z3TypedDirectedGraph
instance (except for theZ3
solver instance). Parameters
fName – the base name (possibly including a path) for the JSON file

class
resmt.datatypes.
Z3TypedDirectedGraph
(solv: z3.z3.Solver, gName: str, vDict: Dict[str, str], eDict: Dict[str, str], stDict: Dict[str, Tuple[str, str]])[source]¶ Bases:
object
Representation of typed directed graphs in Z3.
Following the convention “one vertextype source/tarhet signature per edge type”, typrd directed multigtraphs may be specified via providing the following data: 1. Names of vertices and edges (int he form of two dictionaries of strings, with the entry format
'elName':'elSort'
). 2. Sourcetarget incidence dictionaries (of the entry format'edgeName':('sourceVname', 'targetVname')
).Examples
>>> S = z3.Solver() >>> vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY'} >>> eDictA = {'e1':'sortW', 'e2': 'sortT'} >>> stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')} >>> graphA = Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA)
This will render a representation of a typed directed graph with three vertices, two edges and incidences as specified in the
stDictz
dictionary. Note that since in this example the two edges have different types, each of them is permitted to have a different “typesignature” in terms of their source and targetvertex types/>>> gB = Z3TypedDirectedGraph(S, 'gEmpty', {}, {}, {})
This will render a representation of an empty graph. Special default types are utilized in order to give the nilelements an invariant type, and the nilelement of the vertex set is both the source and target “vertex” of the niledge.

solv
¶ a
Z3
solver instance

name
¶ the name of the TDG instance

stDict
¶ the source/target vertex incidence dictionary

vertices
¶ a
Z3TypedSet
instances representing the vertex set

edges
¶ a
Z3TypedSet
instance representing the edge set

src
¶ a
Z3TypedFunction
representing the source function

trgt
¶ a
Z3TypedFunction
representing the targetß function

stSortsDct
¶ a dictionary with edgesorts as keys and tuples of source/target vertex sorts as values

__init__
(solv: z3.z3.Solver, gName: str, vDict: Dict[str, str], eDict: Dict[str, str], stDict: Dict[str, Tuple[str, str]]) → None[source]¶ Initialization of a Z3TypedDirectedGraph object.
 Parameters
solv – Z3 solver instance
gName – the name of the graph
vDict – a dictionary of vertex name/sort name pairs
eDict – a dictionary of edge name/sort name pairs
stDict – a dictionary with entries of the form
e: (s, t)
, wheree
is the name of an edge, whiles
andt
are the names of the source/target vertices of the edgee

display
(graphLayout: str = 'neato') → IPython.core.display.SVG[source]¶ Display a rendering of the TDG in the current IPython or Jupyter lab interactive session.
 Parameters
graphLayout – (optional) a string with the name of a graph layouting mehtod (default: ‘neato’; alternative options are those provided by the
GraphViz
package, e.g.dot
,twopi
,fdp
,sfdp
andcirco
) Returns
An
IPython
SVG display instance.

isSortCompatibleWith
(gB: resmt.datatypes.Z3TypedDirectedGraph) → bool[source]¶ Compare two
Z3TypedDirectedGraph
instances for sort compatibility.Two TDGs are defined to be sortcompatible if and only if they have precisely the same vertex and edgesorts, and if in addition their edgetosource/target sort “signatures” coincide.
 Parameters
gB – a second
Z3TypedDirectedGraph
instance to compare with Returns
A boolean value (with
True
indicating sortcompatibility).

patchNilElements
(gB: resmt.datatypes.Z3TypedDirectedGraph) → None[source]¶ Patch nilelements for vertex and edge sorts not in original graph.
As an additional effect to merely adding the nilelements to the vertex and edge sets, the method also updates the source and target functions (s.th. the new niledges have source and target as nilelements of the sort “signature” of edges as in
gB
). Parameters
gB – a
Z3TypedDirectedGraph
instance from which to determine the additional sorts
Example
We first set up a
Z3
solver instance and two TDGs:>>> S = z3.Solver() >>> vDictA = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortY'} >>> eDictA = {'e1':'sortW', 'e2': 'sortT'} >>> stDictA = {'e1':('v1','v2'), 'e2':('v3','v1')} >>> graphA = Z3TypedDirectedGraph(S, 'gA', vDictA, eDictA, stDictA) >>> vDictB = {'v1':'sortX', 'v2': 'sortX', 'v3': 'sortZ'} >>> eDictB = {'e1':'sortW', 'e2': 'sortT', 'e3': 'sortU'} >>> stDictB = {'e1':('v1','v3'), 'e2':('v2','v3'), 'e3':('v1','v3')} >>> graphB = Z3TypedDirectedGraph(S, 'gB', vDictB, eDictB, stDictB)
Then the mutual nilelement patching is performed as follows:
>>> graphA.patchNilElements(graphB) >>> graphB.patchNilElements(graphA)
Indeed, one may verify that now e.g.
graphA
has all the sorts it had before plus the new sorts ofgraphB
:>>> graphA.vertices.sorts >>> graphA.edges.sorts

renderNonEmbeddingAssertion
(gN: resmt.datatypes.Z3TypedDirectedGraph) → List[z3.z3.BoolRef][source]¶ Render assertions of a TDG not containing a forbidden pattern as a subgraph.
 Parameters
gN – a
Z3TypedDirectedGraph
instance encoding the forbidden pattern Returns
A list of Z3 assertions expressing the nonembedding constraint.

renderVisualization
(fName: str, graphLayout: str = 'neato') → IPython.core.display.SVG[source]¶ Display and write to disk a rendering of the TDG.
 Parameters
fName – a filename (possibly with a path), where the suffix controls the output format
graphLayout – (optional) a string with the name of a graph layouting mehtod (default: ‘neato’; alternative options are those provided by the
GraphViz
package, e.g.dot
,twopi
,fdp
,sfdp
andcirco
)
..note :: Any format accessible for the
pydot
package is permitted (including e.g. PDF, SVG, JPG, …). Returns
An
IPython
SVG display instance.

writeTDGdataToJSONfile
(fName: str) → None[source]¶ Routine to write the defining data of a
Z3TypedDirectedGraph
instance to a JSON file.The purpose of this routine is to permit a convenient way to store all information necessary to instantiate a
Z3TypedDirectedGraph
instance (except for theZ3
solver instance). Parameters
fName – the base name (possibly including a path) for the JSON file


class
resmt.datatypes.
Z3TypedFunction
(solv: z3.z3.Solver, fName: str, domSet: resmt.datatypes.Z3TypedSet, codomSet: resmt.datatypes.Z3TypedSet, fData: Dict[str, str], isInjective: bool = False, isSurjective: bool = False)[source]¶ Bases:
object
A function of Z3TypedSet objects as domain and codomain.

__init__
(solv: z3.z3.Solver, fName: str, domSet: resmt.datatypes.Z3TypedSet, codomSet: resmt.datatypes.Z3TypedSet, fData: Dict[str, str], isInjective: bool = False, isSurjective: bool = False) → None[source]¶ Initialization of a Z3TypedFunction object.
Example
>>> S = z3.Solver() >>> setD = Z3TypedSet(S, 'domSet', {'a1':'sortX', 'a2':'sortX', 'a3': 'sortY'}) >>> setC = Z3TypedSet(S, 'codomSet', {'b1':'sortX', 'b2':'sortX', 'b3': 'sortY', 'b4':'sortZ'}) >>> f = Z3TypedFunction(S,'f', setD, setC, {'a1':'b2', 'a2':'b1','a3':'b4'}, isInjective = True)
This renders both the respective
Z3
object instnces as well as the requisite assertions in order to faithfully encode a function of typed sets. As a special case, consider below as another example a function of empty sets:>>> emptySet = Z3TypedSet(S, 'emptySet', {}) >>> g = Z3TypedFunction(S,'g', emptySet, emptySet, {}, isInjective = True)
 Parameters
solv – a Z3 solver instance
fName – function name (as string)
domSet – a
Z3TypedSet
instance encoding the domaincodomSet – a
Z3TypedSet
instance encoding the codomainfData – a dictionary with entries key/value pairs of names of domain/codomain elements, encoding the function itself
isInjective – (optional) boolean parameter declaring whether or not the function is injective (default:
False
)isSurjective – (optional) boolean parameter declaring whether or not the function is surjective (default:
False
)


class
resmt.datatypes.
Z3TypedSet
(solv: z3.z3.Solver, setName: str, els: Dict[str, str])[source]¶ Bases:
object
Encode sets of elements with different types.
A
Z3TypedSet
object is a data structure that serves the dual purpose of implementing an encoding of a set within an instance of a Z3 solver, and at the same time providing access to a number of attributes storing information important for the algorithms defined in this package.Note
Since in some of the algorithms (e.g. in the definition of functions between tyoed sets) it is necessary to assert that only constants of the same “global” sort are mappable to each other, we store the name of the set and the name of the sorts of the elements provided as input at initialization in two different fields. Then for the set at hand, the Z3 sorts are named
setName+''+elSortName
, to ensure that the sort universe is closed for each set. In declarations of functions with domain some typed set A and codomain some typed set B, one may then emulate a “global” type mapping constraint via asserting that only constants of typesetAname+''+elSortName
may be mapped to constants of typesetBname+''+elSortName
(with additional issues related to nilcarriers etc. discussed in the documentation of the typed function class).
solv
¶ a Z3 solver instance provided at initialization

setName
¶ a string value containing the name of the set

sortNames
¶ the “global” names of the sorts of the elements

els
¶ a dictionary of element names as keys and “global” element sort names as values

sorts
¶ a dictionary with “local” sort names as keys and the corresponding Z3 sort declaration references as values (where the “local” names are defined as prepending the
setName
to each “global” sort name inelSortNames
)

subsets
¶ a dictionary with “global” sort names as keys and Z3 enumeration sort instances (one for each subset) as values

subsetEls
¶ a dictionary with “global” sort names as keys and the different Z3 constants of the Z3 enumeration sort for the corresponding sort as values (with the constants representing elements of the given sort)

subsetNamesToEls
¶ a dictionary with “global” sort names as keys, and with ordered dictionaries of element name/Z3 constant entries (in order to permit accessing Z3 constants by element names)

nilEls
¶ a dictionary with sort names as keys and Z3 constants as values (representing nilelements)

__init__
(solv: z3.z3.Solver, setName: str, els: Dict[str, str]) → None[source]¶ Instantiate the Z3 set data from a dictionary of element names and types.
Examples
>>> S = z3.Solver() >>> setA = Z3TypedSet(S, 'setA', {'a':'elSort1', 'b':'elSort1', 'c':'elSort2'})
An example of an empty set:
>>> emptySet = Z3TypedSet(S, 'setB', {})
 Parameters
solv – the handle to a Z3 solver instance (automatically passes the current context)
setName – the name the Z3 sort for the set
els – dictionary of element names and types (given as strings)
 Returns
Setting up the Z3TypedSet object. Moreover, a sideeffect of executing the method consists in introducing the necessary definitions of Z3 sorts for the different element sorts and nilelements for each of the element sorts.
Note
If an empty
els
dictionary is specified, the method instantiates a Z3 constant nonetheless for a nilelement whose sort is named'_DEFAULT'
, since fuhnctions must be total in Z3, which is why nilelements are neeeded even for empty sets.Z3 Python API programming details
In order to reference the context of a solver instance
solv
, it suffices to declare the sorts within the contextsolv.ctx
ofsolv
. All other directives (constant or function declarations, assertions etc.) will automatically inherit their context from the sorts.Python 3 programing gems
In some of the constructs here and elsewhere of the code, we use a new language feature in Python 3 (available in Python version > 3.5) that permits to merge two dictionaries without having to update one into the other (cf. this StackExchange article). Given dictionaries
x
andy
, the merge of the two is obtained as{**x, **y}
.

getElandSrtName
(elName: str) → Tuple[z3.z3.ExprRef, str][source]¶ Get both the Z3 constant and the name of the element sort associated to an element name.

patchNilElements
(setB: resmt.datatypes.Z3TypedSet) → None[source]¶ Patch nilelements.
Given a second
Z3TypedSet
instancesetB
, extract the sorts present insetB
but not in the original set, and then add extra nilelements to the original set for each of these extra sorts. Parameters
setB – a
Z3TypedSet
instance whose additional sorts should be “patched” into theself
insstance (and suitable nilelements added, one for each additional sort)
Example
>>> S = z3.Solver() >>> setA = Z3TypedSet(S, 'setA', {'a':'elSort1', 'b':'elSort1', 'c':'elSort2'}) >>> emptySet = Z3TypedSet(S, 'setB', {}) >>> emptySet.patchNilElements(setA)


class
resmt.datatypes.
Z3TypedSetAutomorphismTemplate
(aName: str, domSet: resmt.datatypes.Z3TypedSet)[source]¶ Bases:
object
A template for an automorphism of a typed set.

__init__
(aName: str, domSet: resmt.datatypes.Z3TypedSet) → None[source]¶ Instantiates assertions that permit to find an automorphism of the given set.
 Parameters
aName – the name of the resulting
Z3TypedAutomorphismTemplate
instancedomSet – the
Z3TypedSet
of which to render the automorphism assertions
Example
>>> S = z3.Solver() >>> setD = Z3TypedSet(S, 'domSet', {'a1': 'sortX', 'a2': 'sortX', 'a3': 'sortY'}) >>> autD = Z3TypedSetAutomorphismTemplate('autD', setD)


class
resmt.datatypes.
Z3TypedSetPredicate
(pName: str, domSet: resmt.datatypes.Z3TypedSet)[source]¶ Bases:
object
An assembly of boolean predicates (one per sortwise subset).

__init__
(pName: str, domSet: resmt.datatypes.Z3TypedSet) → None[source]¶ Instantiation of a boolean predicate (template) on a typed set.
 Parameters
pName – a string containing the name of the predicate
domSet – a
Z3TypedSet
instance encoding the domain set of the rpedicate
Example
>>> S = z3.Solver() >>> setD = Z3TypedSet(S, 'domSet', {'a1': 'sortX', 'a2': 'sortX', 'a3': 'sortY'}) >>> predD = Z3TypedSetPredicate('predD', setD)


class
resmt.datatypes.
Z3TypedSetSpanPredicateTemplate
(sName: str, setA: resmt.datatypes.Z3TypedSet, setB: resmt.datatypes.Z3TypedSet, isMonic: bool = False)[source]¶ Bases:
object
A template for a monic span of TDGs and of the required assertions.

__init__
(sName: str, setA: resmt.datatypes.Z3TypedSet, setB: resmt.datatypes.Z3TypedSet, isMonic: bool = False) → None[source]¶ Instantiation of a span predicate template between two typed sets.
 Parameters
sName – the name of the span predicate template
setA – the first
Z3TypedSet
instancesetB – the second
Z3TypedSet
instanceisMonic – a Boolean indicating whether the span is to be minic (default:
False
)
Example
>>> S = z3.Solver() >>> setA = Z3TypedSet(S, 'setA', {'a1':'sortX', 'a2':'sortX', 'a3': 'sortY'}) >>> setB = 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 nilelements if necessary as follows: >>> setA.patchNilElements(setB) >>> setB.patchNilElements(setA) >>> spanPredAB = Z3TypedSetSpanPredicateTemplate(‘predAB’, setA, setB, isMonic=True)

evaluateModel
(M: z3.z3.ModelRef) → Set[Tuple[str, str]][source]¶ Evaluate the structure of a model for a typed set overlap.
 Parameters
M – a Z3 model reference (whose context must coincide with
self.solv.ctx
) Returns
A set of tuples of element names encoding the overlap structure.

genModelBlockingAsts
(M: z3.z3.ModelRef) → z3.z3.BoolRef[source]¶ Generate assertions to block a given model.
 Parameters
M – a Z3 model instance (whose context must coincide with
self.solv.ctx
) Returns
A
z3.Or
expression over a list of assertions of inequality of the predicate values and the model values over the range of all nonnil elements.


class
resmt.datatypes.
Z3TypedSetTemplate
(solv: z3.z3.Solver, setName: str, elSorts: Set[str])[source]¶ Bases:
resmt.datatypes.Z3TypedSet
A templating class for sets of elements with different types.
Mainly for purposes of computing pushouts, this class emulates closely the structure of the
Z3TypedSet
class, yet forgoes the range closure part of the initialization routine. More precisely, while the initialization method of theZ3TypedSet
class relies upon thez3.EnumSort
functionality of theZ3
API,Z3TypedSetTemplate
instances are initialized via 1) issuing az3.DeclareSort
call for each sort of elements, and 2) only explicitly instantiating the nilelements asZ3
constants for each sort. In consequence, instances of theZ3TypedSetTemplate
are useful in situations such as pushout constructions where the concrete nonnil element content of a given respective typed set is only determined at runtime of the algorithm.
solv
¶ a Z3 solver instance provided at initialization

setName
¶ a string value containing the name of the set

sortNames
¶ the “global” names of the sorts of the elements

els
¶ a dictionary of element names as keys and “global” element sort names as values

sorts
¶ a dictionary with “local” sort names as keys and the corresponding Z3 sort declaration references as values (where the “local” names are defined as prepending the
setName
to each “global” sort name inelSortNames
)

subsets
¶ a dictionary with “global” sort names as keys and Z3 enumeration sort instances (one for each subset) as values

subsetEls
¶ a dictionary with “global” sort names as keys and the different Z3 constants of the Z3 enumeration sort for the corresponding sort as values (with the constants representing elements of the given sort)

subsetNamesToEls
¶ a dictionary with “global” sort names as keys, and with ordered dictionaries of element name/Z3 constant entries (in order to permit accessing Z3 constants by element names)

nilEls
¶ a dictionary with sort names as keys and Z3 constants as values (representing nilelements)

__init__
(solv: z3.z3.Solver, setName: str, elSorts: Set[str]) → None[source]¶ Instantiate the Z3 typed set template data from a set of element types.
Examples
>>> S = z3.Solver() >>> setA = Z3TypedSetTemplate(S, 'setA', {'elSort1', 'elSort2'})
 Parameters
solv – the handle to a Z3 solver instance (automatically passes the current context)
setName – the name the Z3 sort for the set
elSorts – a set of element types (given as strings)
 Returns
Setting up the
Z3TypedSetTemplate
object, with the sideeffect of introducing the necessary definitions ofZ3
sorts for the different element sorts andZ3
constants for the nilelements of each of the element sorts.

getEl
(elName: str) → z3.z3.ExprRef¶ Get the Z3 constant associated to an element name.

getElandSrtName
(elName: str) → Tuple[z3.z3.ExprRef, str]¶ Get both the Z3 constant and the name of the element sort associated to an element name.

patchNilElements
(setB: resmt.datatypes.Z3TypedSet) → None¶ Patch nilelements.
Given a second
Z3TypedSet
instancesetB
, extract the sorts present insetB
but not in the original set, and then add extra nilelements to the original set for each of these extra sorts. Parameters
setB – a
Z3TypedSet
instance whose additional sorts should be “patched” into theself
insstance (and suitable nilelements added, one for each additional sort)
Example
>>> S = z3.Solver() >>> setA = Z3TypedSet(S, 'setA', {'a':'elSort1', 'b':'elSort1', 'c':'elSort2'}) >>> emptySet = Z3TypedSet(S, 'setB', {}) >>> emptySet.patchNilElements(setA)


class
resmt.datatypes.
Z3directMethodStatsData
[source]¶ Bases:
resmt.datatypes.Z3statsData
Auxiliary data class to store and evaluate Z3 statistics data for the “direct” method.
In contrast to the
Z3statsData
parent class, instances of this subclass store some additional data specific to the “direct” (i.e. the “generateandtest”) method, in particular runtimes and statistics data from the two different phases. For convenience in comparing the overall performance of this method against other methods, the subclass exposes the same fields as the parent class, which hold the joint information on both phases of the “direct” method.
storeStatsAsDict
(rKey: str, stats: z3.z3.Statistics) → None¶ Store Z3 statistics data from a solver run into a dictionary.
 Parameters
rKey – the key under which to store the statistics data of the solver run
stats – a
z3.Statistics
instance
 Returns
A dictionary with one keyvalye pair per entry in
self.stats[rKey]
.
Example
>>> S = z3.Solver() >>> x, y = z3.Ints('x y') >>> S.add(x > y) >>> S.check() >>> statsData = Z3statsData() >>> statsData.storeStatsAsDict('run1', 'test', S.statistics()) >>> statsDct = statsData.stats

storeStatsAsDictForPhase
(rKey: str, stats: z3.z3.Statistics, phase: str) → None[source]¶ Store Z3 statistics data from a solver run into a dictionary.
 Parameters
rKey – the key under which to store the statistics data of the solver run
stats – a
z3.Statistics
instancephase – a string (either
'generate'
or'test'
) for encoding the phase in which the statistics data was collected
 Returns
A dictionary with one keyvalye pair per entry in
self.stats[rKey]
as well as a copu in the phasespecific statistics dictionary fieldself.statsPhases[phase][rKey]
.
Example
>>> S = z3.Solver() >>> x, y = z3.Ints('x y') >>> S.add(x > y) >>> S.check() >>> statsData = Z3directMethodStatsData() >>> statsData.storeStatsAsDictForPhase('run1', 'test', S.statistics()) >>> statsDct = statsData.stats


class
resmt.datatypes.
Z3experimentsData
(cTimes: List[float], statsData: resmt.datatypes.Z3statsData, statsStr: str, overlapsData: resmt.datatypes.Z3overlapsData, timeOutRunID: str)[source]¶ Bases:
object
Data class for storing outputs of individual experiments.

__init__
(cTimes: List[float], statsData: resmt.datatypes.Z3statsData, statsStr: str, overlapsData: resmt.datatypes.Z3overlapsData, timeOutRunID: str) → None[source]¶ Store data from experiments.
 Parameters
cTimes – a list of computation times (in seconds), where the last entry encodes the time needed to determine
unsat
statsData – a dictionary with keys the runids and values dictionaries encoding statistical information on the individual solver runs
statsStr – the string of statistics data generated from teh last solver run
overlapsData – a
Z3overlapsData
instance encoding a list of overlaps (as well as the data on the two input TDGs of the given routine necessary in order to permit e.g. rendering pushout objects)timeOutRunID – a string encoding the id of the run that led to a solver timeout; in case no timeout occurred, the default value of this entry is ““


class
resmt.datatypes.
Z3overlapsData
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, overlaps: List[Tuple[Set[Tuple[str, str]], Set[Tuple[str, str]]]])[source]¶ Bases:
object
Data class for storing and evaluating overlap data of typed directed graphs.

__init__
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, overlaps: List[Tuple[Set[Tuple[str, str]], Set[Tuple[str, str]]]]) → None[source]¶ Store overlap data into a Z3overlapData class instance.
 Parameters
gA – a
Z3TypedDirectedGraph
instancegB – a
Z3TypedDirectedGraph
instanceoverlaps – a list of overlaps of
gA
andgB
, where each overlap is encoded as a tuple of sets, the first of which encodes the vertex overlaps (in the format(vA, vB)
ifvA
is overlapped withvB
), and analogously for the edges

renderPushoutObject
(S: z3.z3.Solver, idx: int, gPOname: str) → resmt.datatypes.Z3TypedDirectedGraph[source]¶ Render a
Z3TypedDirectedGraph
instance encoding a pushout from overlap data. Parameters
S – a
Z3
solver instanceidx – the index of the overlap in the list of overlaps
gPOname – the name to be given to the pushout object
 Returns
A
Z3TypedDirectedGraph
instance encoding the pushout object ofself.gA
withself.gB
along the overlapself.overlaps[idx]
.


class
resmt.datatypes.
Z3statsData
[source]¶ Bases:
object
Auxiliary data class to store and evaluate Z3 statistics data.
The main purpose of this class is to facilitate the evaluation of
Z3
solver statistics output from the various algorithms in this package, and to provide a template for various extensions and custom data access methods.
storeStatsAsDict
(rKey: str, stats: z3.z3.Statistics) → None[source]¶ Store Z3 statistics data from a solver run into a dictionary.
 Parameters
rKey – the key under which to store the statistics data of the solver run
stats – a
z3.Statistics
instance
 Returns
A dictionary with one keyvalye pair per entry in
self.stats[rKey]
.
Example
>>> S = z3.Solver() >>> x, y = z3.Ints('x y') >>> S.add(x > y) >>> S.check() >>> statsData = Z3statsData() >>> statsData.storeStatsAsDict('run1', 'test', S.statistics()) >>> statsDct = statsData.stats


resmt.datatypes.
genForbiddenTDGrelations
(fG: resmt.datatypes.Z3TypedDirectedGraph) → Tuple[List[Dict[str, str]], List[Tuple[float, str]], str][source]¶ Generation of forbidden relation from a forbidden TDG pattern.
 Parameters
fG – a “forbidden TDG pattern”
 Returns
A list of predicate dictionaries, where each dictionary represents a possible decomposition of the “forbidden TDG pattern”
fG
into a monic span where none of the entries in the entries in the span coincide withfG
itself, and with predicates (per vertex/edge infG
) taking values'<'
(left),'='
(both) and'>'
(right) according to which “leg” of the span an element is included in. The list is curated by isomorphisms, i.e. only one representative per isomorphismclass induced by automorphisms offG
is included.

resmt.datatypes.
generateTDGoverlapsDPEstrategy
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, frClist: List[resmt.datatypes.Z3TDGfrContainer]) → resmt.datatypes.Z3experimentsData[source]¶ Generate overlaps of TDGs compliant with forbidden relation constraints.
 Parameters
gA – a
Z3TypedDirectedGraph
instancegB – a
Z3TypedDirectedGraph
instancefrClist – a list of
Z3TDGfrContainer
instances encoding the forbidden relations
 Returns
A list of computation times for each individual result.
A dictionary with a complete set of statistics information for ecah
Z3
solver runA string containing some statistics on the overall performance of the
Z3
solver runs.A list of valid partial overlaps of the two TDGs, encoded as Tuples of sets of element name pairs (with the first set coding for the vertices, and the second for the edges).
The data is returned in the form of a
Z3experimentsData
instance. Return type
The following data is generated
Note
The design choice to encode the forbidden relation data in the form of
Z3TDGfrContainer
instances has been taken in order to permit the precomputation of the (static) data on forbidden relations given the particular set of negative pattern constraints for the problem at hand. For the overlap finding routine itself, only a computationally inexpensive translation of the resulting doublepullback embedding (DPE) constraints for the input TDGsgA
andgB
is rendered, so that the computational price for computing the forbidden relation data must only be paid once before a possibly large set of overlapsearching runs is executed.

resmt.datatypes.
generateTDGoverlapsDirectStrategy
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, forbiddenPatternsList: List[resmt.datatypes.Z3TypedDirectedGraph]) → resmt.datatypes.Z3experimentsData[source]¶ Generate overlaps of TDG modulo forbidden patterns via the “direct” strategy.
The “direct” strategy (also referred to as the “generateandtest” strategy) for finding overlaps of two typed directed graphs such that each overlap posesses a pushout that does not contain any of a list of “forbidden patterns” consists of the following phases:
Generation phase: determine all (monic) overlaps without taking into account the forbidden pattern constraints
Test phase: for each candidate overlap, form the pushout object and determine whether or not the pushout object possesses any of the “forbidden patterns” as a subgraph; if not, include the overlap in the list of results
 Parameters
gA – a
Z3TypedDirectedGraph
instancegB – a
Z3TypedDirectedGraph
instanceforbiddenPatternsList – a list of
Z3TypedDirectedGraph
instances, each of which encodes one “forbidden pattern”
 Returns
a list of computation times for the individual
Z3
solver runs for determining the unconstrainted overlaps in the “generation phase”statsistics data on the
Z3
solver runs in the “generation” phasea string containing some information on the performance of the
Z3
solver runs (such as memory consumption etc.) in the first phasea list of tuples of the form
(t, b, gPO)
, wheret
is the computation time needed by theZ3
solver to determine the “test phase” computation for the given candidate overlap,b
is a Boolean value (whereTrue
indicates that the overlap is consistent with the constraints), and wheregPO
is the pushout graph of the overlapstatsistics data on the
Z3
solver runs in the “test” phasea string containing some information on the performance of the
Z3
solver runs (such as memory consumption etc.) in the second phase
This data is returned in the form of a
Z3experimentsData
instance. Return type
The output is divided into three parts

resmt.datatypes.
generateTDGoverlapsImplicitStrategy
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, forbiddenPatternsList: List[resmt.datatypes.Z3TypedDirectedGraph]) → resmt.datatypes.Z3experimentsData[source]¶ Generate overlaps of TDGs compliant with forbidden pattern constraints via the “implicit” strategy.
For the “implicit” strategy, certain features of the
Z3
API (i.e. the ability to utilizez3.EnumSort
encodigns for the explicitly specified input TDGsgA
andgB
, but an implicit encoding for a pushout graph viaz3.Const
calls) permits to verify “onthefly” whether or not a given candidate overlap would violate the “forbidden pattern” constraints. As such, this strategy poses an alternative to the DPE strategy, and differs from the “direct” strategy in that the verification of pushout consistency is only performed in the latter after generating all candidate overlaps without the constraints. Parameters
gA – a
Z3TypedDirectedGraph
instancegB – a
Z3TypedDirectedGraph
instanceforbiddenPatternsList – a list of
Z3TypedDirectedGraph
instances encoding the “forbidden patterns”
 Returns
A list of computation times for each individual result.
A dictionary with a complete set of statistics information for ecah
Z3
solver runA string containing some statistics on the overall performance of the
Z3
solver runs.A list of valid partial overlaps of the two TDGs, encoded as Tuples of sets of element name pairs (with the first set coding for the vertices, and the second for the edges).
This set of data is returned in the form of a
Z3experimentsData
instance. Return type
The following data is generated

resmt.datatypes.
generateTDGpushout
(gA: resmt.datatypes.Z3TypedDirectedGraph, gB: resmt.datatypes.Z3TypedDirectedGraph, PhiData: Tuple[Set[Tuple[str, str]], Set[Tuple[str, str]]]) → Tuple[Dict[str, str], Dict[str, str], Dict[str, Tuple[str, str]]][source]¶ Generate the pushout of two TDGs along a given (monic) overlap.
 Parameters
gA – a
Z3TypedDirectedGraph
instancegB – a
Z3TypedDirectedGraph
instancePhiData – a tuple of dictionaries encoding vertex and edgeoverlaps (i.e. every element name pair encodes that these elements are in the overlap of
gA
andgB
)
 Returns
A triple of data encoding the pushout object, consisting of
a dictionary of
vertex name: vertex sort
entriesa dictionary of
edge name: edge sort
entriesa dictionary of
edge name: (source vertex name, target vertex name)
entries.
Note
This data may be utilized to instantiate a TDG that represents this pushout object (e.g. for purposes of visualization).

resmt.datatypes.
loadExpsDataFromJSONfile
(fName: str, expName: str) → resmt.datatypes.ExperimentSpec[source]¶ Load the data defining an experiment from a JSON data file.
 Parameters
fName – the file name (possibly including a path) to a JSON file
expName – the name of the experiment to load

resmt.datatypes.
renderTDGdataFromJSONfile
(fName: str) → Any[source]¶ Read out the TDG data from a data file in JSON format.
This is the inverse method to the
writeTDGdataToJSONfile
method (and likely will only be useful to operate on JSON files generated with said method).Note
Due to a limitation of the JSON file format, storing TDG data via the
writeTDGdataToJSONfile
method inherently converts the tuples in thestDict
fields into lists. This defect is fixed via the additional “repackaging” step performed by the present method. Parameters
fName – the filename of the JSON input file
 Returns
A dictionary of dictionaries, with the toplevel dictionary having keys
gName
,vDict
,eDict
andstDict
(i.e. the data encoding a TDG).

resmt.datatypes.
renderTDGfromJSONfile
(fName: str, gName: str, S: z3.z3.Solver) → resmt.datatypes.Z3TypedDirectedGraph[source]¶ Render a
Z3TypedDirectedGraph
instance from data stored in a JSON file. Parameters
fName – the JSON file containing the TDG data
gName – the name under which the data for the TDG is stored (which doubles as the name of the TDG)
S – a
Z3
solver instance within which the TDG should be instantiated
 Returns
A
Z3TypedDirectedGraph
instance rendered from the TDG data read from the JSON file.

resmt.datatypes.
runExperiments
(experimentSpecs: List[resmt.datatypes.ExperimentSpec], resultsFname: str) → None[source]¶ Auxiliary method to facilitate conducting experiments.
 Parameters
experimentSpecs – a list of
ExperimentSpec
instancesresultsFname – the name (possibly with a path) of a JSON file for storing the experimental results
experiments.py¶
This module contains methods that permit render execution time tests, visualizations and other experiments with routines included in ReSMT
.

resmt.experiments.
genExecTimePlot
(cTimes: List[float], statsInfo: str, titleStr: str, fName: str) → None[source]¶ Generate execution time Logbar plot with average time marked.
 Parameters
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 Logplot 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 filenamefName
.

resmt.experiments.
genFrExecTimePlot
(cTimes: List[Tuple[float, str]], statsInfo: str, titleStr: str, fName: str) → None[source]¶ Generate execution time Logbar plot with average time marked.
 Parameters
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 Logplot 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 filenamefName
.

resmt.experiments.
genOverlaps
(setBname: str, elsBnames: List[str], setAname: str, elsAnames: List[str], S: z3.z3.Solver) → Tuple[List[float], str][source]¶ 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.
 Parameters
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 untilunsat
) and a string containing Z3 solver statistics data is returned.

resmt.experiments.
genOverlapsV2
(setBname: str, elsBnames: List[str], setAname: str, elsAnames: List[str], S: z3.z3.Solver) → Tuple[List[float], str][source]¶ 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.
 Parameters
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 untilunsat
) is returned.

resmt.experiments.
genSetOverlapExperiment
(S: z3.z3.Solver, nAels: int, nBels: int, tStrExtra: str = '', pathStr: str = '') → Tuple[List[float], str][source]¶ Generate a set overlap finding experiment.
 Parameters
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.

resmt.experiments.
genSetOverlapExperimentV2
(S: z3.z3.Solver, nAels: int, nBels: int, tStrExtra: str = '', pathStr: str = '') → Tuple[List[float], str][source]¶ Generate a set overlap finding experiment.
 Parameters
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.

resmt.experiments.
generateForbiddenRelations
(elsNames: List[str]) → Tuple[List[Dict[str, str]], List[Tuple[float, str]], str][source]¶ 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.
 Parameters
elsNames – list of set element names
 Returns
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 isocheck and ‘unsat’ for the final
unsat
run.A string with the statistics summary of the Z3 solver instance used.
 Return type
The routine returns two pieces of data

resmt.experiments.
numSetInjectivePartialOverlaps
(m: int, n: int) → int[source]¶ Function to compute the number of injective partial set overlaps.
Given a set
A
of cardinalitym
and a setB
of cardinalitym+n
, the exact formula for the number of injective partial overlaps of the two sets is given by Parameters
m – cardinality of the smaller set
n – number of additional elements (possibly 0) in the larger set
 Returns
Number of injective partial overlaps.

resmt.experiments.
render3DplotsOfInjPartialObverlaps
(mMax: int, nMax: int, fName: str) → None[source]¶ Render a 3D plot of the numbers of injective partial overlaps between to (finite) sets.
 Parameters
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 logplot will be rendered and (depending on the capabilities of the current Python interface) both displayed and stored to a PDF file.

resmt.experiments.
renderVisualization
(frListInput: List[Dict[str, str]], workDir: str, plotFN: str, templateDir: str, plotLayout: str = '2:1') → None[source]¶ Render the forbidden relations as a grid of graphics.
 Parameters
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()+'/jinja2templates'
)plotLayout – (optional) choice of layout option (
'2:1'
or'1:1'
; default:'2:1'
)
 Returns
Renders PDFs
plotFN+'.pdf'
andplotFN+'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.
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
submodule of ReSMT
.

resmt.visualizations.
displaySVGtable
(tabData: Dict[str, List[str]], width: str = '100%') → None[source]¶ “Display a set of SVG images in an HTML table.
This method is adapted from code by Brian Naughton. 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). Parameters
tabData – a dictionary with entries of the form
'header entry': ['SVG filename 1',...]
, i.e. the data necessary to fill a column of the tablewidth – (optional) a string of the form
"x%"
, withx
an integer between0
and100
(default value:"100%"
)

class
resmt.visualizations.
nxTypedDirectedGraph
(G: resmt.datatypes.Z3TypedDirectedGraph, drawGraph: bool = True, writeGraph: bool = False, fileName: str = None, gLayout: str = 'neato')[source]¶ Bases:
object
Networkx representation of typed directed graphs.

__init__
(G: resmt.datatypes.Z3TypedDirectedGraph, drawGraph: bool = True, writeGraph: bool = False, fileName: str = None, gLayout: str = 'neato') → None[source]¶ Instantiating a Networkx representation of a Z3TypedDirectedGraph.
 Parameters
G – a
Z3TypedDirectedGraph
instancedrawGraph – (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
andcirco
).
Note
The available fileformats 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 plainext 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

A note on the Python types of the native Z3 API¶
Executing the following code permits to determine the types of the different kinds of instances accessible via the official Z3 Python API:
import z3
A = z3.DeclareSort('A') # a Z3 sort declaration
X = z3.Const('X', A) # a Z3 constant expression declaration
F = z3.Function('F', A, A) # a Z3 function expression declaration
# a Z3 assertion declarations
ast1 = z3.ForAll(z3.Const('Y', A), z3.Const('Y', A) == X)
ast2 = z3.Exists(z3.Const('Z',A), F(z3.Const('Z',A)) == X)
ast12 = z3.And([ast1, ast2])
s = z3.Solver()
s.add(ast12)
sC = s.check()
sM = s.model()
for z in [A,X,F, F(X), ast1, ast2, ast12, s, sC, sM]:
print(type(z))
The results of this experiment are as follows:
Expression 






















Gallery of Sourcetrail class diagrams¶
The diagrams in this gallery have been generated via the Sourcetrail opensource crossplatform sourcecode explorer.