what4-1.8: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Utils.Arithmetic

Description

 
Synopsis

Arithmetic utilities

isPow2 :: (Bits a, Num a) => a -> Bool Source #

Returns true if number is a power of two.

isPow2Integer :: Integer -> Bool Source #

Returns true if Integer is a power of two. On GHC 9.0+ this uses a fast primop from ghc-bignum; on earlier GHCs it falls back to isPow2.

lg :: (Bits a, Num a, Ord a) => a -> Int Source #

Returns floor of log base 2. Polymorphic over bit-like types.

Note: For Integer specifically, prefer intLog2 which uses fast primops on GHC 9.0+.

intLog2 :: Integer -> Int Source #

intLog2 n for n >= 1: floor of base-2 logarithm. Undefined for n <= 0. On GHC 9.0+ this delegates to a fast primop in ghc-bignum; on earlier GHCs it falls back to lg.

lgCeil :: (Bits a, Num a, Ord a) => a -> Int Source #

Returns ceil of log base 2. Polymorphic over bit-like types. We define lgCeil 0 = 0 and lgCeil 1 = 0.

Note: For Integer specifically, prefer intLogCeil which uses fast primops on GHC 9.0+.

intLogCeil :: Integer -> Int Source #

intLogCeil n for n >= 0: ceiling of base-2 logarithm. We define intLogCeil 0 = 0 and intLogCeil 1 = 0. On GHC 9.0+ this uses fast primops from ghc-bignum; on earlier GHCs it falls back to lgCeil.

nextMultiple :: Integral a => a -> a -> a Source #

nextMultiple x y computes the next multiple m of x s.t. m >= y. E.g., nextMultiple 4 8 = 8 since 8 is a multiple of 8; nextMultiple 4 7 = 8; nextMultiple 8 6 = 8.

nextPow2Multiple :: (Bits a, Integral a) => a -> Int -> a Source #

nextPow2Multiple x n returns the smallest multiple of 2^n not less than x.

tryIntSqrt :: Integer -> Maybe Integer Source #

This returns the sqrt of an integer if it is well-defined.

tryRationalSqrt :: Rational -> Maybe Rational Source #

Return the rational sqrt of a

roundAway :: RealFrac a => a -> Integer Source #

Evaluate a real to an integer with rounding away from zero.

ctz :: forall (w :: Nat). NatRepr w -> Integer -> Integer Source #

Count trailing zeros

clz :: forall (w :: Nat). NatRepr w -> Integer -> Integer Source #

Count leading zeros

rotateLeft Source #

Arguments

:: forall (w :: Nat). NatRepr w

width

-> Integer

value to rotate

-> Integer

amount to rotate

-> Integer 

rotateRight Source #

Arguments

:: forall (w :: Nat). NatRepr w

width

-> Integer

value to rotate

-> Integer

amount to rotate

-> Integer