API experiments

Preliminaries: setting up the Jupyter environment

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

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

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

$ jupyter lab ReSMT-API-experiments.ipynb

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

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

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

import numpy
import networkx as nx
import z3

Note

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

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

Finding injective partial overlaps of finite sets

As a benchmark and first set of experiments with the ReSMT API, consider the algorithmic task of determining all injective partial overlaps of two finite sets. Given a set A of cardinality m and a set B of cardinality m+n (with m,n\in \mathbb{Z}_{\geq} some non-negative integers), the bar log-plot below displays these numbers for m,n=0,\ldots,10:

../_images/numSolsInjSetOverlaps.svg

The above plot may be rendered (yielding both a PDF and an SVG version) via the following method call:

experiments.render3DplotsOfInjPartialObverlaps(10, 10, 'images/numSolsInjSetOverlaps')

Let us instantiate a Z3 solver,

import z3
S = z3.Solver()

and utilize some of the methods provided by the ReSMT API to compute the number of injective partial overlaps for some (small) finite sets:

titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup

nAels = 2
nBels = 3

S.reset()  # reset the solver state to an empty state
experiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');

The procedure will render a bar log-plot of the following form:

../_images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=2_nB=3.svg

Note that further information on the experiment may be found in a log file called experiments.log. IIn order to illustrate the scalability of the code, we present below a number of further examples (executed on a desktop computer running macos Catalina with an 2.30GHz Intel(R) Core(TM) i7-3615QM CPU and 16 GB of RAM).

Note

The plots of execution times reflext the Z3-based algorithm parts only, yet a considerable amount of time is needed in addition by the matplotlib routines to render the various plots!

titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup

nAels = 3
nBels = 4

S.reset()  # reset the solver state to an empty state
experiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');
../_images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=4.svg
titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup

nAels = 3
nBels = 5

S.reset()  # reset the solver state to an empty state
experiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');
../_images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=5.svg
titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup

nAels = 4
nBels = 5

S.reset()  # reset the solver state to an empty state
experiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');
../_images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=4_nB=5.svg
titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup

nAels = 3
nBels = 6

S.reset()  # reset the solver state to an empty state
experiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');
../_images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=6.svg

Forbidden relations for set patterns

A quintessential role in practical computations with ReSMT is played by so-called forbidden relations. Intuitively, when constructing overlaps of objects (e.g. in rule compositions), if the pushout of the overlap should respect a global constraint expressed in terms of forbidden patterns, it is possible to formulate the compliance of the pushout with this constraints as a non-embedding condition of forbidden relations into the candidate overlap. This approach permits to catch “illegal” overlaps already at the time of the search for possible overlaps, which poses a considerable computational advantage especially for our Z3-based methods. Concretely, determining forbidden relations from a given set of forbidden patterns requires the following algorithmic steps:

1. Determine decompositions of the forbidden patterns as pushouts of monic spans, where in addition each object in the span must not be isomorphic to the forbidden pattern (i.e. must be proper subobjects)

  1. Quotient the resulting candidate forbidden relations by isomorphisms that are induced from isomorphisms of the underlying forbidden pattern objects.

It is precisely the latter step that will in practical examples harness the full utility of the Z3-based algorithms, which are by construction invariant under isomorphisms. For illustration, the examples.py module contains methods to experiment with a Z3-based implementation of the above forbidden relation search for the case of forbidden patterns given by finite sets. Precisely to provide some intuitions on the amount of computation time that would be necessary in order to determine isomorphisms purely in Z3, the methods contain a non-optimized ( i.e. brute force) isomorphism search. As the following experiments for concrete numbers of vertices in teh forbidden patterns demonstrate, with increasing complexity of the set of forbidden relations (visualized below as two-tier diagrams with dashed lines indicating the overlap structures), the number of isomorphisms to quotient grows rather rapidly.

Note

In the isomorphism quotient routines implemented in the main ReSMT forbidden relation search method, we of course utilize a more optimised isomorphism check method, i.e. by pre-checking the relevant numbers of vertices and edges of each type! The variant presented here serves thus mainly the purpose of an easy to scale test method for larger sets of assertions and the respective model search performance and execution times.

Case of three-vertex forbidden pattern

workDir = os.getcwd()+'/images/'
templateDir = os.getcwd()+'/jinja2-templates'

nEls = 3

FRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])

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

plotFN = 'neq%s-frPlots' % nEls
experiments.renderVisualization(FRs, workDir, plotFN, templateDir)
../_images/fr-n=3-Z3-timings.svg../_images/neq3-frPlots-tableaux.svg

Case of four-vertex forbidden pattern

workDir = os.getcwd()+'/images/'
templateDir = os.getcwd()+'/jinja2-templates'

nEls = 4

FRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])

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

plotFN = 'neq%s-frPlots' % nEls
experiments.renderVisualization(FRs, workDir, plotFN, templateDir)
../_images/fr-n=4-Z3-timings.svg../_images/neq4-frPlots-tableaux.svg

Case of five-vertex forbidden pattern

workDir = os.getcwd()+'/images/'
templateDir = os.getcwd()+'/jinja2-templates'

nEls = 5

FRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])

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

plotFN = 'neq%s-frPlots' % nEls
experiments.renderVisualization(FRs, workDir, plotFN, templateDir)
../_images/fr-n=5-Z3-timings.svg../_images/neq5-frPlots-tableaux.svg

Case of six-vertex forbidden pattern

workDir = os.getcwd()+'/images/'
templateDir = os.getcwd()+'/jinja2-templates'

nEls = 6


FRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])

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

plotFN = 'neq%s-frPlots' % nEls
experiments.renderVisualization(FRs, workDir, plotFN, templateDir)
../_images/fr-n=6-Z3-timings.svg../_images/neq6-frPlots-tableaux.svg

Gallery generated by Sphinx-Gallery