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 sub-experiment)

  • numReps – an integer denoting the number of repetitions of the sub-experiment

  • expsData – a list of tuples of the form (gAname, gBname), with gAname and gBname the names of TDGs in graphDataFname whose overlaps should be computed

  • maxRunTime – (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 key expName 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 method genTDGfrData to generate the forbidden relation data for the specified forbidden TDG pattern N.

genFRasts(P: resmt.datatypes.Z3TDGspanPredicateTemplate) → None[source]

Method to render the non-DPE assertions generated from the forbidden TDG relations.

genTDGfrData() → None[source]

Method to trigger the forbidden relation search for the given forbidden TDG pattern self.N.

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 nil-element 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 for domG and/or codomG (which type-checks due to the fact that the class Z3TDGtemplate is a subclass of the class Z3TypedDirectedGraph).

Parameters
  • mName – a string encoding the name of the morphism

  • domG – a Z3TypedDirectedGraph instance encoding the domain graph

  • codomG – a Z3TypedDirectedGraph instance encoding the codomain graph

  • vMap – a dictionary encoding the vertex-mapping

  • eMap – a dictionary encoding the edge-mapping

  • 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, {'nil|X':'nil|X', 'nil|Y':'nil|Y'},             {'nil|Z':'nil|Z'})

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 nil-element 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, {'nil|X':'nil|X', 'nil|Y':'nil|Y'}, {'nil|Z':'nil|Z'})
>>> 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 sub-predicate, and moreover assertions are included to ensure that an edge with predicate True also has its endpoints carrying the predicates True.

__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 “sort-compatible”, i.e. encodes a sort-preserving 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 sort-compatible, i.e. if the input graphs do not satisfy this property a priori, one must invoke the .patchNilElements method in order to fix the sort-matching.

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 nil-elements: >>> 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 non-nil 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 of Z3TypedSet instances at initialization of instance of the template class. The input data necessary for TDG templates is comprised of

  1. Sets of vertex- and edge-sorts, and

  2. a dictionary of edge-sort 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 edge-sorts 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), where eSrt is the name of an edge sort, while sSrt and tSrt are the names of the source/target vertex sort names for edges of sort eSrt

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 and circo)

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 sort-compatible if and only if they have precisely the same vertex- and edge-sorts, and if in addition their edge-to-source/target sort “signatures” coincide.

Parameters

gB – a second Z3TypedDirectedGraph instance to compare with

Returns

A boolean value (with True indicating sort-compatibility).

patchNilElements(gB: resmt.datatypes.Z3TypedDirectedGraph) → None

Patch nil-elements for vertex and edge sorts not in original graph.

As an additional effect to merely adding the nil-elements to the vertex and edge sets, the method also updates the source and target functions (s.th. the new nil-edges have source and target as nil-elements 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 nil-element 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 of graphB:

>>> 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 non-embedding 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 and circo)

..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 the Z3 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 vertex-type 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. Source-target 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 “type-signature” in terms of their source- and target-vertex types/

>>> gB = Z3TypedDirectedGraph(S, 'gEmpty', {}, {}, {})

This will render a representation of an empty graph. Special default types are utilized in order to give the nil-elements an invariant type, and the nil-element of the vertex set is both the source and target “vertex” of the nil-edge.

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 edge-sorts 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), where e is the name of an edge, while s and t are the names of the source/target vertices of the edge e

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 and circo)

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 sort-compatible if and only if they have precisely the same vertex- and edge-sorts, and if in addition their edge-to-source/target sort “signatures” coincide.

Parameters

gB – a second Z3TypedDirectedGraph instance to compare with

Returns

A boolean value (with True indicating sort-compatibility).

patchNilElements(gB: resmt.datatypes.Z3TypedDirectedGraph) → None[source]

Patch nil-elements for vertex and edge sorts not in original graph.

As an additional effect to merely adding the nil-elements to the vertex and edge sets, the method also updates the source and target functions (s.th. the new nil-edges have source and target as nil-elements 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 nil-element 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 of graphB:

>>> 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 non-embedding 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 and circo)

..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 the Z3 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 domain

  • codomSet – a Z3TypedSet instance encoding the codomain

  • fData – 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)

f(elName: str) → z3.z3.ExprRef[source]

Retrieve the Z3 value of a function application by domain element name.

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 type setAname+'|'+elSortName may be mapped to constants of type setBname+'|'+elSortName (with additional issues related to nil-carriers 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 in elSortNames)

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 nil-elements)

