Changelog

0.0.3

Date

August 4, 2020

New Features

  • For the datatype of typed directed multi-graphs, this version introduces three different variants of algorithms capable of computing injective partial overlaps between pairs of TDGs: a “direct” aka “generate-and-test”, a “double-pullback embedding (DPE)” and an “implicit” method.

  • All three overlap-finding algorithms have been equipped with detailed data-logging facilities that permit to extract experimental information such as maximal and average runtimes as well as memory consumption.

  • A new GCM2020 supplementary information section in the Gallery of examples explores the utility of the aforementioned three strategies for the special case of rewriting so-called rigid graphs, which may be obtained from TDGs via imposing certain structural constraints.

  • A general engine for curating data from individual overlap-finding experiment runs as well as an I/O-engine for reading and storing both graph data as well as experiment information into human-readable JSON files is introduced.

Breaking changes

  • In order to facilitate the handling of the large amounts of data rendered in individual overlap-finding experiments, a number of auxiliary data classes have been introduced, which in particular form the new output formats of the various methods. The documentation has been updated to reflect these new conventions.

Bug fixes/improvements

  • Minor bug fixes.

0.0.2

Date

July 16, 2020

New Features

  • This version includes a fully functional prototype of a rewriting theory algorithm package for typed directed (multi-) graphs (TDGs). This functionality is now included in the datatypes.py sub-module.

  • An extensive documentation of the new features for TDGs has been added to the Gallery of examples.

  • The TDG-related methods also include a visualization method, which permits to plot TDGs including loops and multi-edges correctly (based upon the pydot package, and in contrast to the methods provided by the networkX package, which is known to collapse loops and multi-edges).

Bug fixes/improvements

  • In preparation for a more in-detail study of the possibilities of optimizing the Z3-based methods, internally all occurrences of free variables in logical formulas are now encoded via the Z3 API FreshConst method (rather than the Const method). Concretely, this will ensure that every free variable in the resulting assertion outputs will be uniquely named.

  • Some alternative Z3 solver tactics have been added in order to experiment with alternative options in terms of memory vs. time consumption performance etc. (with a more thorough array of options to be added in a future version).

  • Minor bug fixes.

0.0.1

Date

June 24, 2020

New Features

  • This is the first official release of the ReSMT module, a Python 3 library aimed at implementing compositional rewriting theory algorithms based upon the Microsoft Z3 Theorem Prover as a computational core. Our approach takes advantage of the Z3 API enumeration sort functionality, which renders scalable performance as needed in practical applications of the rewriting theory algorithms.

  • The implementation strategy is experimented with in the experiments.py module. Since the question of how to utilize Z3 for rewriting-theoretic purposes might be of interest also beyond our present use cases, this module is intended to remain in the final ReSMT module for documentation purposes.

  • A Gallery of examples is included (together with installation instructions providing information on how to install Jupyter and other convenient utilities). The gallery currently contains some illustrations of how to use the experiments.py module.