    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.Polynomial
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Implementation of polynomial arithmetic
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE FlexibleContexts     #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE PatternGuards        #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.Polynomial (
            -- * Polynomial arithmetic and CRCs
            Polynomial(..), crc, crcBV, ites, mdp, addPoly
            ) where

    import Data.Bits  (Bits(..))
    import Data.List  (genericTake)
    import Data.Maybe (fromJust, fromMaybe)
    import Data.Word  (Word8, Word16, Word32, Word64)

    import Data.SBV.Core.Data
    import Data.SBV.Core.Sized
    import Data.SBV.Core.Model

    import GHC.TypeLits

    -- | Implements polynomial addition, multiplication, division, and modulus operations
    -- over GF(2^n).  NB. Similar to 'sQuotRem', division by @0@ is interpreted as follows:
    --
    --     @x `pDivMod` 0 = (0, x)@
    --
    -- for all @x@ (including @0@)
    --
    -- Minimal complete definition: 'pMult', 'pDivMod', 'showPolynomial'
    class (Num a, Bits a) => Polynomial a where
     -- | Given bit-positions to be set, create a polynomial
     -- For instance
     --
     --     @polynomial [0, 1, 3] :: SWord8@
     --
     -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial
     -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.
     polynomial :: [Int] -> a
     -- | Add two polynomials in GF(2^n).
     pAdd  :: a -> a -> a
     -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by
     -- the polynomial as specified by coefficients of the third argument. Note that the third
     -- argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our
     -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not
     -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,
     -- so this should not be a problem in practice.)
     --
     -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't
     -- fit into the resulting size.
     pMult :: (a, a, [Int]) -> a
     -- | Divide two polynomials in GF(2^n), see above note for division by 0.
     pDiv  :: a -> a -> a
     -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0.
     pMod  :: a -> a -> a
     -- | Division and modulus packed together.
     pDivMod :: a -> a -> (a, a)
     -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type.
     showPoly :: a -> String
     -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument
     -- controls if the final type is shown as well.
     showPolynomial :: Bool -> a -> String

     {-# MINIMAL pMult, pDivMod, showPolynomial #-}
     polynomial = (Int -> a -> a) -> a -> [Int] -> a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((a -> Int -> a) -> Int -> a -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip a -> Int -> a
    forall a. Bits a => a -> Int -> a
    setBit) 0
     pAdd       = a -> a -> a
    forall a. Bits a => a -> a -> a
    xor
     pDiv x :: a
    x y :: a
    y   = (a, a) -> a
    forall a b. (a, b) -> a
    fst (a -> a -> (a, a)
    forall a. Polynomial a => a -> a -> (a, a)
    pDivMod a
    x a
    y)
     pMod x :: a
    x y :: a
    y   = (a, a) -> a
    forall a b. (a, b) -> b
    snd (a -> a -> (a, a)
    forall a. Polynomial a => a -> a -> (a, a)
    pDivMod a
    x a
    y)
     showPoly   = Bool -> a -> String
    forall a. Polynomial a => Bool -> a -> String
    showPolynomial Bool
    False

    instance Polynomial Word8   where {showPolynomial :: Bool -> Word8 -> String
    showPolynomial   = Bool -> Word8 -> String
    forall a. Bits a => Bool -> a -> String
    sp;           pMult :: (Word8, Word8, [Int]) -> Word8
    pMult = ((SBV Word8, SBV Word8, [Int]) -> SBV Word8)
    -> (Word8, Word8, [Int]) -> Word8
    forall a.
    SymVal a =>
    ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift (SBV Word8, SBV Word8, [Int]) -> SBV Word8
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult; pDivMod :: Word8 -> Word8 -> (Word8, Word8)
    pDivMod = (SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8))
    -> Word8 -> Word8 -> (Word8, Word8)
    forall a.
    SymVal a =>
    (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial Word16  where {showPolynomial :: Bool -> Word16 -> String
    showPolynomial   = Bool -> Word16 -> String
    forall a. Bits a => Bool -> a -> String
    sp;           pMult :: (Word16, Word16, [Int]) -> Word16
    pMult = ((SBV Word16, SBV Word16, [Int]) -> SBV Word16)
    -> (Word16, Word16, [Int]) -> Word16
    forall a.
    SymVal a =>
    ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift (SBV Word16, SBV Word16, [Int]) -> SBV Word16
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult; pDivMod :: Word16 -> Word16 -> (Word16, Word16)
    pDivMod = (SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16))
    -> Word16 -> Word16 -> (Word16, Word16)
    forall a.
    SymVal a =>
    (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial Word32  where {showPolynomial :: Bool -> Word32 -> String
    showPolynomial   = Bool -> Word32 -> String
    forall a. Bits a => Bool -> a -> String
    sp;           pMult :: (Word32, Word32, [Int]) -> Word32
    pMult = ((SBV Word32, SBV Word32, [Int]) -> SBV Word32)
    -> (Word32, Word32, [Int]) -> Word32
    forall a.
    SymVal a =>
    ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift (SBV Word32, SBV Word32, [Int]) -> SBV Word32
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult; pDivMod :: Word32 -> Word32 -> (Word32, Word32)
    pDivMod = (SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32))
    -> Word32 -> Word32 -> (Word32, Word32)
    forall a.
    SymVal a =>
    (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial Word64  where {showPolynomial :: Bool -> Word64 -> String
    showPolynomial   = Bool -> Word64 -> String
    forall a. Bits a => Bool -> a -> String
    sp;           pMult :: (Word64, Word64, [Int]) -> Word64
    pMult = ((SBV Word64, SBV Word64, [Int]) -> SBV Word64)
    -> (Word64, Word64, [Int]) -> Word64
    forall a.
    SymVal a =>
    ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift (SBV Word64, SBV Word64, [Int]) -> SBV Word64
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult; pDivMod :: Word64 -> Word64 -> (Word64, Word64)
    pDivMod = (SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64))
    -> Word64 -> Word64 -> (Word64, Word64)
    forall a.
    SymVal a =>
    (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial SWord8  where {showPolynomial :: Bool -> SBV Word8 -> String
    showPolynomial b :: Bool
    b = (Word8 -> String) -> SBV Word8 -> String
    forall a. SymVal a => (a -> String) -> SBV a -> String
    liftS (Bool -> Word8 -> String
    forall a. Bits a => Bool -> a -> String
    sp Bool
    b); pMult :: (SBV Word8, SBV Word8, [Int]) -> SBV Word8
    pMult = (SBV Word8, SBV Word8, [Int]) -> SBV Word8
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult;      pDivMod :: SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
    pDivMod = SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial SWord16 where {showPolynomial :: Bool -> SBV Word16 -> String
    showPolynomial b :: Bool
    b = (Word16 -> String) -> SBV Word16 -> String
    forall a. SymVal a => (a -> String) -> SBV a -> String
    liftS (Bool -> Word16 -> String
    forall a. Bits a => Bool -> a -> String
    sp Bool
    b); pMult :: (SBV Word16, SBV Word16, [Int]) -> SBV Word16
    pMult = (SBV Word16, SBV Word16, [Int]) -> SBV Word16
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult;      pDivMod :: SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
    pDivMod = SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial SWord32 where {showPolynomial :: Bool -> SBV Word32 -> String
    showPolynomial b :: Bool
    b = (Word32 -> String) -> SBV Word32 -> String
    forall a. SymVal a => (a -> String) -> SBV a -> String
    liftS (Bool -> Word32 -> String
    forall a. Bits a => Bool -> a -> String
    sp Bool
    b); pMult :: (SBV Word32, SBV Word32, [Int]) -> SBV Word32
    pMult = (SBV Word32, SBV Word32, [Int]) -> SBV Word32
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult;      pDivMod :: SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
    pDivMod = SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}
    instance Polynomial SWord64 where {showPolynomial :: Bool -> SBV Word64 -> String
    showPolynomial b :: Bool
    b = (Word64 -> String) -> SBV Word64 -> String
    forall a. SymVal a => (a -> String) -> SBV a -> String
    liftS (Bool -> Word64 -> String
    forall a. Bits a => Bool -> a -> String
    sp Bool
    b); pMult :: (SBV Word64, SBV Word64, [Int]) -> SBV Word64
    pMult = (SBV Word64, SBV Word64, [Int]) -> SBV Word64
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult;      pDivMod :: SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
    pDivMod = SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}

    instance (KnownNat n, IsNonZero n) => Polynomial (SWord n) where {showPolynomial :: Bool -> SWord n -> String
    showPolynomial b :: Bool
    b = (WordN n -> String) -> SWord n -> String
    forall a. SymVal a => (a -> String) -> SBV a -> String
    liftS (Bool -> WordN n -> String
    forall a. Bits a => Bool -> a -> String
    sp Bool
    b); pMult :: (SWord n, SWord n, [Int]) -> SWord n
    pMult = (SWord n, SWord n, [Int]) -> SWord n
    forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult;      pDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
    pDivMod = SWord n -> SWord n -> (SWord n, SWord n)
    forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod}

    lift :: SymVal a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift :: ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
    lift f :: (SBV a, SBV a, [Int]) -> SBV a
    f (x :: a
    x, y :: a
    y, z :: [Int]
    z) = Maybe a -> a
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe a -> a) -> Maybe a -> a
    forall a b. (a -> b) -> a -> b
    $ SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SBV a -> Maybe a) -> SBV a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ (SBV a, SBV a, [Int]) -> SBV a
    f (a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    x, a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    y, [Int]
    z)
    liftC :: SymVal a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC :: (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
    liftC f :: SBV a -> SBV a -> (SBV a, SBV a)
    f x :: a
    x y :: a
    y = let (a :: SBV a
    a, b :: SBV a
    b) = SBV a -> SBV a -> (SBV a, SBV a)
    f (a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    x) (a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    y) in (Maybe a -> a
    forall a. HasCallStack => Maybe a -> a
    fromJust (SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a), Maybe a -> a
    forall a. HasCallStack => Maybe a -> a
    fromJust (SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    b))
    liftS :: SymVal a => (a -> String) -> SBV a -> String
    liftS :: (a -> String) -> SBV a -> String
    liftS f :: a -> String
    f s :: SBV a
    s
      | Just x :: a
    x <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    s = a -> String
    f a
    x
      | Bool
    True                  = SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    s

    -- | Pretty print as a polynomial
    sp :: Bits a => Bool -> a -> String
    sp :: Bool -> a -> String
    sp st :: Bool
    st a :: a
    a
     | [Int] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Int]
    cs = '0' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    t
     | Bool
    True    = (Int -> String -> String) -> String -> [Int] -> String
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\x :: Int
    x y :: String
    y -> Int -> String
    forall a. (Eq a, Num a, Show a) => a -> String
    sh Int
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " + " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y) (Int -> String
    forall a. (Eq a, Num a, Show a) => a -> String
    sh ([Int] -> Int
    forall a. [a] -> a
    last [Int]
    cs)) ([Int] -> [Int]
    forall a. [a] -> [a]
    init [Int]
    cs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t
     where t :: String
    t | Bool
    st   = " :: GF(2^" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
             | Bool
    True = ""
           n :: Int
    n  = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe (String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.Polynomial.sp: Unexpected non-finite usage!") (a -> Maybe Int
    forall a. Bits a => a -> Maybe Int
    bitSizeMaybe a
    a)
           is :: [Int]
    is = [Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1, Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -2 .. 0]
           cs :: [Int]
    cs = ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Bool) -> Int
    forall a b. (a, b) -> a
    fst ([(Int, Bool)] -> [Int]) -> [(Int, Bool)] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Int, Bool) -> Bool
    forall a b. (a, b) -> b
    snd ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
    forall a b. (a -> b) -> a -> b
    $ [Int] -> [Bool] -> [(Int, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    is ((Int -> Bool) -> [Int] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map (a -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit a
    a) [Int]
    is)
           sh :: a -> String
    sh 0 = "1"
           sh 1 = "x"
           sh i :: a
    i = "x^" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i

    -- | Add two polynomials
    addPoly :: [SBool] -> [SBool] -> [SBool]
    addPoly :: [SBool] -> [SBool] -> [SBool]
    addPoly xs :: [SBool]
    xs    []      = [SBool]
    xs
    addPoly []    ys :: [SBool]
    ys      = [SBool]
    ys
    addPoly (x :: SBool
    x:xs :: [SBool]
    xs) (y :: SBool
    y:ys :: [SBool]
    ys) = SBool
    x SBool -> SBool -> SBool
    .<+> SBool
    y SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool] -> [SBool] -> [SBool]
    addPoly [SBool]
    xs [SBool]
    ys

    -- | Run down a boolean condition over two lists. Note that this is
    -- different than zipWith as shorter list is assumed to be filled with
    -- sFalse at the end (i.e., zero-bits); which nicely pads it when
    -- considered as an unsigned number in little-endian form.
    ites :: SBool -> [SBool] -> [SBool] -> [SBool]
    ites :: SBool -> [SBool] -> [SBool] -> [SBool]
    ites s :: SBool
    s xs :: [SBool]
    xs ys :: [SBool]
    ys
     | Just t :: Bool
    t <- SBool -> Maybe Bool
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBool
    s
     = if Bool
    t then [SBool]
    xs else [SBool]
    ys
     | Bool
    True
     = [SBool] -> [SBool] -> [SBool]
    go [SBool]
    xs [SBool]
    ys
     where go :: [SBool] -> [SBool] -> [SBool]
    go []     []     = []
           go []     (b :: SBool
    b:bs :: [SBool]
    bs) = SBool -> SBool -> SBool -> SBool
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    s SBool
    sFalse SBool
    b SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool] -> [SBool] -> [SBool]
    go [] [SBool]
    bs
           go (a :: SBool
    a:as :: [SBool]
    as) []     = SBool -> SBool -> SBool -> SBool
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    s SBool
    a SBool
    sFalse SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool] -> [SBool] -> [SBool]
    go [SBool]
    as []
           go (a :: SBool
    a:as :: [SBool]
    as) (b :: SBool
    b:bs :: [SBool]
    bs) = SBool -> SBool -> SBool -> SBool
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    s SBool
    a SBool
    b SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool] -> [SBool] -> [SBool]
    go [SBool]
    as [SBool]
    bs

    -- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients.
    -- See the remarks for the 'pMult' function for this design choice
    polyMult :: SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
    polyMult :: (SBV a, SBV a, [Int]) -> SBV a
    polyMult (x :: SBV a
    x, y :: SBV a
    y, red :: [Int]
    red)
      | SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isReal SBV a
    x
      = String -> SBV a
    forall a. HasCallStack => String -> a
    error (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ "SBV.polyMult: Received a real value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    x
      | Bool -> Bool
    not (SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SBV a
    x)
      = String -> SBV a
    forall a. HasCallStack => String -> a
    error (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ "SBV.polyMult: Received infinite precision value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    x
      | Bool
    True
      = [SBool] -> SBV a
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsLE ([SBool] -> SBV a) -> [SBool] -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Int -> [SBool] -> [SBool]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Int
    sz ([SBool] -> [SBool]) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ [SBool]
    r [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ SBool -> [SBool]
    forall a. a -> [a]
    repeat SBool
    sFalse
      where (_, r :: [SBool]
    r) = [SBool] -> [SBool] -> ([SBool], [SBool])
    mdp [SBool]
    ms [SBool]
    rs
            ms :: [SBool]
    ms = Int -> [SBool] -> [SBool]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake (2Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    sz) ([SBool] -> [SBool]) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> [SBool] -> [SBool] -> [SBool]
    mul (SBV a -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastLE SBV a
    x) (SBV a -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastLE SBV a
    y) [] [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ SBool -> [SBool]
    forall a. a -> [a]
    repeat SBool
    sFalse
            rs :: [SBool]
    rs = Int -> [SBool] -> [SBool]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake (2Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    sz) ([SBool] -> [SBool]) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ [Bool -> SBool
    fromBool (Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Int]
    red) |  Int
    i <- [0 .. (Int -> Int -> Int) -> Int -> [Int] -> Int
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max 0 [Int]
    red] ] [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ SBool -> [SBool]
    forall a. a -> [a]
    repeat SBool
    sFalse
            sz :: Int
    sz = SBV a -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBV a
    x
            mul :: [SBool] -> [SBool] -> [SBool] -> [SBool]
    mul _  []     ps :: [SBool]
    ps = [SBool]
    ps
            mul as :: [SBool]
    as (b :: SBool
    b:bs :: [SBool]
    bs) ps :: [SBool]
    ps = [SBool] -> [SBool] -> [SBool] -> [SBool]
    mul (SBool
    sFalseSBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    :[SBool]
    as) [SBool]
    bs (SBool -> [SBool] -> [SBool] -> [SBool]
    ites SBool
    b ([SBool]
    as [SBool] -> [SBool] -> [SBool]
    `addPoly` [SBool]
    ps) [SBool]
    ps)

    polyDivMod :: SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod :: SBV a -> SBV a -> (SBV a, SBV a)
    polyDivMod x :: SBV a
    x y :: SBV a
    y
       | SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isReal SBV a
    x
       = String -> (SBV a, SBV a)
    forall a. HasCallStack => String -> a
    error (String -> (SBV a, SBV a)) -> String -> (SBV a, SBV a)
    forall a b. (a -> b) -> a -> b
    $ "SBV.polyDivMod: Received a real value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    x
       | Bool -> Bool
    not (SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SBV a
    x)
       = String -> (SBV a, SBV a)
    forall a. HasCallStack => String -> a
    error (String -> (SBV a, SBV a)) -> String -> (SBV a, SBV a)
    forall a b. (a -> b) -> a -> b
    $ "SBV.polyDivMod: Received infinite precision value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    x
       | Bool
    True
       = SBool -> (SBV a, SBV a) -> (SBV a, SBV a) -> (SBV a, SBV a)
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV a
    y SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 0) (0, SBV a
    x) ([SBool] -> SBV a
    adjust [SBool]
    d, [SBool] -> SBV a
    adjust [SBool]
    r)
       where adjust :: [SBool] -> SBV a
    adjust xs :: [SBool]
    xs = [SBool] -> SBV a
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsLE ([SBool] -> SBV a) -> [SBool] -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Int -> [SBool] -> [SBool]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Int
    sz ([SBool] -> [SBool]) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ [SBool]
    xs [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ SBool -> [SBool]
    forall a. a -> [a]
    repeat SBool
    sFalse
             sz :: Int
    sz        = SBV a -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBV a
    x
             (d :: [SBool]
    d, r :: [SBool]
    r)    = [SBool] -> [SBool] -> ([SBool], [SBool])
    mdp (SBV a -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastLE SBV a
    x) (SBV a -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastLE SBV a
    y)

    -- conservative over-approximation of the degree
    degree :: [SBool] -> Int
    degree :: [SBool] -> Int
    degree xs :: [SBool]
    xs = Int -> [SBool] -> Int
    forall t. Num t => t -> [SBool] -> t
    walk ([SBool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBool]
    xs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) ([SBool] -> Int) -> [SBool] -> Int
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> [SBool]
    forall a. [a] -> [a]
    reverse [SBool]
    xs
      where walk :: t -> [SBool] -> t
    walk n :: t
    n []     = t
    n
            walk n :: t
    n (b :: SBool
    b:bs :: [SBool]
    bs)
             | Just t :: Bool
    t <- SBool -> Maybe Bool
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBool
    b
             = if Bool
    t then t
    n else t -> [SBool] -> t
    walk (t
    nt -> t -> t
    forall a. Num a => a -> a -> a
    -1) [SBool]
    bs
             | Bool
    True
             = t
    n -- over-estimate

    -- | Compute modulus/remainder of polynomials on bit-vectors.
    mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
    mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
    mdp xs :: [SBool]
    xs ys :: [SBool]
    ys = Int -> [SBool] -> ([SBool], [SBool])
    go ([SBool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBool]
    ys Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) ([SBool] -> [SBool]
    forall a. [a] -> [a]
    reverse [SBool]
    ys)
      where degTop :: Int
    degTop  = [SBool] -> Int
    degree [SBool]
    xs
            go :: Int -> [SBool] -> ([SBool], [SBool])
    go _ []     = String -> ([SBool], [SBool])
    forall a. HasCallStack => String -> a
    error "SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"
            go n :: Int
    n (b :: SBool
    b:bs :: [SBool]
    bs)
             | Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0   = ([SBool] -> [SBool]
    forall a. [a] -> [a]
    reverse [SBool]
    qs, [SBool]
    rs)
             | Bool
    True     = let (rqs :: [SBool]
    rqs, rrs :: [SBool]
    rrs) = Int -> [SBool] -> ([SBool], [SBool])
    go (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) [SBool]
    bs
                          in (SBool -> [SBool] -> [SBool] -> [SBool]
    ites SBool
    b ([SBool] -> [SBool]
    forall a. [a] -> [a]
    reverse [SBool]
    qs) [SBool]
    rqs, SBool -> [SBool] -> [SBool] -> [SBool]
    ites SBool
    b [SBool]
    rs [SBool]
    rrs)
             where degQuot :: Int
    degQuot = Int
    degTop Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n
                   ys' :: [SBool]
    ys' = Int -> SBool -> [SBool]
    forall a. Int -> a -> [a]
    replicate Int
    degQuot SBool
    sFalse [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ [SBool]
    ys
                   (qs :: [SBool]
    qs, rs :: [SBool]
    rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
    divx (Int
    degQuotInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) Int
    degTop [SBool]
    xs [SBool]
    ys'

    -- return the element at index i; if not enough elements, return sFalse
    -- N.B. equivalent to '(xs ++ repeat sFalse) !! i', but more efficient
    idx :: [SBool] -> Int -> SBool
    idx :: [SBool] -> Int -> SBool
    idx []     _ = SBool
    sFalse
    idx (x :: SBool
    x:_)  0 = SBool
    x
    idx (_:xs :: [SBool]
    xs) i :: Int
    i = [SBool] -> Int -> SBool
    idx [SBool]
    xs (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1)

    divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
    divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
    divx n :: Int
    n _ xs :: [SBool]
    xs _ | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0 = ([], [SBool]
    xs)
    divx n :: Int
    n i :: Int
    i xs :: [SBool]
    xs ys' :: [SBool]
    ys'        = (SBool
    qSBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    :[SBool]
    qs, [SBool]
    rs)
      where q :: SBool
    q        = [SBool]
    xs [SBool] -> Int -> SBool
    `idx` Int
    i
            xs' :: [SBool]
    xs'      = SBool -> [SBool] -> [SBool] -> [SBool]
    ites SBool
    q ([SBool]
    xs [SBool] -> [SBool] -> [SBool]
    `addPoly` [SBool]
    ys') [SBool]
    xs
            (qs :: [SBool]
    qs, rs :: [SBool]
    rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
    divx (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) [SBool]
    xs' ([SBool] -> [SBool]
    forall a. [a] -> [a]
    tail [SBool]
    ys')

    -- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes
    -- the CRC of the message @m@ with respect to polynomial @p@. The
    -- inputs are assumed to be blasted big-endian. The number
    -- @n@ specifies how many bits of CRC is needed. Note that @n@
    -- is actually the degree of the polynomial @p@, and thus it seems
    -- redundant to pass it in. However, in a typical proof context,
    -- the polynomial can be symbolic, so we cannot compute the degree
    -- easily. While this can be worked-around by generating code that
    -- accounts for all possible degrees, the resulting code would
    -- be unnecessarily big and complicated, and much harder to reason
    -- with. (Also note that a CRC is just the remainder from the
    -- polynomial division, but this routine is much faster in practice.)
    --
    -- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC
    -- to be computed correctly. Note that the polynomial argument @p@ will
    -- not even have this bit present most of the time, as it will typically
    -- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher
    -- order @n@th bit is simply assumed to be set, as it does not make
    -- sense to use a polynomial of a lesser degree. This is usually not a problem
    -- since CRC polynomials are designed and expressed this way.
    --
    -- NB. The literature on CRC's has many variants on how CRC's are computed.
    -- We follow the following simple procedure:
    --
    --     * Extend the message @m@ by adding @n@ 0 bits on the right
    --
    --     * Divide the polynomial thus obtained by the @p@
    --
    --     * The remainder is the CRC value.
    --
    -- There are many variants on final XOR's, reversed polynomials etc., so
    -- it is essential to double check you use the correct /algorithm/.
    crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
    crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
    crcBV n :: Int
    n m :: [SBool]
    m p :: [SBool]
    p = Int -> [SBool] -> [SBool]
    forall a. Int -> [a] -> [a]
    take Int
    n ([SBool] -> [SBool]) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> [SBool] -> [SBool]
    go (Int -> SBool -> [SBool]
    forall a. Int -> a -> [a]
    replicate Int
    n SBool
    sFalse) ([SBool]
    m [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ Int -> SBool -> [SBool]
    forall a. Int -> a -> [a]
    replicate Int
    n SBool
    sFalse)
      where mask :: [SBool]
    mask = Int -> [SBool] -> [SBool]
    forall a. Int -> [a] -> [a]
    drop ([SBool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBool]
    p Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) [SBool]
    p
            go :: [SBool] -> [SBool] -> [SBool]
    go c :: [SBool]
    c []     = [SBool]
    c
            go c :: [SBool]
    c (b :: SBool
    b:bs :: [SBool]
    bs) = [SBool] -> [SBool] -> [SBool]
    go [SBool]
    next [SBool]
    bs
              where c' :: [SBool]
    c' = Int -> [SBool] -> [SBool]
    forall a. Int -> [a] -> [a]
    drop 1 [SBool]
    c [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ [SBool
    b]
                    next :: [SBool]
    next = SBool -> [SBool] -> [SBool] -> [SBool]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite ([SBool] -> SBool
    forall a. [a] -> a
    head [SBool]
    c) ((SBool -> SBool -> SBool) -> [SBool] -> [SBool] -> [SBool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SBool -> SBool -> SBool
    (.<+>) [SBool]
    c' [SBool]
    mask) [SBool]
    c'

    -- | Compute CRC's over polynomials, i.e., symbolic words. The first
    -- 'Int' argument plays the same role as the one in the 'crcBV' function.
    crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b
    crc :: Int -> SBV a -> SBV b -> SBV b
    crc n :: Int
    n m :: SBV a
    m p :: SBV b
    p
      | SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isReal SBV a
    m Bool -> Bool -> Bool
    || SBV b -> Bool
    forall a. HasKind a => a -> Bool
    isReal SBV b
    p
      = String -> SBV b
    forall a. HasCallStack => String -> a
    error (String -> SBV b) -> String -> SBV b
    forall a b. (a -> b) -> a -> b
    $ "SBV.crc: Received a real value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SBV a, SBV b) -> String
    forall a. Show a => a -> String
    show (SBV a
    m, SBV b
    p)
      | Bool -> Bool
    not (SBV a -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SBV a
    m) Bool -> Bool -> Bool
    || Bool -> Bool
    not (SBV b -> Bool
    forall a. HasKind a => a -> Bool
    isBounded SBV b
    p)
      = String -> SBV b
    forall a. HasCallStack => String -> a
    error (String -> SBV b) -> String -> SBV b
    forall a b. (a -> b) -> a -> b
    $ "SBV.crc: Received an infinite precision value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SBV a, SBV b) -> String
    forall a. Show a => a -> String
    show (SBV a
    m, SBV b
    p)
      | Bool
    True
      = [SBool] -> SBV b
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV b) -> [SBool] -> SBV b
    forall a b. (a -> b) -> a -> b
    $ Int -> SBool -> [SBool]
    forall a. Int -> a -> [a]
    replicate (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) SBool
    sFalse [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [SBool] -> [SBool] -> [SBool]
    crcBV Int
    n (SBV a -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SBV a
    m) (SBV b -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SBV b
    p)
      where sz :: Int
    sz = SBV b -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBV b
    p