{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SymFiniteBits
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.SymFiniteBits
  ( lsb,
    msb,
    setBitTo,
    bitBlast,
    FromBits (..),
    SymFiniteBits (..),
    symBitBlast,
    symLsb,
    symMsb,
    symPopCount,
    symCountLeadingZeros,
    symCountTrailingZeros,
  )
where

import Data.Bits
  ( Bits (bit, clearBit, setBit, testBit, zeroBits, (.|.)),
    FiniteBits (finiteBitSize),
  )
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.BitVector
  ( BV (bv, bvSelect),
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.SomeBV
  ( SomeBV (SomeBV),
    SomeIntN,
    SomeWordN,
    unsafeSomeBV,
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymBool (SymBool)

-- | Set a bit in a concrete value to a specific value.
setBitTo :: (Bits a) => a -> Int -> Bool -> a
setBitTo :: forall a. Bits a => a -> Int -> Bool -> a
setBitTo a
v Int
i Bool
b = if Bool
b then a -> Int -> a
forall a. Bits a => a -> Int -> a
setBit a
v Int
i else a -> Int -> a
forall a. Bits a => a -> Int -> a
clearBit a
v Int
i

-- | Bit-blast a concrete value into a list of concrete bits. The first element
-- in the resulting list corresponds to the least significant bit.
bitBlast :: (FiniteBits a) => a -> [Bool]
bitBlast :: forall a. FiniteBits a => a -> [Bool]
bitBlast a
x = (Int -> Bool) -> [Int] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
x) [Int
0 .. a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

-- | Extract the least significant bit of a concrete value.
lsb :: (Bits a) => a -> Bool
lsb :: forall a. Bits a => a -> Bool
lsb a
x = a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
x Int
0

-- | Extract the most significant bit of a concrete value.
msb :: (FiniteBits a) => a -> Bool
msb :: forall a. FiniteBits a => a -> Bool
msb a
x = a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
x (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

-- | Type class for assembling concrete bits to a bit-vector.
class (FiniteBits a) => FromBits a where
  -- | Assembling concrete bits to a bit-vector. The first boolean value in the
  -- list corresponding to the least signification value.
  fromBits :: [Bool] -> a
  fromBits [Bool]
bits
    | [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
bits Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (a
forall a. HasCallStack => a
undefined :: a) =
        [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromBits: length mismatch"
    | Bool
otherwise = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
forall a. Bits a => a -> a -> a
(.|.) [a]
lst
    where
      lst :: [a]
      lst :: [a]
lst = (\(Int
pos, Bool
b) -> if Bool
b then Int -> a
forall a. Bits a => Int -> a
bit Int
pos else a
forall a. Bits a => a
zeroBits) ((Int, Bool) -> a) -> [(Int, Bool)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Bool]
bits

instance FromBits Int

instance FromBits Int8

instance FromBits Int16

instance FromBits Int32

instance FromBits Int64

instance FromBits Word

instance FromBits Word8

instance FromBits Word16

instance FromBits Word32

instance FromBits Word64

instance (KnownNat n, 1 <= n) => FromBits (WordN n)

instance (KnownNat n, 1 <= n) => FromBits (IntN n)

instance FromBits SomeIntN where
  fromBits :: [Bool] -> SomeIntN
fromBits [Bool]
bits
    | [Bool] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bool]
bits =
        [Char] -> SomeIntN
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot create a SomeBV from an empty list of bits."
  fromBits [Bool]
bits = Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> IntN n)
-> SomeIntN
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV ([Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
bits) ((forall (proxy :: Nat -> *) (n :: Nat).
  (KnownNat n, 1 <= n) =>
  proxy n -> IntN n)
 -> SomeIntN)
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> IntN n)
-> SomeIntN
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> [Bool] -> IntN n
forall a. FromBits a => [Bool] -> a
fromBits [Bool]
bits

instance FromBits SomeWordN where
  fromBits :: [Bool] -> SomeWordN
fromBits [Bool]
bits
    | [Bool] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bool]
bits =
        [Char] -> SomeWordN
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot create a SomeBV from an empty list of bits."
  fromBits [Bool]
bits = Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> WordN n)
-> SomeWordN
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV ([Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
bits) ((forall (proxy :: Nat -> *) (n :: Nat).
  (KnownNat n, 1 <= n) =>
  proxy n -> WordN n)
 -> SomeWordN)
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> WordN n)
-> SomeWordN
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> [Bool] -> WordN n
forall a. FromBits a => [Bool] -> a
fromBits [Bool]
bits

-- | A class for symbolic finite bit operations.
class (FiniteBits a, ITEOp a) => SymFiniteBits a where
  -- | Test a symbolic bit in a symbolic bit-vector.
  symTestBit :: a -> Int -> SymBool

  -- | Set a bit in a symbolic value to a specific value.
  symSetBitTo :: a -> Int -> SymBool -> a
  symSetBitTo a
v Int
i SymBool
b = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b (a -> Int -> a
forall a. Bits a => a -> Int -> a
setBit a
v Int
i) (a -> Int -> a
forall a. Bits a => a -> Int -> a
clearBit a
v Int
i)

  -- | Assembling symbolic bits to a symbolic bit-vector. The first symbolic
  -- boolean value in the list corresponding to the least signification value.
  symFromBits :: [SymBool] -> a

instance SymFiniteBits (SomeBV SymIntN) where
  symTestBit :: SomeBV SymIntN -> Int -> SymBool
symTestBit SomeBV SymIntN
v Int
i = Int -> Int -> SomeBV SymIntN -> SomeBV SymIntN
forall bv. BV bv => Int -> Int -> bv -> bv
bvSelect Int
i Int
1 SomeBV SymIntN
v SomeBV SymIntN -> SomeBV SymIntN -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== Int -> Integer -> SomeBV SymIntN
forall a. Integral a => Int -> a -> SomeBV SymIntN
forall bv a. (BV bv, Integral a) => Int -> a -> bv
bv Int
1 Integer
1
  symFromBits :: [SymBool] -> SomeBV SymIntN
symFromBits [SymBool]
bits
    | [SymBool] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SymBool]
bits =
        [Char] -> SomeBV SymIntN
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot create a SomeBV from an empty list of bits."
  symFromBits [SymBool]
bits = Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> SymIntN n)
-> SomeBV SymIntN
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV ([SymBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SymBool]
bits) ((forall (proxy :: Nat -> *) (n :: Nat).
  (KnownNat n, 1 <= n) =>
  proxy n -> SymIntN n)
 -> SomeBV SymIntN)
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> SymIntN n)
-> SomeBV SymIntN
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> [SymBool] -> SymIntN n
forall a. SymFiniteBits a => [SymBool] -> a
symFromBits [SymBool]
bits

