23 Sep
2018
23 Sep
'18
7:27 p.m.
Hi Simon,
On Sun, Sep 23, 2018 at 5:46 PM Simon Jantsch <simon.jantsch(a)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
--
Alexandre Duret-Lutz