Cryptol.Symbolic.BitVector

Description

Synopsis

• data BitVector = BV {
  • signedcxt :: Bool
  • width :: !Int
  • val :: !Integer
  }
• bitMask :: Int -> Integer
• bv :: Int -> Integer -> BitVector
• sbv :: Bool -> Int -> Integer -> BitVector
• unsigned :: Int -> Integer -> Integer
• signed :: Int -> Integer -> Integer
• same :: Int -> Int -> Int
• type SWord = SBV BitVector
• extract :: Int -> Int -> SWord -> SWord
• cat :: SWord -> SWord -> SWord
• literalSWord :: Int -> Integer -> SWord
• randomSBVBitVector :: Int -> IO (SBV BitVector)
• mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector)
• forallBV :: String -> Int -> Symbolic (SBV BitVector)
• forallBV_ :: Int -> Symbolic (SBV BitVector)
• existsBV :: String -> Int -> Symbolic (SBV BitVector)
• existsBV_ :: Int -> Symbolic (SBV BitVector)

Documentation