instance SymFiniteBits (SomeBV SymWordN) where
  symTestBit :: SomeBV SymWordN -> Int -> SymBool
symTestBit SomeBV SymWordN
v Int
i = Int -> Int -> SomeBV SymWordN -> SomeBV SymWordN
forall bv. BV bv => Int -> Int -> bv -> bv
bvSelect Int
i Int
1 SomeBV SymWordN
v SomeBV SymWordN -> SomeBV SymWordN -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== Int -> Integer -> SomeBV SymWordN
forall a. Integral a => Int -> a -> SomeBV SymWordN
forall bv a. (BV bv, Integral a) => Int -> a -> bv
bv Int
1 Integer
1
  symFromBits :: [SymBool] -> SomeBV SymWordN
symFromBits [SymBool]
bits
    | [SymBool] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SymBool]
bits =
        [Char] -> SomeBV SymWordN
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot create a SomeBV from an empty list of bits."
  symFromBits [SymBool]
bits = Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> SymWordN n)
-> SomeBV SymWordN
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV ([SymBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SymBool]
bits) ((forall (proxy :: Nat -> *) (n :: Nat).
  (KnownNat n, 1 <= n) =>
  proxy n -> SymWordN n)
 -> SomeBV SymWordN)
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> SymWordN n)
-> SomeBV SymWordN
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> [SymBool] -> SymWordN n
forall a. SymFiniteBits a => [SymBool] -> a
symFromBits [SymBool]
bits

