Hi Simon,
On Sun, Sep 23, 2018 at 5:46 PM Simon Jantsch simon.jantsch@gmail.com wrote:
which makes me believe that simplification is done before removing the operators M and W.
Yes. It has to be in this order because the simplifications can detect patterns that correspond to M or W, and reintroduce these operators...
Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators?
I'm afraid we don't have that. Simplification and unabbrevation are two separate functions, and rewriting those to be a single function would be a lot of work. I've an idea that could improve this specific case, but that isn't like the "simplify with restricted operators" solution you could dream of. See https://gitlab.lrde.epita.fr/spot/spot/issues/362