| Copyright | (c) Sirui Lu 2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | None |
| Language | Haskell2010 |
Grisette.Internal.Core.Data.Class.SymFiniteBits
Description
Synopsis
- lsb :: Bits a => a -> Bool
- msb :: FiniteBits a => a -> Bool
- setBitTo :: Bits a => a -> Int -> Bool -> a
- bitBlast :: FiniteBits a => a -> [Bool]
- class FiniteBits a => FromBits a where
- class (FiniteBits a, ITEOp a) => SymFiniteBits a where
- symTestBit :: a -> Int -> SymBool
- symSetBitTo :: a -> Int -> SymBool -> a
- symFromBits :: [SymBool] -> a
- symBitBlast :: SymFiniteBits a => a -> [SymBool]
- symLsb :: SymFiniteBits a => a -> SymBool
- symMsb :: SymFiniteBits a => a -> SymBool
- symPopCount :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
- symCountLeadingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
- symCountTrailingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
Documentation
msb :: FiniteBits a => a -> Bool Source #
Extract the most significant bit of a concrete value.
setBitTo :: Bits a => a -> Int -> Bool -> a Source #
Set a bit in a concrete value to a specific value.
bitBlast :: FiniteBits a => a -> [Bool] Source #
Bit-blast a concrete value into a list of concrete bits. The first element in the resulting list corresponds to the least significant bit.
class FiniteBits a => FromBits a where Source #
Type class for assembling concrete bits to a bit-vector.
Minimal complete definition
Nothing
Methods
fromBits :: [Bool] -> a Source #
Assembling concrete bits to a bit-vector. The first boolean value in the list corresponding to the least signification value.
Instances
| FromBits Int16 Source # | |
| FromBits Int32 Source # | |
| FromBits Int64 Source # | |
| FromBits Int8 Source # | |
| FromBits Word16 Source # | |
| FromBits Word32 Source # | |
| FromBits Word64 Source # | |
| FromBits Word8 Source # | |
| FromBits SomeIntN Source # | |
| FromBits SomeWordN Source # | |
| FromBits Int Source # | |
| FromBits Word Source # | |
| (KnownNat n, 1 <= n) => FromBits (IntN n) Source # | |
| (KnownNat n, 1 <= n) => FromBits (WordN n) Source # | |
class (FiniteBits a, ITEOp a) => SymFiniteBits a where Source #
A class for symbolic finite bit operations.
Minimal complete definition
Methods
symTestBit :: a -> Int -> SymBool Source #
Test a symbolic bit in a symbolic bit-vector.
symSetBitTo :: a -> Int -> SymBool -> a Source #
Set a bit in a symbolic value to a specific value.
symFromBits :: [SymBool] -> a Source #
Assembling symbolic bits to a symbolic bit-vector. The first symbolic boolean value in the list corresponding to the least signification value.
symBitBlast :: SymFiniteBits a => a -> [SymBool] Source #
Bit-blast a symbolic value into a list of symbolic bits. The first element in the resulting list corresponds to the least significant bit.
symLsb :: SymFiniteBits a => a -> SymBool Source #
Extract the least significant bit of a symbolic value.
symMsb :: SymFiniteBits a => a -> SymBool Source #
Extract the most significant bit of a symbolic value.
symPopCount :: (Num a, ITEOp a, SymFiniteBits a) => a -> a Source #
Count the number of set bits in a symbolic value.
symCountLeadingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a Source #
Count the number of leading zeros in a symbolic value.
symCountTrailingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a Source #
Count the number of trailing zeros in a symbolic value.