{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}
module Data.SBV.Utils.PrettyNum (
PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI
, showCFloat, showCDouble, showHFloat, showHDouble, showBFloat, showFloatAtBase
, showSMTFloat, showSMTDouble, smtRoundingMode, cvToSMTLib, mkSkolemZero
, showNegativeNumber
) where
import Data.Bits ((.&.), countTrailingZeros)
import Data.Char (intToDigit, ord, chr, toUpper)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.List (isPrefixOf)
import Data.Maybe (fromJust, fromMaybe, listToMaybe)
import Data.Ratio (numerator, denominator)
import Data.Word (Word8, Word16, Word32, Word64)
import qualified Data.Set as Set
import Numeric (showIntAtBase, showHex, readInt, floatToDigits)
import qualified Numeric as N (showHFloat)
import Data.SBV.Core.Data
import Data.SBV.Core.Kind (smtType, smtRoundingMode, showBaseKind)
import Data.SBV.Core.AlgReals (algRealToSMTLib2)
import Data.SBV.Core.SizedFloats (fprToSMTLib2, bfToString)
import Data.SBV.Utils.Lib (stringToQFS)
class PrettyNum a where
hexS :: a -> String
binS :: a -> String
hexP :: a -> String
binP :: a -> String
hex :: a -> String
bin :: a -> String
instance PrettyNum Bool where
hexS :: Bool -> String
hexS = forall a. Show a => a -> String
show
binS :: Bool -> String
binS = forall a. Show a => a -> String
show
hexP :: Bool -> String
hexP = forall a. Show a => a -> String
show
binP :: Bool -> String
binP = forall a. Show a => a -> String
show
hex :: Bool -> String
hex = forall a. Show a => a -> String
show
bin :: Bool -> String
bin = forall a. Show a => a -> String
show
instance PrettyNum String where
hexS :: String -> String
hexS = forall a. Show a => a -> String
show
binS :: String -> String
binS = forall a. Show a => a -> String
show
hexP :: String -> String
hexP = forall a. Show a => a -> String
show
binP :: String -> String
binP = forall a. Show a => a -> String
show
hex :: String -> String
hex = forall a. Show a => a -> String
show
bin :: String -> String
bin = forall a. Show a => a -> String
show
instance PrettyNum Word8 where
hexS :: Word8 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, Int
8)
binS :: Word8 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, Int
8)
hexP :: Word8 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, Int
8)
binP :: Word8 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, Int
8)
hex :: Word8 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
8)
bin :: Word8 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
8)
instance PrettyNum Int8 where
hexS :: Int8 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, Int
8)
binS :: Int8 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, Int
8)
hexP :: Int8 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, Int
8)
binP :: Int8 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, Int
8)
hex :: Int8 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
8)
bin :: Int8 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
8)
instance PrettyNum Word16 where
hexS :: Word16 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, Int
16)
binS :: Word16 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, Int
16)
hexP :: Word16 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, Int
16)
binP :: Word16 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, Int
16)
hex :: Word16 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
16)
bin :: Word16 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
16)
instance PrettyNum Int16 where
hexS :: Int16 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, Int
16)
binS :: Int16 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, Int
16)
hexP :: Int16 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, Int
16)
binP :: Int16 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, Int
16)
hex :: Int16 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
16)
bin :: Int16 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
16)
instance PrettyNum Word32 where
hexS :: Word32 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, Int
32)
binS :: Word32 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, Int
32)
hexP :: Word32 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, Int
32)
binP :: Word32 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, Int
32)
hex :: Word32 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
32)
bin :: Word32 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
32)
instance PrettyNum Int32 where
hexS :: Int32 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, Int
32)
binS :: Int32 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, Int
32)
hexP :: Int32 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, Int
32)
binP :: Int32 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, Int
32)
hex :: Int32 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
32)
bin :: Int32 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
32)
instance PrettyNum Word64 where
hexS :: Word64 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, Int
64)
binS :: Word64 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, Int
64)
hexP :: Word64 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, Int
64)
binP :: Word64 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, Int
64)
hex :: Word64 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
64)
bin :: Word64 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
64)
instance PrettyNum Int64 where
hexS :: Int64 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, Int
64)
binS :: Int64 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, Int
64)
hexP :: Int64 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, Int
64)
binP :: Int64 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, Int
64)
hex :: Int64 -> String
hex = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
64)
bin :: Int64 -> String
bin = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
64)
instance PrettyNum Integer where
hexS :: Integer -> String
hexS = Bool -> Bool -> Integer -> String
shexI Bool
True Bool
True
binS :: Integer -> String
binS = Bool -> Bool -> Integer -> String
sbinI Bool
True Bool
True
hexP :: Integer -> String
hexP = Bool -> Bool -> Integer -> String
shexI Bool
False Bool
True
binP :: Integer -> String
binP = Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
True
hex :: Integer -> String
hex = Bool -> Bool -> Integer -> String
shexI Bool
False Bool
False
bin :: Integer -> String
bin = Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
False
shBKind :: HasKind a => a -> String
shBKind :: forall a. HasKind a => a -> String
shBKind a
a = String
" :: " forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (forall a. HasKind a => a -> Kind
kindOf a
a)
instance PrettyNum CV where
hexS :: CV -> String
hexS CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String -> String
shows CV
cv forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv) forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. RealFloat a => a -> String -> String
N.showHFloat Float
f forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. RealFloat a => a -> String -> String
N.showHFloat Double
d forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
True Bool
True FP
f forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
True Bool
True Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
binS :: CV -> String
binS CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String -> String
shows CV
cv forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv) forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat Float
f forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat Double
d forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
True Bool
True FP
f forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String -> String
shows AlgReal
r forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String -> String
shows String
s forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> String
shBKind CV
cv
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
True Bool
True Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
hexP :: CV -> String
hexP CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String
show CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
True Bool
True FP
f
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
True Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
binP :: CV -> String
binP CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String
show CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
True Bool
True FP
f
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
True Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
hex :: CV -> String
hex CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String
show CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
False Bool
True FP
f
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
False Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
bin :: CV -> String
bin CV
cv | forall a. HasKind a => a -> Bool
isUserSort CV
cv = forall a. Show a => a -> String
show CV
cv
| forall a. HasKind a => a -> Bool
isBoolean CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
| forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
| forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
| forall a. HasKind a => a -> Bool
isFP CV
cv = let CFP FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
False Bool
True FP
f
| forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
| forall a. HasKind a => a -> Bool
isString CV
cv = let CString String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
False Integer
i
| Bool
True = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
instance (SymVal a, PrettyNum a) => PrettyNum (SBV a) where
hexS :: SBV a -> String
hexS SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hexS :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
binS :: SBV a -> String
binS SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
binS :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
hexP :: SBV a -> String
hexP SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hexP :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
binP :: SBV a -> String
binP SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
binP :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
hex :: SBV a -> String
hex SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hex :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
bin :: SBV a -> String
bin SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
bin :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
shex :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
| a
a forall a. Ord a => a -> a -> Bool
< a
0
= String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (forall a. (Show a, Integral a) => a -> String
s16 (forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer))) forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (forall a. (Show a, Integral a) => a -> String
s16 a
a) forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = String
" :: " forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
| Bool
True = String
""
pre :: String
pre | Bool
shPre = String
"0x"
| Bool
True = String
""
l :: Int
l = (Int
size forall a. Num a => a -> a -> a
+ Int
3) forall a. Integral a => a -> a -> a
`div` Int
4
chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
chex :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
chex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
| Just String
s <- (Bool
signed, Int
size, forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Bool, Int, Integer), String)]
specials
= String
s
| Bool
True
= forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a forall a. [a] -> [a] -> [a]
++ String
suffix
where specials :: [((Bool, Int, Integer), String)]
specials :: [((Bool, Int, Integer), String)]
specials = [ ((Bool
True, Int
8, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int8)), String
"INT8_MIN" )
, ((Bool
True, Int
16, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int16)), String
"INT16_MIN")
, ((Bool
True, Int
32, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int32)), String
"INT32_MIN")
, ((Bool
True, Int
64, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int64)), String
"INT64_MIN")
]
suffix :: String
suffix = case (Bool
signed, Int
size) of
(Bool
False, Int
16) -> String
"U"
(Bool
False, Int
32) -> String
"UL"
(Bool
True, Int
32) -> String
"L"
(Bool
False, Int
64) -> String
"ULL"
(Bool
True, Int
64) -> String
"LL"
(Bool, Int)
_ -> String
""
shexI :: Bool -> Bool -> Integer -> String
shexI :: Bool -> Bool -> Integer -> String
shexI Bool
shType Bool
shPre Integer
a
| Integer
a forall a. Ord a => a -> a -> Bool
< Integer
0
= String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s16 (forall a. Num a => a -> a
abs Integer
a) forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s16 Integer
a forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = String
" :: Integer"
| Bool
True = String
""
pre :: String
pre | Bool
shPre = String
"0x"
| Bool
True = String
""
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
sbin :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
shType Bool
shPre (Bool
signed,Int
size) a
a
| a
a forall a. Ord a => a -> a -> Bool
< a
0
= String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (forall a. (Show a, Integral a) => a -> String
s2 (forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer))) forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (forall a. (Show a, Integral a) => a -> String
s2 a
a) forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = String
" :: " forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
| Bool
True = String
""
pre :: String
pre | Bool
shPre = String
"0b"
| Bool
True = String
""
sbinI :: Bool -> Bool -> Integer -> String
sbinI :: Bool -> Bool -> Integer -> String
sbinI Bool
shType Bool
shPre Integer
a
| Integer
a forall a. Ord a => a -> a -> Bool
< Integer
0
= String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s2 (forall a. Num a => a -> a
abs Integer
a) forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s2 Integer
a forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = String
" :: Integer"
| Bool
True = String
""
pre :: String
pre | Bool
shPre = String
"0b"
| Bool
True = String
""
pad :: Int -> String -> String
pad :: Int -> String -> String
pad Int
l String
s = forall a. Int -> a -> [a]
replicate (Int
l forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Char
'0' forall a. [a] -> [a] -> [a]
++ String
s
s2 :: (Show a, Integral a) => a -> String
s2 :: forall a. (Show a, Integral a) => a -> String
s2 a
v = forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase a
2 Int -> Char
dig a
v String
"" where dig :: Int -> Char
dig = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [(Int
0, Char
'0'), (Int
1, Char
'1')]
s16 :: (Show a, Integral a) => a -> String
s16 :: forall a. (Show a, Integral a) => a -> String
s16 a
v = forall a. (Integral a, Show a) => a -> String -> String
showHex a
v String
""
readBin :: Num a => String -> a
readBin :: forall a. Num a => String -> a
readBin (Char
'-':String
s) = -(forall a. Num a => String -> a
readBin String
s)
readBin String
s = case forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt a
2 Char -> Bool
isDigit Char -> Int
cvt String
s' of
[(a
a, String
"")] -> a
a
[(a, String)]
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.readBin: Cannot read a binary number from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
s
where cvt :: Char -> Int
cvt Char
c = Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
isDigit :: Char -> Bool
isDigit = (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01")
s' :: String
s' | String
"0b" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s = forall a. Int -> [a] -> [a]
drop Int
2 String
s
| Bool
True = String
s
showCFloat :: Float -> String
showCFloat :: Float -> String
showCFloat Float
f
| forall a. RealFloat a => a -> Bool
isNaN Float
f = String
"((float) NAN)"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((float) (-INFINITY))"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f = String
"((float) INFINITY)"
| Bool
True = forall a. RealFloat a => a -> String -> String
N.showHFloat Float
f forall a b. (a -> b) -> a -> b
$ String
"F /* " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Float
f forall a. [a] -> [a] -> [a]
++ String
"F */"
showCDouble :: Double -> String
showCDouble :: Double -> String
showCDouble Double
d
| forall a. RealFloat a => a -> Bool
isNaN Double
d = String
"((double) NAN)"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((double) (-INFINITY))"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d = String
"((double) INFINITY)"
| Bool
True = forall a. RealFloat a => a -> String -> String
N.showHFloat Double
d String
" /* " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Double
d forall a. [a] -> [a] -> [a]
++ String
" */"
showHFloat :: Float -> String
showHFloat :: Float -> String
showHFloat Float
f
| forall a. RealFloat a => a -> Bool
isNaN Float
f = String
"((0/0) :: Float)"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((-1/0) :: Float)"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f = String
"((1/0) :: Float)"
| Bool
True = forall a. Show a => a -> String
show Float
f
showHDouble :: Double -> String
showHDouble :: Double -> String
showHDouble Double
d
| forall a. RealFloat a => a -> Bool
isNaN Double
d = String
"((0/0) :: Double)"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((-1/0) :: Double)"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d = String
"((1/0) :: Double)"
| Bool
True = forall a. Show a => a -> String
show Double
d
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat RoundingMode
rm Float
f
| forall a. RealFloat a => a -> Bool
isNaN Float
f = String -> String
as String
"NaN"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String -> String
as String
"-oo"
| forall a. RealFloat a => a -> Bool
isInfinite Float
f = String -> String
as String
"+oo"
| forall a. RealFloat a => a -> Bool
isNegativeZero Float
f = String -> String
as String
"-zero"
| Float
f forall a. Eq a => a -> a -> Bool
== Float
0 = String -> String
as String
"+zero"
| Bool
True = String
"((_ to_fp 8 24) " forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (forall a. Real a => a -> Rational
toRational Float
f) forall a. [a] -> [a] -> [a]
++ String
")"
where as :: String -> String
as String
s = String
"(_ " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" 8 24)"
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble RoundingMode
rm Double
d
| forall a. RealFloat a => a -> Bool
isNaN Double
d = String -> String
as String
"NaN"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String -> String
as String
"-oo"
| forall a. RealFloat a => a -> Bool
isInfinite Double
d = String -> String
as String
"+oo"
| forall a. RealFloat a => a -> Bool
isNegativeZero Double
d = String -> String
as String
"-zero"
| Double
d forall a. Eq a => a -> a -> Bool
== Double
0 = String -> String
as String
"+zero"
| Bool
True = String
"((_ to_fp 11 53) " forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (forall a. Real a => a -> Rational
toRational Double
d) forall a. [a] -> [a] -> [a]
++ String
")"
where as :: String -> String
as String
s = String
"(_ " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" 11 53)"
showSMTRational :: Rational -> String
showSMTRational :: Rational -> String
showSMTRational Rational
r = String
"(SBV.Rational " forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (forall a. Ratio a -> a
numerator Rational
r) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (forall a. Ratio a -> a
denominator Rational
r) forall a. [a] -> [a] -> [a]
++ String
")"
toSMTLibRational :: Rational -> String
toSMTLibRational :: Rational -> String
toSMTLibRational Rational
r
| Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0
= String
"(- (/ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs Integer
n) forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
d forall a. [a] -> [a] -> [a]
++ String
".0))"
| Bool
True
= String
"(/ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
d forall a. [a] -> [a] -> [a]
++ String
".0)"
where n :: Integer
n = forall a. Ratio a -> a
numerator Rational
r
d :: Integer
d = forall a. Ratio a -> a
denominator Rational
r
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm CV
x
| forall a. HasKind a => a -> Bool
isBoolean CV
x, CInteger Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0 then String
"false" else String
"true"
| forall a. HasKind a => a -> Bool
isUserSort CV
x, CUserSort (Maybe Int
_, String
s) <- CV -> CVal
cvVal CV
x = String -> String
roundModeConvert String
s
| forall a. HasKind a => a -> Bool
isReal CV
x, CAlgReal AlgReal
r <- CV -> CVal
cvVal CV
x = AlgReal -> String
algRealToSMTLib2 AlgReal
r
| forall a. HasKind a => a -> Bool
isFloat CV
x, CFloat Float
f <- CV -> CVal
cvVal CV
x = RoundingMode -> Float -> String
showSMTFloat RoundingMode
rm Float
f
| forall a. HasKind a => a -> Bool
isDouble CV
x, CDouble Double
d <- CV -> CVal
cvVal CV
x = RoundingMode -> Double -> String
showSMTDouble RoundingMode
rm Double
d
| forall a. HasKind a => a -> Bool
isRational CV
x, CRational Rational
r <- CV -> CVal
cvVal CV
x = Rational -> String
showSMTRational Rational
r
| forall a. HasKind a => a -> Bool
isFP CV
x, CFP FP
f <- CV -> CVal
cvVal CV
x = FP -> String
fprToSMTLib2 FP
f
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
x), CInteger Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Ord a => a -> a -> Bool
>= Integer
0 then forall a. Show a => a -> String
show Integer
w else String
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs Integer
w) forall a. [a] -> [a] -> [a]
++ String
")"
| Bool -> Bool
not (forall a. HasKind a => a -> Bool
hasSign CV
x) , CInteger Integer
w <- CV -> CVal
cvVal CV
x = Int -> Integer -> String
smtLibHex (forall a. HasKind a => a -> Int
intSizeOf CV
x) Integer
w
| forall a. HasKind a => a -> Bool
hasSign CV
x , CInteger Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Eq a => a -> a -> Bool
== forall a. Num a => a -> a
negate (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. HasKind a => a -> Int
intSizeOf CV
x)
then Int -> String
mkMinBound (forall a. HasKind a => a -> Int
intSizeOf CV
x)
else Bool -> String -> String
negIf (Integer
w forall a. Ord a => a -> a -> Bool
< Integer
0) forall a b. (a -> b) -> a -> b
$ Int -> Integer -> String
smtLibHex (forall a. HasKind a => a -> Int
intSizeOf CV
x) (forall a. Num a => a -> a
abs Integer
w)
| forall a. HasKind a => a -> Bool
isChar CV
x , CChar Char
c <- CV -> CVal
cvVal CV
x = String
"(_ char " forall a. [a] -> [a] -> [a]
++ Int -> Integer -> String
smtLibHex Int
8 (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
c)) forall a. [a] -> [a] -> [a]
++ String
")"
| forall a. HasKind a => a -> Bool
isString CV
x , CString String
s <- CV -> CVal
cvVal CV
x = Char
'\"' forall a. a -> [a] -> [a]
: String -> String
stringToQFS String
s forall a. [a] -> [a] -> [a]
++ String
"\""
| forall a. HasKind a => a -> Bool
isList CV
x , CList [CVal]
xs <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibSeq (forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
| forall a. HasKind a => a -> Bool
isSet CV
x , CSet RCSet CVal
s <- CV -> CVal
cvVal CV
x = Kind -> RCSet CVal -> String
smtLibSet (forall a. HasKind a => a -> Kind
kindOf CV
x) RCSet CVal
s
| forall a. HasKind a => a -> Bool
isTuple CV
x , CTuple [CVal]
xs <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibTup (forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
| forall a. HasKind a => a -> Bool
isMaybe CV
x , CMaybe Maybe CVal
mc <- CV -> CVal
cvVal CV
x = Kind -> Maybe CVal -> String
smtLibMaybe (forall a. HasKind a => a -> Kind
kindOf CV
x) Maybe CVal
mc
| forall a. HasKind a => a -> Bool
isEither CV
x , CEither Either CVal CVal
ec <- CV -> CVal
cvVal CV
x = Kind -> Either CVal CVal -> String
smtLibEither (forall a. HasKind a => a -> Kind
kindOf CV
x) Either CVal CVal
ec
| Bool
True = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvtCV: Impossible happened: Kind/Value disagreement on: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Kind
kindOf CV
x, CV
x)
where roundModeConvert :: String -> String
roundModeConvert String
s = forall a. a -> Maybe a -> a
fromMaybe String
s (forall a. [a] -> Maybe a
listToMaybe [RoundingMode -> String
smtRoundingMode RoundingMode
m | RoundingMode
m <- [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound] :: [RoundingMode], forall a. Show a => a -> String
show RoundingMode
m forall a. Eq a => a -> a -> Bool
== String
s])
smtLibHex :: Int -> Integer -> String
smtLibHex :: Int -> Integer -> String
smtLibHex Int
1 Integer
v = String
"#b" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
v
smtLibHex Int
sz Integer
v
| Int
sz forall a. Integral a => a -> a -> a
`mod` Int
4 forall a. Eq a => a -> a -> Bool
== Int
0 = String
"#x" forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad (Int
sz forall a. Integral a => a -> a -> a
`div` Int
4) (forall a. (Integral a, Show a) => a -> String -> String
showHex Integer
v String
"")
| Bool
True = String
"#b" forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
sz (Integer -> String -> String
showBin Integer
v String
"")
where showBin :: Integer -> String -> String
showBin = forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase Integer
2 Int -> Char
intToDigit
negIf :: Bool -> String -> String
negIf :: Bool -> String -> String
negIf Bool
True String
a = String
"(bvneg " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
")"
negIf Bool
False String
a = String
a
smtLibSeq :: Kind -> [CVal] -> String
smtLibSeq :: Kind -> [CVal] -> String
smtLibSeq Kind
k [] = String
"(as seq.empty " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k forall a. [a] -> [a] -> [a]
++ String
")"
smtLibSeq (KList Kind
ek) [CVal]
xs = let mkSeq :: [String] -> String
mkSeq [String
e] = String
e
mkSeq [String]
es = String
"(seq.++ " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
es forall a. [a] -> [a] -> [a]
++ String
")"
mkUnit :: String -> String
mkUnit String
inner = String
"(seq.unit " forall a. [a] -> [a] -> [a]
++ String
inner forall a. [a] -> [a] -> [a]
++ String
")"
in [String] -> String
mkSeq (String -> String
mkUnit forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ek forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CVal]
xs)
smtLibSeq Kind
k [CVal]
_ = forall a. HasCallStack => String -> a
error String
"SBV.cvToSMTLib: Impossible case (smtLibSeq), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
smtLibSet :: Kind -> RCSet CVal -> String
smtLibSet :: Kind -> RCSet CVal -> String
smtLibSet Kind
k RCSet CVal
set = case RCSet CVal
set of
RegularSet Set CVal
rs -> forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify String
"true") (String -> String
start String
"false") Set CVal
rs
ComplementSet Set CVal
rs -> forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify String
"false") (String -> String
start String
"true") Set CVal
rs
where ke :: Kind
ke = case Kind
k of
KSet Kind
ek -> Kind
ek
Kind
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibSet), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
start :: String -> String
start String
def = String
"((as const " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
def forall a. [a] -> [a] -> [a]
++ String
")"
modify :: String -> CVal -> String -> String
modify String
how CVal
e String
s = String
"(store " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ke CVal
e) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
how forall a. [a] -> [a] -> [a]
++ String
")"
smtLibTup :: Kind -> [CVal] -> String
smtLibTup :: Kind -> [CVal] -> String
smtLibTup (KTuple []) [CVal]
_ = String
"mkSBVTuple0"
smtLibTup (KTuple [Kind]
ks) [CVal]
xs = String
"(mkSBVTuple" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Kind
ek CVal
e -> RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ek CVal
e)) [Kind]
ks [CVal]
xs) forall a. [a] -> [a] -> [a]
++ String
")"
smtLibTup Kind
k [CVal]
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibTup), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
dtConstructor :: String -> [String] -> Kind -> String
dtConstructor String
fld [] Kind
res = String
"(as " forall a. [a] -> [a] -> [a]
++ String
fld forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res forall a. [a] -> [a] -> [a]
++ String
")"
dtConstructor String
fld [String]
args Kind
res = String
"((as " forall a. [a] -> [a] -> [a]
++ String
fld forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args forall a. [a] -> [a] -> [a]
++ String
")"
smtLibMaybe :: Kind -> Maybe CVal -> String
smtLibMaybe :: Kind -> Maybe CVal -> String
smtLibMaybe km :: Kind
km@KMaybe{} Maybe CVal
Nothing = String -> [String] -> Kind -> String
dtConstructor String
"nothing_SBVMaybe" [] Kind
km
smtLibMaybe km :: Kind
km@(KMaybe Kind
k) (Just CVal
c) = String -> [String] -> Kind -> String
dtConstructor String
"just_SBVMaybe" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
km
smtLibMaybe Kind
k Maybe CVal
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibMaybe), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
smtLibEither :: Kind -> Either CVal CVal -> String
smtLibEither :: Kind -> Either CVal CVal -> String
smtLibEither ke :: Kind
ke@(KEither Kind
k Kind
_) (Left CVal
c) = String -> [String] -> Kind -> String
dtConstructor String
"left_SBVEither" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
smtLibEither ke :: Kind
ke@(KEither Kind
_ Kind
k) (Right CVal
c) = String -> [String] -> Kind -> String
dtConstructor String
"right_SBVEither" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
smtLibEither Kind
k Either CVal CVal
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibEither), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
mkMinBound :: Int -> String
mkMinBound :: Int -> String
mkMinBound Int
i = String
"#b1" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
iforall a. Num a => a -> a -> a
-Int
1) Char
'0'
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero RoundingMode
_ (KUserSort String
_ (Just (String
f:[String]
_))) = String
f
mkSkolemZero RoundingMode
_ (KUserSort String
s Maybe [String]
_) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.mkSkolemZero: Unexpected user sort: " forall a. [a] -> [a] -> [a]
++ String
s
mkSkolemZero RoundingMode
rm Kind
k = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
0::Integer))
showBFloat :: (Show a, RealFloat a) => a -> ShowS
showBFloat :: forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat = forall a. (Show a, RealFloat a) => Int -> a -> String -> String
showFloatAtBase Int
2
showFloatAtBase :: (Show a, RealFloat a) => Int -> a -> ShowS
showFloatAtBase :: forall a. (Show a, RealFloat a) => Int -> a -> String -> String
showFloatAtBase Int
base a
input
| Int
base forall a. Ord a => a -> a -> Bool
< Int
2 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"showFloatAtBase: Received invalid base (must be >= 2): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
base
| Bool
True = String -> String -> String
showString forall a b. (a -> b) -> a -> b
$ forall {a}. RealFloat a => a -> String
fmt a
input
where fmt :: a -> String
fmt a
x
| forall a. RealFloat a => a -> Bool
isNaN a
x = String
"NaN"
| forall a. RealFloat a => a -> Bool
isInfinite a
x = (if a
x forall a. Ord a => a -> a -> Bool
< a
0 then String
"-" else String
"") forall a. [a] -> [a] -> [a]
++ String
"Infinity"
| a
x forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isNegativeZero a
x = Char
'-' forall a. a -> [a] -> [a]
: forall {a}. RealFloat a => a -> String
cvt (-a
x)
| Bool
True = forall {a}. RealFloat a => a -> String
cvt a
x
basePow2 :: Bool
basePow2 = Int
base forall a. Bits a => a -> a -> a
.&. (Int
baseforall a. Num a => a -> a -> a
-Int
1) forall a. Eq a => a -> a -> Bool
== Int
0
lg2Base :: Int
lg2Base = forall b. FiniteBits b => b -> Int
countTrailingZeros Int
base
prefix :: String
prefix = case Int
base of
Int
2 -> String
"0b"
Int
8 -> String
"0o"
Int
10 -> String
""
Int
16 -> String
"0x"
Int
x -> String
"0<" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
x forall a. [a] -> [a] -> [a]
++ String
">"
powChar :: Char
powChar
| Int
base forall a. Eq a => a -> a -> Bool
== Int
10 = Char
'e'
| Bool
basePow2 = Char
'p'
| Bool
True = Char
'@'
f2d :: a -> (Int, [Int], Int)
f2d a
x = case forall a. RealFloat a => Integer -> a -> ([Int], Int)
floatToDigits (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
base) a
x of
([], Int
e) -> (Int
0, [], Int
e forall a. Num a => a -> a -> a
- Int
1)
(Int
d:[Int]
ds, Int
e) -> (Int
d, [Int]
ds, Int
e forall a. Num a => a -> a -> a
- Int
1)
cvt :: a -> String
cvt a
x
| a
x forall a. Eq a => a -> a -> Bool
== a
0 = String
prefix forall a. [a] -> [a] -> [a]
++ Char
'0' forall a. a -> [a] -> [a]
: Char
powChar forall a. a -> [a] -> [a]
: String
"+0"
| Bool
True = String
prefix forall a. [a] -> [a] -> [a]
++ Int -> String
toDigit Int
d forall a. [a] -> [a] -> [a]
++ forall {t :: * -> *}. Foldable t => t Int -> String
frac [Int]
ds forall a. [a] -> [a] -> [a]
++ String
pow
where (Int
d, [Int]
ds, Int
e) = forall {a}. RealFloat a => a -> (Int, [Int], Int)
f2d a
x
pow :: String
pow
| Int
base forall a. Eq a => a -> a -> Bool
== Int
10 = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned Int
e
| Bool
basePow2 = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned (Int
e forall a. Num a => a -> a -> a
* Int
lg2Base)
| Bool
True = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned Int
e
shSigned :: a -> String
shSigned a
v
| a
v forall a. Ord a => a -> a -> Bool
< a
0 = forall a. Show a => a -> String
show a
v
| Bool
True = Char
'+' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show a
v
frac :: t Int -> String
frac t Int
digits
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== Int
0) t Int
digits = String
""
| Bool
True = String
"." forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> String
toDigit t Int
digits
toDigit :: Int -> String
toDigit Int
v = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
d
where d :: String
d | Int
v forall a. Ord a => a -> a -> Bool
<= Int
15 = [Int -> Char
intToDigit Int
v]
| Int
v forall a. Ord a => a -> a -> Bool
< Int
36 = [Int -> Char
chr (Char -> Int
ord Char
'a' forall a. Num a => a -> a -> a
+ Int
v forall a. Num a => a -> a -> a
- Int
10)]
| Bool
True = Char
'<' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
v forall a. [a] -> [a] -> [a]
++ String
">"
showNegativeNumber :: (Show a, Num a, Ord a) => a -> String
showNegativeNumber :: forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber a
i
| a
i forall a. Ord a => a -> a -> Bool
< a
0 = String
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (-a
i) forall a. [a] -> [a] -> [a]
++ String
")"
| Bool
True = forall a. Show a => a -> String
show a
i