August 4, 2020
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.
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.
Minor bug fixes.
July 16, 2020
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
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
pydotpackage, and in contrast to the methods provided by the
networkXpackage, which is known to collapse loops and multi-edges).
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
FreshConstmethod (rather than the
Constmethod). Concretely, this will ensure that every free variable in the resulting assertion outputs will be uniquely named.
Z3solver 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.
June 24, 2020
This is the first official release of the
Python 3library aimed at implementing compositional rewriting theory algorithms based upon the Microsoft Z3 Theorem Prover as a computational core. Our approach takes advantage of the
Z3API 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.pymodule. Since the question of how to utilize
Z3for rewriting-theoretic purposes might be of interest also beyond our present use cases, this module is intended to remain in the final
ReSMTmodule 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