sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.BitPrecise.BitTricks

Description

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

Synopsis

- fastMinCorrect :: SInt32 -> SInt32 -> SBool
- fastMaxCorrect :: SInt32 -> SInt32 -> SBool
- oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
- conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
- powerOfTwoCorrect :: SWord32 -> SBool
- queries :: IO ()

# Documentation

fastMinCorrect :: SInt32 -> SInt32 -> SBool Source #

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

fastMaxCorrect :: SInt32 -> SInt32 -> SBool Source #

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

oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool Source #

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

conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool Source #

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

powerOfTwoCorrect :: SWord32 -> SBool Source #

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

queries :: IO () Source #

Collection of queries