{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Utils.PrettyNum (
PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI
, showCFloat, showCDouble, showHFloat, showHDouble
, showSMTFloat, showSMTDouble, smtRoundingMode, cvToSMTLib, mkSkolemZero
) where
import Data.Char (intToDigit, ord)
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)
import qualified Numeric (showHFloat)
import Data.Numbers.CrackNum (floatToFP, doubleToFP)
import Data.SBV.Core.Data
import Data.SBV.Core.Kind (smtType)
import Data.SBV.Core.AlgReals (algRealToSMTLib2)
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 = Bool -> String
forall a. Show a => a -> String
show
binS :: Bool -> String
binS = Bool -> String
forall a. Show a => a -> String
show
hexP :: Bool -> String
hexP = Bool -> String
forall a. Show a => a -> String
show
binP :: Bool -> String
binP = Bool -> String
forall a. Show a => a -> String
show
hex :: Bool -> String
hex = Bool -> String
forall a. Show a => a -> String
show
bin :: Bool -> String
bin = Bool -> String
forall a. Show a => a -> String
show
instance PrettyNum String where
hexS :: String -> String
hexS = String -> String
forall a. Show a => a -> String
show
binS :: String -> String
binS = String -> String
forall a. Show a => a -> String
show
hexP :: String -> String
hexP = String -> String
forall a. Show a => a -> String
show
binP :: String -> String
binP = String -> String
forall a. Show a => a -> String
show
hex :: String -> String
hex = String -> String
forall a. Show a => a -> String
show
bin :: String -> String
bin = String -> String
forall a. Show a => a -> String
show
instance PrettyNum Word8 where
hexS :: Word8 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, 8)
binS :: Word8 -> String
binS = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, 8)
hexP :: Word8 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, 8)
binP :: Word8 -> String
binP = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, 8)
hex :: Word8 -> String
hex = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, 8)
bin :: Word8 -> String
bin = Bool -> Bool -> (Bool, Int) -> Word8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, 8)
instance PrettyNum Int8 where
hexS :: Int8 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, 8)
binS :: Int8 -> String
binS = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, 8)
hexP :: Int8 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, 8)
binP :: Int8 -> String
binP = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, 8)
hex :: Int8 -> String
hex = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, 8)
bin :: Int8 -> String
bin = Bool -> Bool -> (Bool, Int) -> Int8 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, 8)
instance PrettyNum Word16 where
hexS :: Word16 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, 16)
binS :: Word16 -> String
binS = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, 16)
hexP :: Word16 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, 16)
binP :: Word16 -> String
binP = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, 16)
hex :: Word16 -> String
hex = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, 16)
bin :: Word16 -> String
bin = Bool -> Bool -> (Bool, Int) -> Word16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, 16)
instance PrettyNum Int16 where
hexS :: Int16 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, 16)
binS :: Int16 -> String
binS = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, 16)
hexP :: Int16 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, 16)
binP :: Int16 -> String
binP = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, 16)
hex :: Int16 -> String
hex = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, 16)
bin :: Int16 -> String
bin = Bool -> Bool -> (Bool, Int) -> Int16 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, 16)
instance PrettyNum Word32 where
hexS :: Word32 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, 32)
binS :: Word32 -> String
binS = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, 32)
hexP :: Word32 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, 32)
binP :: Word32 -> String
binP = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, 32)
hex :: Word32 -> String
hex = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, 32)
bin :: Word32 -> String
bin = Bool -> Bool -> (Bool, Int) -> Word32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, 32)
instance PrettyNum Int32 where
hexS :: Int32 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, 32)
binS :: Int32 -> String
binS = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, 32)
hexP :: Int32 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, 32)
binP :: Int32 -> String
binP = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, 32)
hex :: Int32 -> String
hex = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, 32)
bin :: Int32 -> String
bin = Bool -> Bool -> (Bool, Int) -> Int32 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, 32)
instance PrettyNum Word64 where
hexS :: Word64 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
False, 64)
binS :: Word64 -> String
binS = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
False, 64)
hexP :: Word64 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
False, 64)
binP :: Word64 -> String
binP = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
False, 64)
hex :: Word64 -> String
hex = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, 64)
bin :: Word64 -> String
bin = Bool -> Bool -> (Bool, Int) -> Word64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, 64)
instance PrettyNum Int64 where
hexS :: Int64 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (Bool
True, 64)
binS :: Int64 -> String
binS = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (Bool
True, 64)
hexP :: Int64 -> String
hexP = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (Bool
True, 64)
binP :: Int64 -> String
binP = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (Bool
True, 64)
hex :: Int64 -> String
hex = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, 64)
bin :: Int64 -> String
bin = Bool -> Bool -> (Bool, Int) -> Int64 -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, 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
instance PrettyNum CV where
hexS :: CV -> String
hexS cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Bool"
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Float\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FP -> String
forall a. Show a => a -> String
show (Float -> FP
floatToFP Float
f)
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Double\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FP -> String
forall a. Show a => a -> String
show (Double -> FP
doubleToFP Double
d)
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Real"
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: String"
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
True Bool
True Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True Bool
True (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
binS :: CV -> String
binS cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Bool"
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Float\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FP -> String
forall a. Show a => a -> String
show (Float -> FP
floatToFP Float
f)
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Double\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FP -> String
forall a. Show a => a -> String
show (Double -> FP
doubleToFP Double
d)
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: Real"
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: String"
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
True Bool
True Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True Bool
True (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
hexP :: CV -> String
hexP cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
True Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
binP :: CV -> String
binP cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
True Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
hex :: CV -> String
hex cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
False Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i
bin :: CV -> String
bin cv :: CV
cv | CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
cv = let CFloat f :: Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
cv = let CDouble d :: Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
cv = let CAlgReal r :: AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
cv = let CString s :: String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
False Integer
i
| Bool
True = let CInteger i :: Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
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 s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
hexS :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
binS :: SBV a -> String
binS s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
binS :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
hexP :: SBV a -> String
hexP s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
hexP :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
binP :: SBV a -> String
binP s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
binP :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
hex :: SBV a -> String
hex s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
hex :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
bin :: SBV a -> String
bin s :: SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
bin :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
shex :: Bool -> Bool -> (Bool, Int) -> a -> String
shex shType :: Bool
shType shPre :: Bool
shPre (signed :: Bool
signed, size :: Int
size) a :: a
a
| a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0
= "-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 (Integer -> Integer
forall a. Num a => a -> a
abs (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer))) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (a -> String
forall a. (Show a, Integral a) => a -> String
s16 a
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
signed then "Int" else "Word") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
size
| Bool
True = ""
pre :: String
pre | Bool
shPre = "0x"
| Bool
True = ""
l :: Int
l = (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 4
chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
chex :: Bool -> Bool -> (Bool, Int) -> a -> String
chex shType :: Bool
shType shPre :: Bool
shPre (signed :: Bool
signed, size :: Int
size) a :: a
a
| Just s :: String
s <- (Bool
signed, Int
size, a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (Bool, Int, Integer)
-> [((Bool, Int, Integer), String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Bool, Int, Integer), String)]
specials
= String
s
| Bool
True
= Bool -> Bool -> (Bool, Int) -> a -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suffix
where specials :: [((Bool, Int, Integer), String)]
specials :: [((Bool, Int, Integer), String)]
specials = [ ((Bool
True, 8, Int8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int8
forall a. Bounded a => a
minBound :: Int8)), "INT8_MIN" )
, ((Bool
True, 16, Int16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int16
forall a. Bounded a => a
minBound :: Int16)), "INT16_MIN")
, ((Bool
True, 32, Int32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32
forall a. Bounded a => a
minBound :: Int32)), "INT32_MIN")
, ((Bool
True, 64, Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
forall a. Bounded a => a
minBound :: Int64)), "INT64_MIN")
]
suffix :: String
suffix = case (Bool
signed, Int
size) of
(False, 16) -> "U"
(False, 32) -> "UL"
(True, 32) -> "L"
(False, 64) -> "ULL"
(True, 64) -> "LL"
_ -> ""
shexI :: Bool -> Bool -> Integer -> String
shexI :: Bool -> Bool -> Integer -> String
shexI shType :: Bool
shType shPre :: Bool
shPre a :: Integer
a
| Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0
= "-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 (Integer -> Integer
forall a. Num a => a -> a
abs Integer
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 Integer
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = " :: Integer"
| Bool
True = ""
pre :: String
pre | Bool
shPre = "0x"
| Bool
True = ""
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
sbin :: Bool -> Bool -> (Bool, Int) -> a -> String
sbin shType :: Bool
shType shPre :: Bool
shPre (signed :: Bool
signed,size :: Int
size) a :: a
a
| a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0
= "-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 (Integer -> Integer
forall a. Num a => a -> a
abs (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer))) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (a -> String
forall a. (Show a, Integral a) => a -> String
s2 a
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
signed then "Int" else "Word") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
size
| Bool
True = ""
pre :: String
pre | Bool
shPre = "0b"
| Bool
True = ""
sbinI :: Bool -> Bool -> Integer -> String
sbinI :: Bool -> Bool -> Integer -> String
sbinI shType :: Bool
shType shPre :: Bool
shPre a :: Integer
a
| Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0
= "-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 (Integer -> Integer
forall a. Num a => a -> a
abs Integer
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
| Bool
True
= String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 Integer
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t | Bool
shType = " :: Integer"
| Bool
True = ""
pre :: String
pre | Bool
shPre = "0b"
| Bool
True = ""
pad :: Int -> String -> String
pad :: Int -> String -> String
pad l :: Int
l s :: String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) '0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
s2 :: (Show a, Integral a) => a -> String
s2 :: a -> String
s2 v :: a
v = a -> (Int -> Char) -> a -> String -> String
forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase 2 Int -> Char
dig a
v "" where dig :: Int -> Char
dig = Maybe Char -> Char
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Char -> Char) -> (Int -> Maybe Char) -> Int -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> [(Int, Char)] -> Maybe Char)
-> [(Int, Char)] -> Int -> Maybe Char
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> [(Int, Char)] -> Maybe Char
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [(0, '0'), (1, '1')]
s16 :: (Show a, Integral a) => a -> String
s16 :: a -> String
s16 v :: a
v = a -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex a
v ""
readBin :: Num a => String -> a
readBin :: String -> a
readBin ('-':s :: String
s) = -(String -> a
forall a. Num a => String -> a
readBin String
s)
readBin s :: String
s = case a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt 2 Char -> Bool
isDigit Char -> Int
cvt String
s' of
[(a :: a
a, "")] -> a
a
_ -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "SBV.readBin: Cannot read a binary number from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s
where cvt :: Char -> Int
cvt c :: Char
c = Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord '0'
isDigit :: Char -> Bool
isDigit = (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "01")
s' :: String
s' | "0b" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s = Int -> String -> String
forall a. Int -> [a] -> [a]
drop 2 String
s
| Bool
True = String
s
showCFloat :: Float -> String
showCFloat :: Float -> String
showCFloat f :: Float
f
| Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f = "((float) NAN)"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "((float) (-INFINITY))"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f = "((float) INFINITY)"
| Bool
True = Float -> String -> String
forall a. RealFloat a => a -> String -> String
Numeric.showHFloat Float
f (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "F /* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Float -> String
forall a. Show a => a -> String
show Float
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ "F */"
showCDouble :: Double -> String
showCDouble :: Double -> String
showCDouble d :: Double
d
| Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d = "((double) NAN)"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "((double) (-INFINITY))"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d = "((double) INFINITY)"
| Bool
True = Double -> String -> String
forall a. RealFloat a => a -> String -> String
Numeric.showHFloat Double
d " /* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
forall a. Show a => a -> String
show Double
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ " */"
showHFloat :: Float -> String
showHFloat :: Float -> String
showHFloat f :: Float
f
| Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f = "((0/0) :: Float)"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "((-1/0) :: Float)"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f = "((1/0) :: Float)"
| Bool
True = Float -> String
forall a. Show a => a -> String
show Float
f
showHDouble :: Double -> String
showHDouble :: Double -> String
showHDouble d :: Double
d
| Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d = "((0/0) :: Double)"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "((-1/0) :: Double)"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d = "((1/0) :: Double)"
| Bool
True = Double -> String
forall a. Show a => a -> String
show Double
d
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat rm :: RoundingMode
rm f :: Float
f
| Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f = String -> String
as "NaN"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = String -> String
as "-oo"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f = String -> String
as "+oo"
| Float -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Float
f = String -> String
as "-zero"
| Float
f Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = String -> String
as "+zero"
| Bool
True = "((_ to_fp 8 24) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (Float -> Rational
forall a. Real a => a -> Rational
toRational Float
f) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
where as :: String -> String
as s :: String
s = "(_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 8 24)"
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble rm :: RoundingMode
rm d :: Double
d
| Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d = String -> String
as "NaN"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = String -> String
as "-oo"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d = String -> String
as "+oo"
| Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
d = String -> String
as "-zero"
| Double
d Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = String -> String
as "+zero"
| Bool
True = "((_ to_fp 11 53) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
where as :: String -> String
as s :: String
s = "(_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 11 53)"
toSMTLibRational :: Rational -> String
toSMTLibRational :: Rational -> String
toSMTLibRational r :: Rational
r
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0
= "(- (/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0))"
| Bool
True
= "(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0)"
where n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r
smtRoundingMode :: RoundingMode -> String
smtRoundingMode :: RoundingMode -> String
smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven"
smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway"
smtRoundingMode RoundTowardPositive = "roundTowardPositive"
smtRoundingMode RoundTowardNegative = "roundTowardNegative"
smtRoundingMode RoundTowardZero = "roundTowardZero"
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib rm :: RoundingMode
rm x :: CV
x
| CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
x, CInteger w :: Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then "false" else "true"
| CV -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted CV
x, CUserSort (_, s :: String
s) <- CV -> CVal
cvVal CV
x = String -> String
roundModeConvert String
s
| CV -> Bool
forall a. HasKind a => a -> Bool
isReal CV
x, CAlgReal r :: AlgReal
r <- CV -> CVal
cvVal CV
x = AlgReal -> String
algRealToSMTLib2 AlgReal
r
| CV -> Bool
forall a. HasKind a => a -> Bool
isFloat CV
x, CFloat f :: Float
f <- CV -> CVal
cvVal CV
x = RoundingMode -> Float -> String
showSMTFloat RoundingMode
rm Float
f
| CV -> Bool
forall a. HasKind a => a -> Bool
isDouble CV
x, CDouble d :: Double
d <- CV -> CVal
cvVal CV
x = RoundingMode -> Double -> String
showSMTDouble RoundingMode
rm Double
d
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
x), CInteger w :: Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 then Integer -> String
forall a. Show a => a -> String
show Integer
w else "(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
w) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
| Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
x) , CInteger w :: Integer
w <- CV -> CVal
cvVal CV
x = Int -> Integer -> String
smtLibHex (CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x) Integer
w
| CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
x , CInteger w :: Integer
w <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
forall a. Num a => a -> a
negate (2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x)
then Int -> String
mkMinBound (CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x)
else Bool -> String -> String
negIf (Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> String
smtLibHex (CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x) (Integer -> Integer
forall a. Num a => a -> a
abs Integer
w)
| CV -> Bool
forall a. HasKind a => a -> Bool
isChar CV
x , CChar c :: Char
c <- CV -> CVal
cvVal CV
x = Int -> Integer -> String
smtLibHex 8 (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
c))
| CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
x , CString s :: String
s <- CV -> CVal
cvVal CV
x = '\"' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
stringToQFS String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
| CV -> Bool
forall a. HasKind a => a -> Bool
isList CV
x , CList xs :: [CVal]
xs <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibSeq (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
| CV -> Bool
forall a. HasKind a => a -> Bool
isSet CV
x , CSet s :: RCSet CVal
s <- CV -> CVal
cvVal CV
x = Kind -> RCSet CVal -> String
smtLibSet (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) RCSet CVal
s
| CV -> Bool
forall a. HasKind a => a -> Bool
isTuple CV
x , CTuple xs :: [CVal]
xs <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibTup (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
| CV -> Bool
forall a. HasKind a => a -> Bool
isMaybe CV
x , CMaybe mc :: Maybe CVal
mc <- CV -> CVal
cvVal CV
x = Kind -> Maybe CVal -> String
smtLibMaybe (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) Maybe CVal
mc
| CV -> Bool
forall a. HasKind a => a -> Bool
isEither CV
x , CEither ec :: Either CVal CVal
ec <- CV -> CVal
cvVal CV
x = Kind -> Either CVal CVal -> String
smtLibEither (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) Either CVal CVal
ec
| Bool
True = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.cvtCV: Impossible happened: Kind/Value disagreement on: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, CV) -> String
forall a. Show a => a -> String
show (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x, CV
x)
where roundModeConvert :: String -> String
roundModeConvert s :: String
s = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
s ([String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [RoundingMode -> String
smtRoundingMode RoundingMode
m | RoundingMode
m <- [RoundingMode
forall a. Bounded a => a
minBound .. RoundingMode
forall a. Bounded a => a
maxBound] :: [RoundingMode], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
m String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s])
smtLibHex :: Int -> Integer -> String
smtLibHex :: Int -> Integer -> String
smtLibHex 1 v :: Integer
v = "#b" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
v
smtLibHex sz :: Int
sz v :: Integer
v
| Int
sz Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 4 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = "#x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad (Int
sz Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 4) (Integer -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex Integer
v "")
| Bool
True = "#b" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
sz (Integer -> String -> String
showBin Integer
v "")
where showBin :: Integer -> String -> String
showBin = Integer -> (Int -> Char) -> Integer -> String -> String
forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase 2 Int -> Char
intToDigit
negIf :: Bool -> String -> String
negIf :: Bool -> String -> String
negIf True a :: String
a = "(bvneg " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
negIf False a :: String
a = String
a
smtLibSeq :: Kind -> [CVal] -> String
smtLibSeq :: Kind -> [CVal] -> String
smtLibSeq k :: Kind
k [] = "(as seq.empty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
smtLibSeq (KList ek :: Kind
ek) xs :: [CVal]
xs = let mkSeq :: [String] -> String
mkSeq [e :: String
e] = String
e
mkSeq es :: [String]
es = "(seq.++ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
mkUnit :: String -> String
mkUnit inner :: String
inner = "(seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
inner String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
in [String] -> String
mkSeq (String -> String
mkUnit (String -> String) -> (CVal -> String) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (CV -> String) -> (CVal -> CV) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ek (CVal -> String) -> [CVal] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CVal]
xs)
smtLibSeq k :: Kind
k _ = String -> String
forall a. HasCallStack => String -> a
error "SBV.cvToSMTLib: Impossible case (smtLibSeq), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
smtLibSet :: Kind -> RCSet CVal -> String
smtLibSet :: Kind -> RCSet CVal -> String
smtLibSet k :: Kind
k set :: RCSet CVal
set = case RCSet CVal
set of
RegularSet rs :: Set CVal
rs -> (CVal -> String -> String) -> String -> Set CVal -> String
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify "true") (String -> String
start "false") Set CVal
rs
ComplementSet rs :: Set CVal
rs -> (CVal -> String -> String) -> String -> Set CVal -> String
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify "false") (String -> String
start "true") Set CVal
rs
where ke :: Kind
ke = case Kind
k of
KSet ek :: Kind
ek -> Kind
ek
_ -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ "SBV.cvToSMTLib: Impossible case (smtLibSet), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
start :: String -> String
start def :: String
def = "((as const " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
modify :: String -> CVal -> String -> String
modify how :: String
how e :: CVal
e s :: String
s = "(store " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ke CVal
e) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
how String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
smtLibTup :: Kind -> [CVal] -> String
smtLibTup :: Kind -> [CVal] -> String
smtLibTup (KTuple []) _ = "mkSBVTuple0"
smtLibTup (KTuple ks :: [Kind]
ks) xs :: [CVal]
xs = "(mkSBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Kind -> CVal -> String) -> [Kind] -> [CVal] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ek :: Kind
ek e :: CVal
e -> RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ek CVal
e)) [Kind]
ks [CVal]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
smtLibTup k :: Kind
k _ = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.cvToSMTLib: Impossible case (smtLibTup), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
dtConstructor :: String -> [String] -> Kind -> String
dtConstructor fld :: String
fld [] res :: Kind
res = "(as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
dtConstructor fld :: String
fld args :: [String]
args res :: Kind
res = "((as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
smtLibMaybe :: Kind -> Maybe CVal -> String
smtLibMaybe :: Kind -> Maybe CVal -> String
smtLibMaybe km :: Kind
km@ KMaybe{} Nothing = String -> [String] -> Kind -> String
dtConstructor "nothing_SBVMaybe" [] Kind
km
smtLibMaybe km :: Kind
km@(KMaybe k :: Kind
k) (Just c :: CVal
c) = String -> [String] -> Kind -> String
dtConstructor "just_SBVMaybe" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
km
smtLibMaybe k :: Kind
k _ = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.cvToSMTLib: Impossible case (smtLibMaybe), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
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 k :: Kind
k _) (Left c :: CVal
c) = String -> [String] -> Kind -> String
dtConstructor "left_SBVEither" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
smtLibEither ke :: Kind
ke@(KEither _ k :: Kind
k) (Right c :: CVal
c) = String -> [String] -> Kind -> String
dtConstructor "right_SBVEither" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
smtLibEither k :: Kind
k _ = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.cvToSMTLib: Impossible case (smtLibEither), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
mkMinBound :: Int -> String
mkMinBound :: Int -> String
mkMinBound i :: Int
i = "#b1" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) '0'
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero _ (KUninterpreted _ (Right (f :: String
f:_))) = String
f
mkSkolemZero _ (KUninterpreted s :: String
s _) = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.mkSkolemZero: Unexpected uninterpreted sort: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
mkSkolemZero rm :: RoundingMode
rm k :: Kind
k = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (0::Integer))