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.