ltlsynt trivial symplifications
There are a few trivial simplification we could do in ltlsynt to reduce the number of atomic propositions it has to deal with. I'm pretty sure I've seen at least the first one in some Strix paper, but I cannot point to the correct paper at the moment.
- If the specification φ contains an output atomic proposition α that always has the same polarity, then we can simply decide that this is the value our controller will always output, and we can simplify φ accordingly.
- If the specification contains a pattern such a G(α
↔ β) where α is an output atomic proposition, and β is another atomic proposition, then we can remove this pattern by replacing α by β, and then create the output signal for α only while encoding the controller.
The later idea can also work with G(α XOR β). I'm thinking that maybe the synthesis_info structure should have an extra field that maps atomic proposition to constants (to implement the first point) or to another literal (second point).