search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
244 stars 34 forks source link

`SInteger` and `sbvTestBit` don't play nice #84

Closed TomMD closed 10 years ago

TomMD commented 10 years ago

Observe:

SAT.sat $ SAT.forSome ["x"] (\i -> SAT.sbvTestBit i 4)
*** Exception: SBV.SMTLib2: Unsupported operation on unbounded integers: s0 & s1

Intentional or not, it appears SInteger is not supported by sbvTestBit. If this is expected then I can submit a documentation patch. If not then.. well... bug!

LeventErkok commented 10 years ago

This is a "known" shortcoming.. Unfortunately, SMT-Lib does not support bit-wise operations for unbounded integers (for good reason); while Haskell fully does. So, there's a tension between what's possible and what's actually supported. For instance, the following doesn't work either:

sat $ \x y -> (x .&. y .== (x::SInteger))

for pretty much the same reason. So, we're bound by the class hierarchy in Haskell not quite nicely matching up with what SMT-Lib understands.

(Note that this is the same issue with Cryptols finite/infinite type variables; which is similarly problematic. But I digress.)

The right thing to do is to actually have two classes: FiniteBits and Bits, I suppose; and only allow these operations on FiniteBits members. (And obviously do not make Integer and instance of FiniteBits.) But that's a whole another can of worms.

I'd be willing to entertain other ideas if you can come up with a reasonable design to avoid such anomalies.