-----------------------------------------------------------------------------
-- |
-- 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 SBool -> IO SatResult
forall a. Provable a => SMTConfig -> a -> IO SatResult
satWith SMTConfig
z3{printBase :: Int
printBase=Int
16} SymbolicT IO SBool
find
  where find :: SymbolicT IO SBool
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
":tactic.default_tactic" [String
"sat"]
                  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
":sat.euf"               [String
"true"]
                  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)
sbvExists String
"mask"
                  SBV Word64
mult <- String -> Symbolic (SBV Word64)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"mult"
                  SBV Word64
inp  <- String -> Symbolic (SBV Word64)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"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)
                  [SBool] -> SymbolicT IO SBool
solve [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]]