overhaul the formula simplification routines
The current way to implement LTL simplifications has a few issues:
- The number of rules is huge, and the
spot/twaalgos/simplify.cc
file implementing them is the largest all handwritten source files of Spot. Readingdoc/tl/tl.pdf
in parallel is almost mandatory to understand what is being done. - These rules are hard-coded.
- They use nested switches to match the structure of some patterns, sometimes relying on formulas properties. But sometimes we have a set of rules that should only be applied in some context (e.g., star normal form, or rules that apply inside
GF(...)
). These nesting patterns are quite painful to follow, and are often implemented twice for the dual rules. - Some of generic options can also affect the way some rules are applied (sometimes they affect the direction of some rewriting).
- Dealing with n-ary operators is quite painful, especially when multiple rules compete to combine the operands.
All these theses points make it very hard to implement new simplification rules. It's also impossible to test a new simplification rule without implementing it. Finally, adding a new operator to the syntax would have an enormous cost since we would also need to alter many rules to support that new operator.
Our goal is therefore to change the way we do LTL simplifications. We need at least:
-
a DSL to express all our simplification rules in a way that is simple and unambiguous -
the (hopefully) complete list of rules expressed in that language -
a parser for that language -
a function that applies all the reductions on some given formula -
some abstract representation of a set of rules, such that the above function can be implemented efficiently
Once that is done, we should evaluate ways to make it faster. Parsing the list of all rules before the first simplification is likely to incur some overhead. We could try to generate some C++ code from this list at compile time to avoid the parsing at run time, but we would loose the ability to edit the list of rules at run time.
An option would be store the abstract (parsed) representation of the set of rules into some kind of bytecode that can be loaded quickly and used readily without costly syntax checks.
It would be useful if the users of the command-line tools could be allowed to supply their own rules. (This implies that the DSL will need to be documented.)
I suggest keeping the current simplification function around until all of the above is working, so that the result can be compared (if possible). When we are confident that we can switch to the new function, we still need to maintain backward compatibility of the API.