__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 side-effect of executing the method consists in introducing the necessary definitions of Z3 sorts for the different element sorts and nil-elements for each of the element sorts.

Note

If an empty els dictionary is specified, the method instantiates a Z3 constant nonetheless for a nil-element whose sort is named '_DEFAULT', since fuhnctions must be total in Z3, which is why nil-elements 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 context solv.ctx of solv. 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 and y, the merge of the two is obtained as {**x, **y}.

getEl(elName: str) → z3.z3.ExprRef[source]

Get the Z3 constant associated to an element name.

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 nil-elements.

Given a second Z3TypedSet instance setB, extract the sorts present in setB but not in the original set, and then add extra nil-elements to the original set for each of these extra sorts.

Parameters

setB – a Z3TypedSet instance whose additional sorts should be “patched” into the self insstance (and suitable nil-elements 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 instance

  • domSet – 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)
f(elName: str) → z3.z3.ExprRef[source]

Retrieve the Z3 value of an automorphism application by domain element name.

class resmt.datatypes.Z3TypedSetPredicate(pName: str, domSet: resmt.datatypes.Z3TypedSet)[source]

Bases: object

An assembly of boolean predicates (one per sort-wise 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)
f(elName: str) → z3.z3.BoolRef[source]

Refer to the value of the predicate by element name.

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 instance

  • setB – the second Z3TypedSet instance

  • isMonic – 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 nil-elements 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 non-nil 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 the Z3TypedSet class relies upon the z3.EnumSort functionality of the Z3 API, Z3TypedSetTemplate instances are initialized via 1) issuing a z3.DeclareSort call for each sort of elements, and 2) only explicitly instantiating the nil-elements as Z3 constants for each sort. In consequence, instances of the Z3TypedSetTemplate are useful in situations such as pushout constructions where the concrete non-nil 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 in elSortNames)

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 nil-elements)

__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 side-effect of introducing the necessary definitions of Z3 sorts for the different element sorts and Z3 constants for the nil-elements 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 nil-elements.

Given a second Z3TypedSet instance setB, extract the sorts present in setB but not in the original set, and then add extra nil-elements to the original set for each of these extra sorts.

Parameters

setB – a Z3TypedSet instance whose additional sorts should be “patched” into the self insstance (and suitable nil-elements 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 “generate-and-test”) method, in particular run-times 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 key-valye 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 instance

  • phase – a string (either 'generate' or 'test') for encoding the phase in which the statistics data was collected

Returns

A dictionary with one key-valye pair per entry in self.stats[rKey] as well as a copu in the phase-specific statistics dictionary field self.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 run-ids 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 time-out; in case no time-out occurred, the default value of this entry is “-“

getAverageMemory() → float[source]

Average memory consumption over all runs (including unsat run).

getAverageRuntime() → float[source]

Compute the average run-time (excluding the unsat run).

getMaxMemory(rKey: str) → float[source]

Maximum memory value for a specific run.

Parameters

rKey – the key identifying the solver run in the self.statsData.stats dictionary

Returns

The maximum memory value of the run (in MB).

getOverallMaxMemory() → float[source]

Maximum memory consumption value over all runs.

getTotalRuntime() → float[source]
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 instance

  • gB – a Z3TypedDirectedGraph instance

  • overlaps – a list of overlaps of gA and gB, where each overlap is encoded as a tuple of sets, the first of which encodes the vertex overlaps (in the format (vA, vB) if vA is overlapped with vB), 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 instance

  • idx – 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 of self.gA with self.gB along the overlap self.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 key-valye 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 with fG itself, and with predicates (per vertex/edge in fG) 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 isomorphism-class induced by automorphisms of fG 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 instance

  • gB – a Z3TypedDirectedGraph instance

  • frClist – 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 run

  • A 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 pre-computation 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 double-pullback embedding (DPE) constraints for the input TDGs gA and gB is rendered, so that the computational price for computing the forbidden relation data must only be paid once before a possibly large set of overlap-searching 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 “generate-and-test” 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:

  1. Generation phase: determine all (monic) overlaps without taking into account the forbidden pattern constraints

  2. 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 instance

  • gB – a Z3TypedDirectedGraph instance

  • forbiddenPatternsList – 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” phase

  • a string containing some information on the performance of the Z3 solver runs (such as memory consumption etc.) in the first phase

  • a list of tuples of the form (t, b, gPO), where t is the computation time needed by the Z3 solver to determine the “test phase” computation for the given candidate overlap, b is a Boolean value (where True indicates that the overlap is consistent with the constraints), and where gPO is the pushout graph of the overlap

  • statsistics data on the Z3 solver runs in the “test” phase

  • a 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 utilize z3.EnumSort encodigns for the explicitly specified input TDGs gA and gB, but an implicit encoding for a pushout graph via z3.Const calls) permits to verify “on-the-fly” 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 instance

  • gB – a Z3TypedDirectedGraph instance

  • forbiddenPatternsList – 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 run

  • A 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 instance

  • gB – a Z3TypedDirectedGraph instance

  • PhiData – a tuple of dictionaries encoding vertex- and edge-overlaps (i.e. every element name pair encodes that these elements are in the overlap of gA and gB)

