Data.SBV.Plugin.Examples.BitTricks

Checks the correctness of a few tricks from the large collection found in: https://graphics.stanford.edu/~seander/bithacks.html

Documentation

elem :: Eq a => a -> [a] -> Bool

SBVPlugin can only see definitions in the current module. So we define elem ourselves.

oneIf :: Num a => Bool -> a

Returns 1 if bool is True

fastMinCorrect :: Proved (Int -> Int -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax

fastMaxCorrect :: Proved (Int -> Int -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax

oppositeSignsCorrect :: Proved (Int -> Int -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns

conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching

powerOfTwoCorrect :: Proved (Word32 -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2

maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge

roundPowerOfTwoCorrect :: Proved (Word32 -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2

zeroInWord :: Proved (Word32 -> Bool)

Formalizes https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord