{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.BitPrecise.MultMask where
import Data.SBV
import Data.SBV.Control
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
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]