-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.BitPrecise.BitTricks
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Checks the correctness of a few tricks from the large collection found in:
--      <http://graphics.stanford.edu/~seander/bithacks.html>
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.BitPrecise.BitTricks where

import Data.SBV

-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
fastMinCorrect :: SInt32 -> SInt32 -> SBool
fastMinCorrect :: SInt32 -> SInt32 -> SBool
fastMinCorrect SInt32
x SInt32
y = SInt32
m forall a. EqSymbolic a => a -> a -> SBool
.== SInt32
fm
  where m :: SInt32
m  = forall a. Mergeable a => SBool -> a -> a -> a
ite (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y) SInt32
x SInt32
y
        fm :: SInt32
fm = SInt32
y forall a. Bits a => a -> a -> a
`xor` ((SInt32
x forall a. Bits a => a -> a -> a
`xor` SInt32
y) forall a. Bits a => a -> a -> a
.&. (-(forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y))));

-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
fastMaxCorrect :: SInt32 -> SInt32 -> SBool
fastMaxCorrect :: SInt32 -> SInt32 -> SBool
fastMaxCorrect SInt32
x SInt32
y = SInt32
m forall a. EqSymbolic a => a -> a -> SBool
.== SInt32
fm
  where m :: SInt32
m  = forall a. Mergeable a => SBool -> a -> a -> a
ite (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y) SInt32
y SInt32
x
        fm :: SInt32
fm = SInt32
x forall a. Bits a => a -> a -> a
`xor` ((SInt32
x forall a. Bits a => a -> a -> a
`xor` SInt32
y) forall a. Bits a => a -> a -> a
.&. (-(forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y))));

-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
oppositeSignsCorrect SInt32
x SInt32
y = SBool
r forall a. EqSymbolic a => a -> a -> SBool
.== SBool
os
  where r :: SBool
r  = (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
0 SBool -> SBool -> SBool
.&& SInt32
y forall a. OrdSymbolic a => a -> a -> SBool
.>= SInt32
0) SBool -> SBool -> SBool
.|| (SInt32
x forall a. OrdSymbolic a => a -> a -> SBool
.>= SInt32
0 SBool -> SBool -> SBool
.&& SInt32
y forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
0)
        os :: SBool
os = (SInt32
x forall a. Bits a => a -> a -> a
`xor` SInt32
y) forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
0

-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
conditionalSetClearCorrect SBool
f SWord32
m SWord32
w = SWord32
r forall a. EqSymbolic a => a -> a -> SBool
.== SWord32
r'
  where r :: SWord32
r  = forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
f (SWord32
w forall a. Bits a => a -> a -> a
.|. SWord32
m) (SWord32
w forall a. Bits a => a -> a -> a
.&. forall a. Bits a => a -> a
complement SWord32
m)
        r' :: SWord32
r' = SWord32
w forall a. Bits a => a -> a -> a
`xor` ((-(forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf SBool
f) forall a. Bits a => a -> a -> a
`xor` SWord32
w) forall a. Bits a => a -> a -> a
.&. SWord32
m);

-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>
powerOfTwoCorrect :: SWord32 -> SBool
powerOfTwoCorrect :: SWord32 -> SBool
powerOfTwoCorrect SWord32
v = SBool
f forall a. EqSymbolic a => a -> a -> SBool
.== SBool
s
  where f :: SBool
f = (SWord32
v forall a. EqSymbolic a => a -> a -> SBool
./= SWord32
0) SBool -> SBool -> SBool
.&& ((SWord32
v forall a. Bits a => a -> a -> a
.&. (SWord32
vforall a. Num a => a -> a -> a
-SWord32
1)) forall a. EqSymbolic a => a -> a -> SBool
.== SWord32
0);
        powers :: [Word32]
        powers :: [Word32]
powers = forall a b. (a -> b) -> [a] -> [b]
map ((Word32
2::Word32)forall a b. (Num a, Integral b) => a -> b -> a
^) [(Word32
0::Word32) .. Word32
31]
        s :: SBool
s = forall a. (a -> SBool) -> [a] -> SBool
sAny (SWord32
v forall a. EqSymbolic a => a -> a -> SBool
.==) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. SymVal a => a -> SBV a
literal [Word32]
powers

-- | Collection of queries
queries :: IO ()
queries :: IO ()
queries =
  let check :: Provable a => String -> a -> IO ()
      check :: forall a. Provable a => String -> a -> IO ()
check String
w a
t = do String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ String
"Proving " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
w forall a. [a] -> [a] -> [a]
++ String
": "
                     forall a. Show a => a -> IO ()
print forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Provable a => a -> IO ThmResult
prove a
t
  in do forall a. Provable a => String -> a -> IO ()
check String
"Fast min             " SInt32 -> SInt32 -> SBool
fastMinCorrect
        forall a. Provable a => String -> a -> IO ()
check String
"Fast max             " SInt32 -> SInt32 -> SBool
fastMaxCorrect
        forall a. Provable a => String -> a -> IO ()
check String
"Opposite signs       " SInt32 -> SInt32 -> SBool
oppositeSignsCorrect
        forall a. Provable a => String -> a -> IO ()
check String
"Conditional set/clear" SBool -> SWord32 -> SWord32 -> SBool
conditionalSetClearCorrect
        forall a. Provable a => String -> a -> IO ()
check String
"PowerOfTwo           " SWord32 -> SBool
powerOfTwoCorrect