s-falke/kittel-koat — pull request #8 by mmjb (2014-08-18 16:56:31+00:00)
Title: Refactor KoAT to use Maps (corresponding to paper) instead of lists of tuples

This branch contains a major refactoring to make the KoAT implementation match the TACAS'14 paper.

To this end, I've changed the internal representation of transitions systems to (a) a record type ctrs, which stores rules and the start symbol and (b) a record type ctrsobl, which stores a ctrs and maps from rules to cost/complexity (plus a leaf cost for removed rules). This allowed to simplify a lot of code, moving it to something that matches the paper.
As I had to touch most of the existing code, I have adapted the KoAT syntax style to the default Emacs caml-mode/Tuareg style (mostly, this means no intend after let ... in).

In the course of this major refactoring, I have also introduced a number of additional features and fixes:
* A logging facility that allows to watch the proof as it progresses (including time stamps, to see where the time is actually spent)
* The code extracting results Farkas-based polo synthesis is now more stable, and not relying on several lists being in the same order anymore
* The heuristic for separating out parts of the transition system is more robust

I've tested with the examples in cexamples/* that no regressions exist. Runtimes haven't changed in general (i.e., variations under 0.1s), and coefficients for solutions are in general slightly smaller, probably due to reordered constraints in the SMT problem and pure luck.