in Satchmo, I have "non-overflowing" numbers, cf. https://hackage.haskell.org/package/satchmo-2.9.9.3/docs/Satchmo-Binary-Op-Fixed.html where the implementation emits extra clauses that assert that overflow does not happen. This is useful because it gives a correct implementation of numbers (QF_NIA in STMLIB speak) It is of course not complete (we might miss solutions that need larger bit width).
Another option to get correct implementation of numbers is to increase the bit width as necessary:
width of "x+y" equals 1 + max (width x)(width y), etc. but this might lead to huge formulas quickly.
With applications in termination analysis (implemented with satchmo) we found that fixed bit width is better.
We cannot emit extra assertions in Ersatz, because we construct a pure formula. For a while I thought this should be hacked (internally, we can do IO/effects in the realization of observable sharing) but now I think this is wrong:
it would need an addition to ersatz internals,
that looks ugly,
it destroys the mathematical model by introducing side effects.
I now think the correct Ersatz representation is a type like
data Fixed3 = Fixed3 { contents :: [Bit] , overflow :: Bit }
with the semantics: if overflow is set, then this is not a number (and contents is irrelevant).
The type's Num instance will compute and propagate overflows. Multiplication by zero
could even ignore them.
(note to self, and implementation plan)
in Satchmo, I have "non-overflowing" numbers, cf. https://hackage.haskell.org/package/satchmo-2.9.9.3/docs/Satchmo-Binary-Op-Fixed.html where the implementation emits extra clauses that assert that overflow does not happen. This is useful because it gives a correct implementation of numbers (QF_NIA in STMLIB speak) It is of course not complete (we might miss solutions that need larger bit width). Another option to get correct implementation of numbers is to increase the bit width as necessary: width of "x+y" equals 1 + max (width x)(width y), etc. but this might lead to huge formulas quickly. With applications in termination analysis (implemented with satchmo) we found that fixed bit width is better.
We cannot emit extra assertions in Ersatz, because we construct a pure formula. For a while I thought this should be hacked (internally, we can do IO/effects in the realization of observable sharing) but now I think this is wrong:
I now think the correct Ersatz representation is a type like
with the semantics: if
overflowis set, then this is not a number (andcontentsis irrelevant). The type's Num instance will compute and propagate overflows. Multiplication by zero could even ignore them.related: #19 #21