instance (KnownNat n, 1 <= n) => SymFiniteBits (SymIntN n) where
  symTestBit :: SymIntN n -> Int -> SymBool
symTestBit SymIntN n
v = SomeBV SymIntN -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
symTestBit (SymIntN n -> SomeBV SymIntN
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV SymIntN n
v)
  symSetBitTo :: SymIntN n -> Int -> SymBool -> SymIntN n
symSetBitTo SymIntN n
v Int
i SymBool
b = SymBool -> SymIntN n -> SymIntN n -> SymIntN n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b (SymIntN n -> Int -> SymIntN n
forall a. Bits a => a -> Int -> a
setBit SymIntN n
v Int
i) (SymIntN n -> Int -> SymIntN n
forall a. Bits a => a -> Int -> a
clearBit SymIntN n
v Int
i)
  symFromBits :: [SymBool] -> SymIntN n
symFromBits [SymBool]
bits
    | [SymBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SymBool]
bits Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= SymWordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (SymWordN n
forall a. HasCallStack => a
undefined :: SymWordN n) =
        [Char] -> SymIntN n
forall a. HasCallStack => [Char] -> a
error [Char]
"symFromBits: length mismatch"
    | Bool
otherwise = (SymIntN n -> SymIntN n -> SymIntN n) -> [SymIntN n] -> SymIntN n
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SymIntN n -> SymIntN n -> SymIntN n
forall a. Bits a => a -> a -> a
(.|.) [SymIntN n]
lst
    where
      lst :: [SymIntN n]
      lst :: [SymIntN n]
