    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.BitPrecise.MultMask
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- An SBV solution to the bit-precise puzzle of shuffling the bits in a
    -- 64-bit word in a custom order. The idea is to take a 64-bit value:
    --
    --    @1.......2.......3.......4.......5.......6.......7.......8.......@
    --
    -- And turn it into another 64-bit value, that looks like this:
    --
    --    @12345678........................................................@
    --
    -- We do not care what happens to the bits that are represented by dots. The
    -- problem is to do this with one mask and one multiplication.
    --
    -- Apparently this operation has several applications, including in programs
    -- that play chess of all things. We use SBV to find the appropriate mask and
    -- the multiplier.
    --
    -- Note that this is an instance of the program synthesis problem, where
    -- we "fill in the blanks" given a certain skeleton that satisfy a certain
    -- property, using quantified formulas.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.BitPrecise.MultMask where

    import Data.SBV
    import Data.SBV.Control

    -- | Find the multiplier and the mask as described. We have:
    --
    -- >>> maskAndMult
    -- Satisfiable. Model:
    --   mask = 0x8080808080808080 :: Word64
    --   mult = 0x0002040810204081 :: Word64
    --
    -- That is, any 64 bit value masked by the first and multiplied by the second
    -- value above will have its bits at positions @[7,15,23,31,39,47,55,63]@ moved
    -- to positions @[56,57,58,59,60,61,62,63]@ respectively.
    --
    -- NB. Depending on your z3 version, you might also get the following
    -- multiplier as the result: 0x8202040810204081. That value works just fine as well!
    --
    -- NB. Note the custom call to z3 with a specific tactic. A simple call to z3 unfortunately
    -- does not terminate quickly.
    maskAndMult :: IO ()
    maskAndMult :: IO ()
    maskAndMult = SatResult -> IO ()
    forall a. Show a => a -> IO ()
    print (SatResult -> IO ()) -> IO SatResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SMTConfig -> SymbolicT IO () -> IO SatResult
    forall a. Satisfiable a => SMTConfig -> a -> IO SatResult
    satWith SMTConfig
    z3{printBase=16} SymbolicT IO ()
    find
      where find :: SymbolicT IO ()
    find = do -- Magic incantation to make the test go fast. See <http://github.com/Z3Prover/z3/issues/5660> for details.
                      SMTOption -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
    setOption (SMTOption -> SymbolicT IO ()) -> SMTOption -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> [String] -> SMTOption
    OptionKeyword String
    ":smt.ematching" [String
    "false"]

                      SBV Word64
    mask <- String -> Symbolic (SBV Word64)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "mask"
                      SBV Word64
    mult <- String -> Symbolic (SBV Word64)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "mult"
                      (Forall Any Word64 -> SBool) -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Word64 -> SBool) -> SymbolicT IO ())
    -> (Forall Any Word64 -> SBool) -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SBV Word64
    inp) -> let res :: SBV Word64
    res = (SBV Word64
    mask SBV Word64 -> SBV Word64 -> SBV Word64
    forall a. Bits a => a -> a -> a
    .&. SBV Word64
    inp) SBV Word64 -> SBV Word64 -> SBV Word64
    forall a. Num a => a -> a -> a
    * (SBV Word64
    mult :: SWord64)
                                                    in SBV Word64
    inp SBV Word64 -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    `sExtractBits` [Int
    7, Int
    15 .. Int
    63] [SBool] -> [SBool] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV Word64
    res SBV Word64 -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    `sExtractBits` [Int
    56 .. Int
    63]