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	Safe-Inferred
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
- fromBits :: [Bool] -> a
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

lsb :: Bits a => a -> Bool Source #

Extract the least significant bit of a concrete value.

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

Instances details

FromBits Int16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Int16 Source #
FromBits Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Int32 Source #
FromBits Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Int64 Source #
FromBits Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Int8 Source #
FromBits Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Word16 Source #
FromBits Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Word32 Source #
FromBits Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Word64 Source #
FromBits Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Word8 Source #
FromBits SomeIntN Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> SomeIntN Source #
FromBits SomeWordN Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> SomeWordN Source #
FromBits Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Int Source #
FromBits Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> Word Source #
(KnownNat n, 1 <= n) => FromBits (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> IntN n Source #
(KnownNat n, 1 <= n) => FromBits (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> WordN n Source #

class (FiniteBits a, ITEOp a) => SymFiniteBits a where Source #

A class for symbolic finite bit operations.

Minimal complete definition

symTestBit, symFromBits

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.

Instances

Instances details

SymFiniteBits (SomeBV SymIntN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymIntN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymIntN -> Int -> SymBool -> SomeBV SymIntN Source # symFromBits :: [SymBool] -> SomeBV SymIntN Source #
SymFiniteBits (SomeBV SymWordN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymWordN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymWordN -> Int -> SymBool -> SomeBV SymWordN Source # symFromBits :: [SymBool] -> SomeBV SymWordN Source #
(KnownNat n, 1 <= n) => SymFiniteBits (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SymIntN n -> Int -> SymBool Source # symSetBitTo :: SymIntN n -> Int -> SymBool -> SymIntN n Source # symFromBits :: [SymBool] -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymFiniteBits (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SymWordN n -> Int -> SymBool Source # symSetBitTo :: SymWordN n -> Int -> SymBool -> SymWordN n Source # symFromBits :: [SymBool] -> SymWordN n Source #

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.