hasmtlib-2.3.2: A monad for interfacing with external SMT solvers
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Hasmtlib.Internal.Bitvec

Synopsis

Documentation

newtype Bitvec (n :: Nat) Source #

Unsigned and length-indexed bitvector with MSB first.

Constructors

Bitvec 

Fields

Instances

Instances details
KnownNat n => Bounded (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

minBound :: Bitvec n #

maxBound :: Bitvec n #

KnownNat n => Enum (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

succ :: Bitvec n -> Bitvec n #

pred :: Bitvec n -> Bitvec n #

toEnum :: Int -> Bitvec n #

fromEnum :: Bitvec n -> Int #

enumFrom :: Bitvec n -> [Bitvec n] #

enumFromThen :: Bitvec n -> Bitvec n -> [Bitvec n] #

enumFromTo :: Bitvec n -> Bitvec n -> [Bitvec n] #

enumFromThenTo :: Bitvec n -> Bitvec n -> Bitvec n -> [Bitvec n] #

KnownNat n => Num (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

(+) :: Bitvec n -> Bitvec n -> Bitvec n #

(-) :: Bitvec n -> Bitvec n -> Bitvec n #

(*) :: Bitvec n -> Bitvec n -> Bitvec n #

negate :: Bitvec n -> Bitvec n #

abs :: Bitvec n -> Bitvec n #

signum :: Bitvec n -> Bitvec n #

fromInteger :: Integer -> Bitvec n #

KnownNat n => Integral (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

quot :: Bitvec n -> Bitvec n -> Bitvec n #

rem :: Bitvec n -> Bitvec n -> Bitvec n #

div :: Bitvec n -> Bitvec n -> Bitvec n #

mod :: Bitvec n -> Bitvec n -> Bitvec n #

quotRem :: Bitvec n -> Bitvec n -> (Bitvec n, Bitvec n) #

divMod :: Bitvec n -> Bitvec n -> (Bitvec n, Bitvec n) #

toInteger :: Bitvec n -> Integer #

KnownNat n => Real (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

toRational :: Bitvec n -> Rational #

Show (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

showsPrec :: Int -> Bitvec n -> ShowS #

show :: Bitvec n -> String #

showList :: [Bitvec n] -> ShowS #

Eq (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

(==) :: Bitvec n -> Bitvec n -> Bool #

(/=) :: Bitvec n -> Bitvec n -> Bool #

Ord (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

compare :: Bitvec n -> Bitvec n -> Ordering #

(<) :: Bitvec n -> Bitvec n -> Bool #

(<=) :: Bitvec n -> Bitvec n -> Bool #

(>) :: Bitvec n -> Bitvec n -> Bool #

(>=) :: Bitvec n -> Bitvec n -> Bool #

max :: Bitvec n -> Bitvec n -> Bitvec n #

min :: Bitvec n -> Bitvec n -> Bitvec n #

KnownNat n => Boolean (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Render (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

render :: Bitvec n -> Builder Source #

bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n Source #

bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n Source #

bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n Source #

bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m) Source #

bvTake' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec n Source #

bvDrop' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec m Source #

bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> (Bitvec n, Bitvec m) Source #

bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n) Source #

bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n) Source #

bvRotL :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n Source #

bvRotR :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n Source #

bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n) Source #

bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n + i) Source #

bvExtract :: forall n i j. (KnownNat i, KnownNat ((j - i) + 1), (i + (n - i)) ~ n, (((j - i) + 1) + ((n - i) - ((j - i) + 1))) ~ (n - i)) => Proxy i -> Proxy j -> Bitvec n -> Bitvec ((j - i) + 1) Source #