4 ms·
That's pretty cool, although it ought to be mentioned that x must be a uint32. Here's a proof: λ> import Data.SBV λ> prove $ do x <- Data.SBV.sWord32 "
by conistonwater 10y ago
That's pretty cool, although it ought to be mentioned that x must be a uint32. Here's a proof:
λ> import Data.SBV
λ> prove $ do x <- Data.SBV.sWord32 "x"; return $ (x * 0xaaaaaaab .< 0x55555556) .== (x `sMod` 3 .== 0)
Q.E.D.
Are you sure it doesn't work for other factors? It seems it works for 7, 9, and 11.
λ> sat $ do [a,b] <- sWord16s ["a", "b"]; forAll_ (\x -> (x * a .< b) <=> (x `sMod` 7 .== 0))
Satisfiable. Model:
a = 28087 :: Word16
b = 9363 :: Word16
λ> sat $ do [a,b] <- sWord16s ["a", "b"]; forAll_ (\x -> (x * a .< b) <=> (x `sMod` 9 .== 0))
Satisfiable. Model:
a = 36409 :: Word16
b = 7282 :: Word16
λ> sat $ do [a,b] <- sWord16s ["a", "b"]; forAll_ (\x -> (x * a .< b) <=> (x `sMod` 11 .== 0))
Satisfiable. Model:
a = 35747 :: Word16
b = 5958 :: Word16
So a is equal to 7^{-1} mod 2^16, and b to ceil((2^16-1)/7), etc.
- panic 10y agoWow, that's really cool! Looks like this is a Haskell library: https://hackage.haskell.org/package/sbv-5.15/docs/Data-SBV.html https://hackage.haskell.org/package/sbv-5.15/docs/Data-SBV.h...
- conistonwater 10y agoYes, it's really good! Makes it feasible to "sat first, ask questions later", especially for bit trickery.
- raphlinus 10y agoDuh, you're right on both counts. It should work for any odd divisor, I was just computing the inverse in a dumb way when I tried out other divisors. And I should have stated u32 wrapping arithmetic.
- im3w1l 10y agoAnd for even divisors you can separate the divisor into a power of two, and an odd part. The odd part is checked as before, and the power of two is checked with an and mask.