lst = (\(Int
pos, SymBool
b) -> SymBool -> SymIntN n -> SymIntN n -> SymIntN n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b (SymIntN n -> Int -> SymIntN n
forall a. Bits a => a -> Int -> a
setBit SymIntN n
0 Int
pos) SymIntN n
0) ((Int, SymBool) -> SymIntN n) -> [(Int, SymBool)] -> [SymIntN n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int] -> [SymBool] -> [(Int, SymBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [SymBool]
bits

instance (KnownNat n, 1 <= n) => SymFiniteBits (SymWordN n) where
  symTestBit :: SymWordN n -> Int -> SymBool
symTestBit SymWordN n
v = SomeBV SymWordN -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
symTestBit (SymWordN n -> SomeBV SymWordN
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV SymWordN n
v)
  symSetBitTo :: SymWordN n -> Int -> SymBool -> SymWordN n
symSetBitTo SymWordN n
v Int
i SymBool
b = SymBool -> SymWordN n -> SymWordN n -> SymWordN n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b (SymWordN n -> Int -> SymWordN n
forall a. Bits a => a -> Int -> a
setBit SymWordN n
v Int
i) (SymWordN n -> Int -> SymWordN n
forall a. Bits a => a -> Int -> a
clearBit SymWordN n
v Int
i)
  symFromBits :: [SymBool] -> SymWordN n
symFromBits [SymBool]
bits
    | [SymBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SymBool]
bits Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= SymWordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (SymWordN n
forall a. HasCallStack => a
undefined :: SymWordN n) =
        [Char] -> SymWordN n
forall a. HasCallStack => [Char] -> a
error [Char]
"symFromBits: length mismatch"
    | Bool
otherwise = (SymWordN n -> SymWordN n -> SymWordN n)
-> [SymWordN n] -> SymWordN n
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SymWordN n -> SymWordN n -> SymWordN n
forall a. Bits a => a -> a -> a
(.|.) [SymWordN n]
lst
    where
      lst :: [SymWordN n]
      lst :: [SymWordN n]
lst = (\(Int
pos, SymBool
b) -> SymBool -> SymWordN n -> SymWordN n -> SymWordN n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b (SymWordN n -> Int -> SymWordN n
forall a. Bits a => a -> Int -> a
setBit SymWordN n
0 Int
pos) SymWordN n
0) ((Int, SymBool) -> SymWordN n) -> [(Int, SymBool)] -> [SymWordN n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int] -> [SymBool] -> [(Int, SymBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [SymBool]
bits

-- | Bit-blast a symbolic value into a list of symbolic bits. The first element
-- in the resulting list corresponds to the least significant bit.
symBitBlast :: (SymFiniteBits a) => a -> [SymBool]
symBitBlast :: forall a. SymFiniteBits a => a -> [SymBool]
symBitBlast a
x = (Int -> SymBool) -> [Int] -> [SymBool]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
symTestBit a
x) [Int
0 .. a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

-- | Extract the least significant bit of a symbolic value.
symLsb :: (SymFiniteBits a) => a -> SymBool
symLsb :: forall a. SymFiniteBits a => a -> SymBool
symLsb a
x = a -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
symTestBit a
x Int
0

-- | Extract the most significant bit of a symbolic value.
symMsb :: (SymFiniteBits a) => a -> SymBool
symMsb :: forall a. SymFiniteBits a => a -> SymBool
symMsb a
x = a -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
symTestBit a
x (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

-- | Count the number of set bits in a symbolic value.
symPopCount :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
-- Node: v - v + is a trick to assign the correct bit-width to the result.
symPopCount :: forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
symPopCount a
v = a
v a -> a -> a
forall a. Num a => a -> a -> a
- a
v a -> a -> a
forall a. Num a => a -> a -> a
+ [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((\SymBool
b -> SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b a
1 a
0) (SymBool -> a) -> [SymBool] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [SymBool]
forall a. SymFiniteBits a => a -> [SymBool]
symBitBlast a
v)

-- | Count the number of leading zeros in a symbolic value.
symCountLeadingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
-- Node: v - v + is a trick to assign the correct bit-width to the result.
symCountLeadingZeros :: forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
symCountLeadingZeros a
v = a
v a -> a -> a
forall a. Num a => a -> a -> a
- a
v a -> a -> a
forall a. Num a => a -> a -> a
+ [SymBool] -> [a] -> a
forall {t}. ITEOp t => [SymBool] -> [t] -> t
go [SymBool]
bits [a]
rs
  where
    bits :: [SymBool]
bits = [SymBool] -> [SymBool]
forall a. [a] -> [a]
reverse ([SymBool] -> [SymBool]) -> [SymBool] -> [SymBool]
forall a b. (a -> b) -> a -> b
$ a -> [SymBool]
forall a. SymFiniteBits a => a -> [SymBool]
symBitBlast a
v
    rs :: [a]
rs = Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> a) -> [Integer] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 ..]
    go :: [SymBool] -> [t] -> t
go [] (t
r : [t]
_) = t
r
    go (SymBool
b : [SymBool]
bs) (t
r : [t]
rs) = SymBool -> t -> t -> t
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b t
r ([SymBool] -> [t] -> t
go [SymBool]
bs [t]
rs)
    go [SymBool]
_ [] = [Char] -> t
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"

-- | Count the number of trailing zeros in a symbolic value.
symCountTrailingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a
-- Node: v - v + is a trick to assign the correct bit-width to the result.
symCountTrailingZeros :: forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
symCountTrailingZeros a
v = a
v a -> a -> a
forall a. Num a => a -> a -> a
- a
v a -> a -> a
forall a. Num a => a -> a -> a
+ [SymBool] -> [a] -> a
forall {t}. ITEOp t => [SymBool] -> [t] -> t
go [SymBool]
bits [a]
rs
  where
    bits :: [SymBool]
bits = a -> [SymBool]
forall a. SymFiniteBits a => a -> [SymBool]
symBitBlast a
v
    rs :: [a]
rs = Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> a) -> [Integer] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 ..]
    go :: [SymBool] -> [t] -> t
go [] (t
r : [t]
_) = t
r
    go (SymBool
b : [SymBool]
bs) (t
r : [t]
rs) = SymBool -> t -> t -> t
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
b t
r ([SymBool] -> [t] -> t
go [SymBool]
bs [t]
rs)
    go [SymBool]
_ [] = [Char] -> t
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"