find a way to reduce {b*;r} = (b W r) when r is satisfiable

Commit 11568666 removed the following rules

{b*;r} = b W r
!{b*;r} = !b M !{r}

because it is only true when r is satisifiable, but the code did not check that.

Currently the only way we have to ensure that r is satisifiable is to translate it into an automaton. Doing so seems unlikely to be efficient.

But there are many formulas that we can tell as satisfiable without even translation: for instance any SERE that do not involve &, &&, and false is satisfiable. So maybe each formula could have a Boolean property that tells when it is trivially satisfiable.