-----------------------------------------------------------------------------
-- |
-- 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 SInt32 -> SInt32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInt32
fm
  where m :: SInt32
m  = SBool -> SInt32 -> SInt32 -> SInt32
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInt32
x SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y) SInt32
x SInt32
y
        fm :: SInt32
fm = SInt32
y SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
`xor` ((SInt32
x SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
`xor` SInt32
y) SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
.&. (-(SBool -> SInt32
forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (SInt32
x SInt32 -> SInt32 -> SBool
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 SInt32 -> SInt32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInt32
fm
  where m :: SInt32
m  = SBool -> SInt32 -> SInt32 -> SInt32
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInt32
x SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
y) SInt32
y SInt32
x
        fm :: SInt32
fm = SInt32
x SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
`xor` ((SInt32
x SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
`xor` SInt32
y) SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
.&. (-(SBool -> SInt32
forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (SInt32
x SInt32 -> SInt32 -> SBool
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 SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool
os
  where r :: SBool
r  = (SInt32
x SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
0 SBool -> SBool -> SBool
.&& SInt32
y SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInt32
0) SBool -> SBool -> SBool
.|| (SInt32
x SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInt32
0 SBool -> SBool -> SBool
.&& SInt32
y SInt32 -> SInt32 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInt32
0)
        os :: SBool
os = (SInt32
x SInt32 -> SInt32 -> SInt32
forall a. Bits a => a -> a -> a
`xor` SInt32
y) SInt32 -> SInt32 -> SBool
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 SWord32 -> SWord32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord32
r'
  where r :: SWord32
r  = SBool -> SWord32 -> SWord32 -> SWord32
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
f (SWord32
w SWord32 -> SWord32 -> SWord32
forall a. Bits a => a -> a -> a
.|. SWord32
m) (SWord32
w SWord32 -> SWord32 -> SWord32
forall a. Bits a => a -> a -> a
.&. SWord32 -> SWord32
forall a. Bits a => a -> a
complement SWord32
m)
        r' :: SWord32
r' = SWord32
w SWord32 -> SWord32 -> SWord32
forall a. Bits a => a -> a -> a
`xor` ((-(SBool -> SWord32
forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf SBool
f) SWord32 -> SWord32 -> SWord32
forall a. Bits a => a -> a -> a
`xor` SWord32
w) SWord32 -> SWord32 -> SWord32
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 SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool
s
  where f :: SBool
f = (SWord32
v SWord32 -> SWord32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SWord32
0) SBool -> SBool -> SBool
.&& ((SWord32
v SWord32 -> SWord32 -> SWord32
forall a. Bits a => a -> a -> a
.&. (SWord32
vSWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
-SWord32
1)) SWord32 -> SWord32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord32
0);
        powers :: [Word32]
        powers :: [Word32]
powers = (Word32 -> Word32) -> [Word32] -> [Word32]
forall a b. (a -> b) -> [a] -> [b]
map ((Word32
2::Word32)Word32 -> Word32 -> Word32
forall a b. (Num a, Integral b) => a -> b -> a
^) [(Word32
0::Word32) .. Word32
31]
        s :: SBool
s = (SWord32 -> SBool) -> [SWord32] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAny (SWord32
v SWord32 -> SWord32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==) ([SWord32] -> SBool) -> [SWord32] -> SBool
forall a b. (a -> b) -> a -> b
$ (Word32 -> SWord32) -> [Word32] -> [SWord32]
forall a b. (a -> b) -> [a] -> [b]
map Word32 -> SWord32
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 :: String -> a -> IO ()
check String
w a
t = do String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Proving " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": "
                     ThmResult -> IO ()
forall a. Show a => a -> IO ()
print (ThmResult -> IO ()) -> IO ThmResult -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove a
t
  in do String -> (SInt32 -> SInt32 -> SBool) -> IO ()
forall a. Provable a => String -> a -> IO ()
check String
"Fast min             " SInt32 -> SInt32 -> SBool
fastMinCorrect
        String -> (SInt32 -> SInt32 -> SBool) -> IO ()
forall a. Provable a => String -> a -> IO ()
check String
"Fast max             " SInt32 -> SInt32 -> SBool
fastMaxCorrect
        String -> (SInt32 -> SInt32 -> SBool) -> IO ()
forall a. Provable a => String -> a -> IO ()
check String
"Opposite signs       " SInt32 -> SInt32 -> SBool
oppositeSignsCorrect
        String -> (SBool -> SWord32 -> SWord32 -> SBool) -> IO ()
forall a. Provable a => String -> a -> IO ()
check String
"Conditional set/clear" SBool -> SWord32 -> SWord32 -> SBool
conditionalSetClearCorrect
        String -> (SWord32 -> SBool) -> IO ()
forall a. Provable a => String -> a -> IO ()
check String
"PowerOfTwo           " SWord32 -> SBool
powerOfTwoCorrect