{
  "cells": [
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "%matplotlib inline\nfrom IPython.display import SVG, display, Image"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "\n\nAPI experiments\n===============\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Preliminaries: setting up the Jupyter environment\n-------------------------------------------------\n\nIf you have not already done so, please consult the **Installation instructions** chapter of the ``ReSMT`` \\\ndocumentation for  information on how to install the necessary Python version, Python packages and \\\nthe necessary additional shell scripts. You  will also require a local copy of the \\\n**ReSMT GitLab repository**, which may be obtained as follows: ::\n\n    $ git clone https://gitlab.com/nicolasbehr/ReSMT.git <path-to-your-local-folder>\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "A convenient method to experiment with this document consists in starting up a ``Jupyter Lab`` \\\ninstance: navigate to the ``docs/py_and_ipynb_examples`` folder of your local copy of the repository \\\nin a terminal session and execute the command ::\n\n     $ jupyter lab ReSMT-API-experiments.ipynb\n\nThis will open an interactive ``Jupyter`` session of the present notebook.\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Assuming that the current working directory of the Python instance is the aforementioned \\\n``docs/py_and_ipynb_examples`` sub-directory of the ``ReSMT`` package main directory, the package is \\\nloaded as follows:\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "import os\nimport timeit\nimport sys\nsys.path.insert(0, os.path.abspath('../../'))\nimport resmt.datatypes as datatypes\nimport resmt.experiments as experiments\nimport resmt.visualizations as visualizations\n\nimport numpy\nimport networkx as nx\nimport z3"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "<div class=\"alert alert-info\"><h4>Note</h4><p>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 ::\n\n    $ os.chdir('/local/path/to/ReSMT/docs/py_and_ipynb_examples')</p></div>\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Finding injective partial overlaps of finite sets\n-------------------------------------------------\n\nAs a benchmark and first set of experiments with the ``ReSMT`` API, consider the algorithmic task of determining\nall *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$:\n\n![](images/numSolsInjSetOverlaps.svg)\n\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The above plot may be rendered (yielding both a PDF and an SVG version) via the following method call:\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "experiments.render3DplotsOfInjPartialObverlaps(10, 10, 'images/numSolsInjSetOverlaps')"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Let us instantiate a Z3 solver,\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "import z3\nS = z3.Solver()"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "and utilize some of the methods provided by the ``ReSMT`` API to compute the number\nof injective partial overlaps for some (small) finite sets:\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup\n\nnAels = 2\nnBels = 3\n\nS.reset()  # reset the solver state to an empty state\nexperiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The procedure will render a bar log-plot of the following form:\n\n![](images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=2_nB=3.svg)\n\n\nNote that further information on the experiment may be found in a log file called ``experiments.log``. IIn order to\nillustrate the\nscalability of the code, we present\nbelow a number of further examples (executed on a\ndesktop computer running *macos Catalina* with an *2.30GHz Intel(R) Core(TM) i7-3615QM CPU* and *16 GB* of\nRAM).\n\n<div class=\"alert alert-info\"><h4>Note</h4><p>The plots of execution times reflext the Z3-based algorithm parts only, yet a considerable \\\n    amount of time is needed in addition by the ``matplotlib`` routines to render the various plots!</p></div>\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup\n\nnAels = 3\nnBels = 4\n\nS.reset()  # reset the solver state to an empty state\nexperiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=4.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup\n\nnAels = 3\nnBels = 5\n\nS.reset()  # reset the solver state to an empty state\nexperiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=5.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup\n\nnAels = 4\nnBels = 5\n\nS.reset()  # reset the solver state to an empty state\nexperiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=4_nB=5.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "titleStrExtra = 'Z3-4.8.8-python-3.8.2'  # some information on the current setup\n\nnAels = 3\nnBels = 6\n\nS.reset()  # reset the solver state to an empty state\nexperiments.genSetOverlapExperiment(S, nAels, nBels, titleStrExtra, 'images/');"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/overlaps-(Z3-4.8.8-python-3.8.2)_nA=3_nB=6.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Forbidden relations for set patterns\n------------------------------------\nA quintessential role in practical computations with ``ReSMT`` is played by so-called *forbidden relations*.\nIntuitively, when constructing overlaps of objects (e.g. in rule compositions), if the pushout of the overlap\nshould respect a global constraint expressed in terms of *forbidden patterns*, it is possible to formulate the\ncompliance of the pushout with this constraints as a non-embedding condition of forbidden relations into the\ncandidate overlap. This approach permits to catch \"illegal\" overlaps already at the time of the search for possible\noverlaps, which poses a considerable computational advantage especially for our Z3-based methods. Concretely,\ndetermining *forbidden relations* from a given set of *forbidden patterns* requires the following algorithmic steps:\n\n1. Determine decompositions of the forbidden patterns as pushouts of monic spans, where in addition each object in\nthe span must not be isomorphic to the forbidden pattern (i.e. must be proper subobjects)\n\n2. Quotient the resulting candidate forbidden relations by isomorphisms that are induced from isomorphisms of the underlying forbidden pattern objects.\n\nIt is precisely the latter step that will in practical examples harness the full utility of the Z3-based\nalgorithms, which are by construction invariant under isomorphisms. For illustration, the ``examples.py`` module\ncontains methods to experiment with a Z3-based implementation of the above forbidden relation search for the case\nof forbidden patterns given by finite sets. Precisely to provide some intuitions on the amount of computation time\nthat would be necessary in order to determine isomorphisms purely in Z3, the methods contain a **non-optimized** (\ni.e. brute force) isomorphism search. As the following experiments for concrete numbers of vertices in teh\nforbidden patterns demonstrate, with increasing complexity of the set of forbidden relations (visualized below as\ntwo-tier diagrams with dashed lines indicating the overlap structures), the number of isomorphisms to quotient\ngrows rather rapidly.\n\n<div class=\"alert alert-info\"><h4>Note</h4><p>In the isomorphism quotient routines implemented in the main ReSMT forbidden relation \\\n    search method, we of course utilize a more optimised isomorphism check method, i.e. by pre-\\\n    checking the relevant numbers of vertices and edges of each type! The variant presented here \\\n    serves thus mainly the purpose of an easy to scale test method for larger sets of assertions \\\n    and the respective model search performance and execution times.</p></div>\n\n**Case of three-vertex forbidden pattern**\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "workDir = os.getcwd()+'/images/'\ntemplateDir = os.getcwd()+'/jinja2-templates'\n\nnEls = 3\n\nFRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])\n\ntotalTime = numpy.round(sum([x[0] for x in execTimes]), 8)\ntitleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) '\\\n           + 'for n = %s (total time: %ss)' % (nEls, totalTime)\nfN = 'images/fr-n=%s-Z3-timings' % nEls\nstatStr = str(solverStats)[1:-1]\nexperiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)\n\nplotFN = 'neq%s-frPlots' % nEls\nexperiments.renderVisualization(FRs, workDir, plotFN, templateDir)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/fr-n=3-Z3-timings.svg)\n\n\n![](images/neq3-frPlots-tableaux.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "**Case of four-vertex forbidden pattern**\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "workDir = os.getcwd()+'/images/'\ntemplateDir = os.getcwd()+'/jinja2-templates'\n\nnEls = 4\n\nFRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])\n\ntotalTime = numpy.round(sum([x[0] for x in execTimes]), 8)\ntitleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \\\n           + 'for n = %s (total time: %ss)' % (nEls, totalTime)\nfN = 'images/fr-n=%s-Z3-timings' % nEls\nstatStr = str(solverStats)[1:-1]\nexperiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)\n\nplotFN = 'neq%s-frPlots' % nEls\nexperiments.renderVisualization(FRs, workDir, plotFN, templateDir)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/fr-n=4-Z3-timings.svg)\n\n\n![](images/neq4-frPlots-tableaux.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "**Case of five-vertex forbidden pattern**\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "workDir = os.getcwd()+'/images/'\ntemplateDir = os.getcwd()+'/jinja2-templates'\n\nnEls = 5\n\nFRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])\n\ntotalTime = numpy.round(sum([x[0] for x in execTimes]), 8)\ntitleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \\\n           + 'for n = %s (total time: %ss)' % (nEls, totalTime)\nfN = 'images/fr-n=%s-Z3-timings' % nEls\nstatStr = str(solverStats)[1:-1]\nexperiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)\n\nplotFN = 'neq%s-frPlots' % nEls\nexperiments.renderVisualization(FRs, workDir, plotFN, templateDir)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/fr-n=5-Z3-timings.svg)\n\n\n![](images/neq5-frPlots-tableaux.svg)\n\n\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "**Case of six-vertex forbidden pattern**\n\n\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "collapsed": false
      },
      "outputs": [],
      "source": [
        "workDir = os.getcwd()+'/images/'\ntemplateDir = os.getcwd()+'/jinja2-templates'\n\nnEls = 6\n\n\nFRs, execTimes, solverStats = experiments.generateForbiddenRelations(['n%s' % i for i in range(1, nEls+1)])\n\ntotalTime = numpy.round(sum([x[0] for x in execTimes]), 8)\ntitleStr = 'Forbidden relation search (Python-3.8.2, Z3-4.8.8) ' \\\n           + 'for n = %s (total time: %ss)' % (nEls, totalTime)\nfN = 'images/fr-n=%s-Z3-timings' % nEls\nstatStr = str(solverStats)[1:-1]\nexperiments.genFrExecTimePlot(execTimes, statStr, titleStr, fN)\n\nplotFN = 'neq%s-frPlots' % nEls\nexperiments.renderVisualization(FRs, workDir, plotFN, templateDir)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "![](images/fr-n=6-Z3-timings.svg)\n\n\n![](images/neq6-frPlots-tableaux.svg)\n\n\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.8.2"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}