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