what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Utils.Arithmetic

Contents

- Arithmetic utilities

Description

Synopsis

- isPow2 :: (Bits a, Num a) => a -> Bool
- lg :: (Bits a, Num a, Ord a) => a -> Int
- lgCeil :: (Bits a, Num a, Ord a) => a -> Int
- nextMultiple :: Integral a => a -> a -> a
- nextPow2Multiple :: (Bits a, Integral a) => a -> Int -> a
- tryIntSqrt :: Integer -> Maybe Integer
- tryRationalSqrt :: Rational -> Maybe Rational
- roundAway :: RealFrac a => a -> Integer
- ctz :: NatRepr w -> Integer -> Integer
- clz :: NatRepr w -> Integer -> Integer
- rotateLeft :: NatRepr w -> Integer -> Integer -> Integer
- rotateRight :: NatRepr w -> Integer -> Integer -> Integer

# Arithmetic utilities

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

Returns true if number is a power of two.

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

Returns floor of log base 2.

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

Returns ceil of log base 2. We define `lgCeil 0 = 0`

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 :: NatRepr w -> Integer -> Integer Source #

Count trailing zeros

clz :: NatRepr w -> Integer -> Integer Source #

Count leading zeros

rotateLeft Source #

Arguments

:: NatRepr w | width
-> Integer | value to rotate
-> Integer | amount to rotate
-> Integer |

rotateRight Source #

Arguments

:: NatRepr w | width
-> Integer | value to rotate
-> Integer | amount to rotate
-> Integer |