Returns

A triple of data encoding the pushout object, consisting of

  • a dictionary of vertex name: vertex sort entries

  • a dictionary of edge name: edge sort entries

  • a 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 the stDict fields into lists. This defect is fixed via the additional “re-packaging” step performed by the present method.

Parameters

fName – the filename of the JSON input file

Returns

A dictionary of dictionaries, with the top-level dictionary having keys gName, vDict, eDict and stDict (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 instances

  • resultsFname – 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 Log-bar 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 Log-plot with a dotted horizontal line marking the average execution time, and with the last bar (highlighted in a different color) indicating the time until unsat; the plot is saved into a PDF with filename fName.

resmt.experiments.genFrExecTimePlot(cTimes: List[Tuple[float, str]], statsInfo: str, titleStr: str, fName: str) → None[source]

Generate execution time Log-bar 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 Log-plot with a dotted horizontal line marking the average execution time, and with the last bar (highlighted in a different color) indicating the time until unsat; the plot is saved into a PDF with filename fName.

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 until unsat) 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 until unsat) 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 iso-check 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 cardinality m and a set B of cardinality m+n, the exact formula for the number of injective partial overlaps of the two sets is given by

n_{sols} = \sum_{k=0}^m k! \binom{m}{k}\binom{m+n}{k} = (-1)^m U(-m, n+1, -1)\,.

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 log-plot 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()+'/jinja2-templates')

  • plotLayout – (optional) choice of layout option ('2:1' or '1:1'; default: '2:1')

Returns

Renders PDFs plotFN+'.pdf' and plotFN+'-tableaux.pdf with vizualizations of the forbidden relations (individual plots and tableaux of plots, respectively). The latter PDF will then be opened in the system’s default PDF viewer.

visualizations.py

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

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 table

  • width – (optional) a string of the form "x%", with x an integer between 0 and 100 (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 instance

  • drawGraph – (optional) a boolean controlling whether or not to draw the graph via the matplotlib plot commands after instantiation (default: True)

  • writeGraph – (optional) controls whether or not the graph should be written to a file (default: False)

  • fileName – (optional) a filename for the graph, where the extension controls the output format (default: None)

  • gLayout – (optional) a string controlling the graph layout for the interactive display (default: ‘neato’; alternative options are those of GraphViz, e.g. dot, twopi, fdp, sfdp and circo).

Note

The available file-formats for the graph visualizations are those supported by the GraphViz package, i.e. either of the following ones:

bmp canon cgimage cmap cmapx cmapx_np dot dot_json eps exr fig gd gd2 gif gv icns ico imap imap_np ismap jp2 jpe jpeg jpg json json0 mp pct pdf pic pict plain plain-ext png pov ps ps2 psd sgi svg svgz tga tif tiff tk vdx vml vmlz vrml wbmp webp xdot xdot1.2 xdot1.4 xdot_json

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:

Python types of instances generated with the Z3 API

Expression x

type(x)

A = z3.DeclareSort('A')

z3.SortRef

X = z3.Const('X', A)

z3.ExprRef

F = z3.Function('F', A, A)

z3.FuncDeclRef

F(X)

z3.ExprRef

ast1 = z3.ForAll(z3.Const('Y', A), z3.Const('Y', A) == X)

z3.QuantifierRef

ast2 = z3.Exists(z3.Const('Z',A), F(z3.Const('Z',A)) == X)

z3.QuantifierRef

ast12 = z3.And([ast1, ast2])

z3.BoolRef

s = z3.Solver()

z3.Solver

sC = s.check()

z3.CheckSatResult

sM = s.model()

z3.ModelRef