sbvPlugin-0.5: Formally prove properties of Haskell programs using SBV/SMT

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Plugin.Examples.BitTricks

Description

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

Synopsis

Documentation

oneIf :: Num a => Bool -> a Source

Returns 1 if bool is True

fastMinCorrect :: Int -> Int -> Bool Source

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

fastMaxCorrect :: Int -> Int -> Bool Source

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

oppositeSignsCorrect :: Int -> Int -> Bool Source

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

conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool Source

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

powerOfTwoCorrect :: Word32 -> Bool Source

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