what4-domains-0.1: Abstract domains for What4 term simplification
Safe HaskellNone
LanguageHaskell2010

What4.Domains.Arithmetic.Internal

Description

Internal module exposing both optimized and reference implementations for property testing. Items in this module should not be considered part of What4's API; they are exported only for the sake of the test suite.

Synopsis

Reference implementations (always available)

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

Reference implementation: Count trailing zeros using bit testing loop

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

Reference implementation: Count leading zeros using bit testing loop

intLog2Ref :: Integer -> Int Source #

Reference implementation: Floor of log base 2 using shift loop

isPow2IntegerRef :: Integer -> Bool Source #

Reference implementation: Check if Integer is a positive power of two.

Optimized implementations (GHC 9.0+ only)

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

Optimized implementation: Count trailing zeros using ghc-bignum primops

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

Optimized implementation: Count leading zeros using integerLog2 primop

intLog2Opt :: Integer -> Int Source #

Optimized implementation: Floor of log base 2 using integerLog2 primop

isPow2IntegerOpt :: Integer -> Bool Source #

Optimized implementation: Check if Integer is power of two using primops