    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Utils.PrettyNum
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Number representations in hex/bin
    -----------------------------------------------------------------------------

    {-# 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)

    -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
    class PrettyNum a where
      -- | Show a number in hexadecimal, starting with @0x@ and type.
      hexS :: a -> String
      -- | Show a number in binary, starting with @0b@ and type.
      binS :: a -> String
      -- | Show a number in hexadecimal, starting with @0x@ but no type.
      hexP :: a -> String
      -- | Show a number in binary, starting with @0b@ but no type.
      binP :: a -> String
      -- | Show a number in hex, without prefix, or types.
      hex :: a -> String
      -- | Show a number in bin, without prefix, or types.
      bin :: a -> String

    -- Why not default methods? Because defaults need "Integral a" but Bool is not..
    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

    -- | Show as a hexadecimal value. First bool controls whether type info is printed
    -- while the second boolean controls wether 0x prefix is printed. The tuple is
    -- the signedness and the bit-length of the input. The length of the string
    -- will /not/ depend on the value, but rather the bit-length.
    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

    -- | Show as hexadecimal, but for C programs. We have to be careful about
    -- printing min-bounds, since C does some funky casting, possibly losing
    -- the sign bit. In those cases, we use the defined constants in <stdint.h>.
    -- We also properly append the necessary suffixes as needed.
    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"

                       _           -> ""

    -- | Show as a hexadecimal value, integer version. Almost the same as shex above
    -- except we don't have a bit-length so the length of the string will depend
    -- on the actual value.
    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  = ""

    -- | Similar to 'shex'; except in binary.
    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  = ""

    -- | Similar to 'shexI'; except in binary.
    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 a string to a given length. If the string is longer, then we don't drop anything.
    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

    -- | Binary printer
    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')]

    -- | Hex printer
    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 ""

    -- | A more convenient interface for reading binary numbers, also supports negative numbers
    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

    -- | A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
    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 */"

    -- | A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
    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]
    ++ " */"

    -- | A version of show for floats that generates correct Haskell literals for nan/infinite
    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

    -- | A version of show for doubles that generates correct Haskell literals for nan/infinite
    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

    -- | A version of show for floats that generates correct SMTLib literals using the rounding mode
    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)"

    -- | A version of show for doubles that generates correct SMTLib literals using the rounding mode
    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)"

    -- | Show a rational in SMTLib format
    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

    -- | Convert a rounding mode to the format SMT-Lib2 understands.
    smtRoundingMode :: RoundingMode -> String
    smtRoundingMode :: RoundingMode -> String
    smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven"
    smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway"
    smtRoundingMode RoundTowardPositive    = "roundTowardPositive"
    smtRoundingMode RoundTowardNegative    = "roundTowardNegative"
    smtRoundingMode RoundTowardZero        = "roundTowardZero"

    -- | Convert a CV to an SMTLib2 compliant value
    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
      -- signed numbers (with 2's complement representation) is problematic
      -- since there's no way to put a bvneg over a positive number to get minBound..
      -- Hence, we punt and use binary notation in that particular case
      | 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])
            -- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time
            -- being, SBV only supports sizes that are multiples of 4, but the below code is more robust
            -- in case of future extensions to support arbitrary sizes.
            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

            -- anomaly at the 2's complement min value! Have to use binary notation here
            -- as there is no positive value we can provide to make the bvneg work.. (see above)
            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'

    -- | Create a skolem 0 for the kind
    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))