    -----------------------------------------------------------------------------
    -- |
    -- 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 x :: SInt32
    x y :: 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 x :: SInt32
    x y :: 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 x :: SInt32
    x y :: 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
    .< 0 SBool -> SBool -> SBool
    .&& SInt32
    y SInt32 -> SInt32 -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 0) SBool -> SBool -> SBool
    .|| (SInt32
    x SInt32 -> SInt32 -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 0 SBool -> SBool -> SBool
    .&& SInt32
    y SInt32 -> SInt32 -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< 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
    .< 0

    -- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>
    conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
    conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
    conditionalSetClearCorrect f :: SBool
    f m :: SWord32
    m w :: 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 v :: 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
    ./= 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
    -1)) SWord32 -> SWord32 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 0);
            powers :: [Word32]
            powers :: [Word32]
    powers = (Word32 -> Word32) -> [Word32] -> [Word32]
    forall a b. (a -> b) -> [a] -> [b]
    map ((2::Word32)Word32 -> Word32 -> Word32
    forall a b. (Num a, Integral b) => a -> b -> a
    ^) [(0::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 w :: String
    w t :: a
    t = do String -> IO ()
    putStr (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "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]
    ++ ": "
                         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 "Fast min             " SInt32 -> SInt32 -> SBool
    fastMinCorrect
            String -> (SInt32 -> SInt32 -> SBool) -> IO ()
    forall a. Provable a => String -> a -> IO ()
    check "Fast max             " SInt32 -> SInt32 -> SBool
    fastMaxCorrect
            String -> (SInt32 -> SInt32 -> SBool) -> IO ()
    forall a. Provable a => String -> a -> IO ()
    check "Opposite signs       " SInt32 -> SInt32 -> SBool
    oppositeSignsCorrect
            String -> (SBool -> SWord32 -> SWord32 -> SBool) -> IO ()
    forall a. Provable a => String -> a -> IO ()
    check "Conditional set/clear" SBool -> SWord32 -> SWord32 -> SBool
    conditionalSetClearCorrect
            String -> (SWord32 -> SBool) -> IO ()
    forall a. Provable a => String -> a -> IO ()
    check "PowerOfTwo           " SWord32 -> SBool
    powerOfTwoCorrect