data Bit
= ...
| Run ( forall m s . MonadSAT s m => m Bit )
the idea was to have clause output as a side effect. I am now convinced that this is a bad idea, and I think it never fully worked.
My motivating use case was fixed-bitwidth numbers with forbidden overflow. With this implementation, overflow acts like an exception (or NaN) - that can never be caught (un-NaN-ed). This makes it impossible to have "zero * overflow = zero".
https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Bit.hs#L60
the idea was to have clause output as a side effect. I am now convinced that this is a bad idea, and I think it never fully worked.
My motivating use case was fixed-bitwidth numbers with forbidden overflow. With this implementation, overflow acts like an exception (or NaN) - that can never be caught (un-NaN-ed). This makes it impossible to have "zero * overflow = zero".
I thinkt this way of overflowing is much better: https://github.com/jwaldmann/ersatz/blob/38327a07774dc85d1ad27e412d2f2569b3d4cd68/tests/Z001.hs#L89