{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Tools.Polynomial (
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.Kind
import Data.SBV.Core.Sized
import Data.SBV.Core.Model
import GHC.TypeLits
class (Num a, Bits a) => Polynomial a where
polynomial :: [Int] -> a
pAdd :: a -> a -> a
pMult :: (a, a, [Int]) -> a
pDiv :: a -> a -> a
pMod :: a -> a -> a
pDivMod :: a -> a -> (a, a)
showPoly :: a -> String
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) a
0
pAdd = a -> a -> a
forall a. Bits a => a -> a -> a
xor
pDiv a
x 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 a
x 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 = ((SWord8, SWord8, [Int]) -> SWord8)
-> (Word8, Word8, [Int]) -> Word8
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SWord8, SWord8, [Int]) -> SWord8
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word8 -> Word8 -> (Word8, Word8)
pDivMod = (SWord8 -> SWord8 -> (SWord8, SWord8))
-> Word8 -> Word8 -> (Word8, Word8)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SWord8 -> SWord8 -> (SWord8, SWord8)
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 = ((SWord16, SWord16, [Int]) -> SWord16)
-> (Word16, Word16, [Int]) -> Word16
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SWord16, SWord16, [Int]) -> SWord16
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word16 -> Word16 -> (Word16, Word16)
pDivMod = (SWord16 -> SWord16 -> (SWord16, SWord16))
-> Word16 -> Word16 -> (Word16, Word16)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SWord16 -> SWord16 -> (SWord16, SWord16)
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 = ((SWord32, SWord32, [Int]) -> SWord32)
-> (Word32, Word32, [Int]) -> Word32
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SWord32, SWord32, [Int]) -> SWord32
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word32 -> Word32 -> (Word32, Word32)
pDivMod = (SWord32 -> SWord32 -> (SWord32, SWord32))
-> Word32 -> Word32 -> (Word32, Word32)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SWord32 -> SWord32 -> (SWord32, SWord32)
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 = ((SWord64, SWord64, [Int]) -> SWord64)
-> (Word64, Word64, [Int]) -> Word64
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SWord64, SWord64, [Int]) -> SWord64
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word64 -> Word64 -> (Word64, Word64)
pDivMod = (SWord64 -> SWord64 -> (SWord64, SWord64))
-> Word64 -> Word64 -> (Word64, Word64)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SWord64 -> SWord64 -> (SWord64, SWord64)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord8 where {showPolynomial :: Bool -> SWord8 -> String
showPolynomial Bool
b = (Word8 -> String) -> SWord8 -> 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 :: (SWord8, SWord8, [Int]) -> SWord8
pMult = (SWord8, SWord8, [Int]) -> SWord8
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)
pDivMod = SWord8 -> SWord8 -> (SWord8, SWord8)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord16 where {showPolynomial :: Bool -> SWord16 -> String
showPolynomial Bool
b = (Word16 -> String) -> SWord16 -> 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 :: (SWord16, SWord16, [Int]) -> SWord16
pMult = (SWord16, SWord16, [Int]) -> SWord16
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)
pDivMod = SWord16 -> SWord16 -> (SWord16, SWord16)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord32 where {showPolynomial :: Bool -> SWord32 -> String
showPolynomial Bool
b = (Word32 -> String) -> SWord32 -> 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 :: (SWord32, SWord32, [Int]) -> SWord32
pMult = (SWord32, SWord32, [Int]) -> SWord32
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)
pDivMod = SWord32 -> SWord32 -> (SWord32, SWord32)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord64 where {showPolynomial :: Bool -> SWord64 -> String
showPolynomial Bool
b = (Word64 -> String) -> SWord64 -> 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 :: (SWord64, SWord64, [Int]) -> SWord64
pMult = (SWord64, SWord64, [Int]) -> SWord64
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)
pDivMod = SWord64 -> SWord64 -> (SWord64, SWord64)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance (KnownNat n, BVIsNonZero n) => Polynomial (SWord n) where {showPolynomial :: Bool -> SWord n -> String
showPolynomial 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 :: forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV a, SBV a, [Int]) -> SBV a
f (a
x, a
y, [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 :: forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV a -> SBV a -> (SBV a, SBV a)
f a
x a
y = let (SBV a
a, 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 :: forall a. SymVal a => (a -> String) -> SBV a -> String
liftS a -> String
f SBV a
s
| Just 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
sp :: Bits a => Bool -> a -> String
sp :: forall a. Bits a => Bool -> a -> String
sp Bool
st a
a
| [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
cs = Char
'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 (\Int
x 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 -> 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 = String
" :: 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]
++ String
")"
| Bool
True = String
""
n :: Int
n = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
"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
-Int
1, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2 .. Int
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 a
0 = String
"1"
sh a
1 = String
"x"
sh a
i = String
"x^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
addPoly :: [SBool] -> [SBool] -> [SBool]
addPoly :: [SBool] -> [SBool] -> [SBool]
addPoly [SBool]
xs [] = [SBool]
xs
addPoly [] [SBool]
ys = [SBool]
ys
addPoly (SBool
x:[SBool]
xs) (SBool
y:[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
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
s [SBool]
xs [SBool]
ys
| Just 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 [] (SBool
b:[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 (SBool
a:[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 (SBool
a:[SBool]
as) (SBool
b:[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
polyMult :: SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult :: forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult (SBV a
x, SBV a
y, [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
$ String
"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
$ String
"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 ([SBool]
_, [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 (Int
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 (Int
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 <- [Int
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 Int
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 [SBool]
_ [] [SBool]
ps = [SBool]
ps
mul [SBool]
as (SBool
b:[SBool]
bs) [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 :: forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod SBV a
x 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
$ String
"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
$ String
"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
.== SBV a
0) (SBV a
0, SBV a
x) ([SBool] -> SBV a
adjust [SBool]
d, [SBool] -> SBV a
adjust [SBool]
r)
where adjust :: [SBool] -> SBV a
adjust [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
([SBool]
d, [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)
degree :: [SBool] -> Int
degree :: [SBool] -> Int
degree [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
- Int
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 t
n [] = t
n
walk t
n (SBool
b:[SBool]
bs)
| Just 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
-t
1) [SBool]
bs
| Bool
True
= t
n
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
mdp [SBool]
xs [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
- Int
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 Int
_ [] = String -> ([SBool], [SBool])
forall a. HasCallStack => String -> a
error String
"SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"
go Int
n (SBool
b:[SBool]
bs)
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
qs, [SBool]
rs)
| Bool
True = let ([SBool]
rqs, [SBool]
rrs) = Int -> [SBool] -> ([SBool], [SBool])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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
([SBool]
qs, [SBool]
rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx (Int
degQuotInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
degTop [SBool]
xs [SBool]
ys'
idx :: [SBool] -> Int -> SBool
idx :: [SBool] -> Int -> SBool
idx [] Int
_ = SBool
sFalse
idx (SBool
x:[SBool]
_) Int
0 = SBool
x
idx (SBool
_:[SBool]
xs) Int
i = [SBool] -> Int -> SBool
idx [SBool]
xs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx Int
n Int
_ [SBool]
xs [SBool]
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = ([], [SBool]
xs)
divx Int
n Int
i [SBool]
xs [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
([SBool]
qs, [SBool]
rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBool]
xs' ([SBool] -> [SBool]
forall a. [a] -> [a]
tail [SBool]
ys')
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
crcBV Int
n [SBool]
m [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 [SBool]
c [] = [SBool]
c
go [SBool]
c (SBool
b:[SBool]
bs) = [SBool] -> [SBool] -> [SBool]
go [SBool]
next [SBool]
bs
where c' :: [SBool]
c' = Int -> [SBool] -> [SBool]
forall a. Int -> [a] -> [a]
drop Int
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'
crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b
crc :: forall a b.
(SFiniteBits a, SFiniteBits b) =>
Int -> SBV a -> SBV b -> SBV b
crc Int
n SBV a
m 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
$ String
"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
$ String
"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