    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Floating
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Implementation of floating-point operations mapping to SMT-Lib2 floats
    -----------------------------------------------------------------------------

    {-# LANGUAGE DefaultSignatures    #-}
    {-# LANGUAGE FlexibleContexts     #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE Rank2Types           #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE TypeOperators        #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans -Wno-incomplete-uni-patterns #-}

    module Data.SBV.Core.Floating (
             IEEEFloating(..), IEEEFloatConvertible(..)
           , sFloatAsSWord32, sDoubleAsSWord64, sFloatingPointAsSWord
           , sWord32AsSFloat, sWord64AsSDouble, sWordAsSFloatingPoint
           , blastSFloat, blastSDouble,  blastSFloatingPoint
           , sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord
           , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint
           ) where

    import Data.Bits (testBit)
    import Data.Int  (Int8,  Int16,  Int32,  Int64)
    import Data.Word (Word8, Word16, Word32, Word64)

    import Data.Proxy

    import Data.SBV.Core.AlgReals (isExactRational)
    import Data.SBV.Core.Sized
    import Data.SBV.Core.SizedFloats

    import Data.SBV.Core.Data
    import Data.SBV.Core.Kind
    import Data.SBV.Core.Model
    import Data.SBV.Core.Symbolic (addSValOptGoal)

    import Data.SBV.Utils.Numeric

    import Data.Ratio

    import GHC.TypeLits

    import LibBF

    import Data.SBV.Core.Operations

    -- | A class of floating-point (IEEE754) operations, some of
    -- which behave differently based on rounding modes. Note that unless
    -- the rounding mode is concretely RoundNearestTiesToEven, we will
    -- not concretely evaluate these, but rather pass down to the SMT solver.
    class (SymVal a, RealFloat a) => IEEEFloating a where
      -- | Compute the floating point absolute value.
      fpAbs             ::                  SBV a -> SBV a

      -- | Compute the unary negation. Note that @0 - x@ is not equivalent to @-x@ for floating-point, since @-0@ and @0@ are different.
      fpNeg             ::                  SBV a -> SBV a

      -- | Add two floating point values, using the given rounding mode
      fpAdd             :: SRoundingMode -> SBV a -> SBV a -> SBV a

      -- | Subtract two floating point values, using the given rounding mode
      fpSub             :: SRoundingMode -> SBV a -> SBV a -> SBV a

      -- | Multiply two floating point values, using the given rounding mode
      fpMul             :: SRoundingMode -> SBV a -> SBV a -> SBV a

      -- | Divide two floating point values, using the given rounding mode
      fpDiv             :: SRoundingMode -> SBV a -> SBV a -> SBV a

      -- | Fused-multiply-add three floating point values, using the given rounding mode. @fpFMA x y z = x*y+z@ but with only
      -- one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
      -- Haskell lacks an FMA implementation.
      fpFMA             :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a

      -- | Compute the square-root of a float, using the given rounding mode
      fpSqrt            :: SRoundingMode -> SBV a -> SBV a

      -- | Compute the remainder: @x - y * n@, where @n@ is the truncated integer nearest to x/y. The rounding mode
      -- is implicitly assumed to be @RoundNearestTiesToEven@.
      fpRem             ::                  SBV a -> SBV a -> SBV a

      -- | Round to the nearest integral value, using the given rounding mode.
      fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a

      -- | Compute the minimum of two floats, respects @infinity@ and @NaN@ values
      fpMin             ::                  SBV a -> SBV a -> SBV a

      -- | Compute the maximum of two floats, respects @infinity@ and @NaN@ values
      fpMax             ::                  SBV a -> SBV a -> SBV a

      -- | Are the two given floats exactly the same. That is, @NaN@ will compare equal to itself, @+0@ will /not/ compare
      -- equal to @-0@ etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use '.=='.)
      fpIsEqualObject   ::                  SBV a -> SBV a -> SBool

      -- | Is the floating-point number a normal value. (i.e., not denormalized.)
      fpIsNormal :: SBV a -> SBool

      -- | Is the floating-point number a subnormal value. (Also known as denormal.)
      fpIsSubnormal :: SBV a -> SBool

      -- | Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)
      fpIsZero :: SBV a -> SBool

      -- | Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)
      fpIsInfinite :: SBV a -> SBool

      -- | Is the floating-point number a NaN value?
      fpIsNaN ::  SBV a -> SBool

      -- | Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.
      fpIsNegative :: SBV a -> SBool

      -- | Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.
      fpIsPositive :: SBV a -> SBool

      -- | Is the floating point number -0?
      fpIsNegativeZero :: SBV a -> SBool

      -- | Is the floating point number +0?
      fpIsPositiveZero :: SBV a -> SBool

      -- | Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.
      fpIsPoint :: SBV a -> SBool

      -- Default definitions. Minimal complete definition: None! All should be taken care by defaults
      -- Note that we never evaluate FMA concretely, as there's no fma operator in Haskell
      fpAbs              = FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1  FPOp
    FP_Abs             ((a -> a) -> Maybe (a -> a)
    forall a. a -> Maybe a
    Just a -> a
    forall a. Num a => a -> a
    abs)                Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpNeg              = FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1  FPOp
    FP_Neg             ((a -> a) -> Maybe (a -> a)
    forall a. a -> Maybe a
    Just a -> a
    forall a. Num a => a -> a
    negate)             Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpAdd              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2  FPOp
    FP_Add             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. Num a => a -> a -> a
    (+))                (Maybe SRoundingMode -> SBV a -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpSub              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2  FPOp
    FP_Sub             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just (-))                (Maybe SRoundingMode -> SBV a -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpMul              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2  FPOp
    FP_Mul             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. Num a => a -> a -> a
    (*))                (Maybe SRoundingMode -> SBV a -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpDiv              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2  FPOp
    FP_Div             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. Fractional a => a -> a -> a
    (/))                (Maybe SRoundingMode -> SBV a -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpFMA              = FPOp
    -> Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    lift3  FPOp
    FP_FMA             Maybe (a -> a -> a -> a)
    forall a. Maybe a
    Nothing                   (Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpSqrt             = FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1  FPOp
    FP_Sqrt            ((a -> a) -> Maybe (a -> a)
    forall a. a -> Maybe a
    Just a -> a
    forall a. Floating a => a -> a
    sqrt)               (Maybe SRoundingMode -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpRem              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2  FPOp
    FP_Rem             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. RealFloat a => a -> a -> a
    fpRemH)             Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpRoundToIntegral  = FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1  FPOp
    FP_RoundToIntegral ((a -> a) -> Maybe (a -> a)
    forall a. a -> Maybe a
    Just a -> a
    forall a. RealFloat a => a -> a
    fpRoundToIntegralH) (Maybe SRoundingMode -> SBV a -> SBV a)
    -> (SRoundingMode -> Maybe SRoundingMode)
    -> SRoundingMode
    -> SBV a
    -> SBV a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just
      fpMin              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    (SymVal a, RealFloat a) =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    liftMM FPOp
    FP_Min             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. RealFloat a => a -> a -> a
    fpMinH)             Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpMax              = FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    forall a.
    (SymVal a, RealFloat a) =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    liftMM FPOp
    FP_Max             ((a -> a -> a) -> Maybe (a -> a -> a)
    forall a. a -> Maybe a
    Just a -> a -> a
    forall a. RealFloat a => a -> a -> a
    fpMaxH)             Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpIsEqualObject    = FPOp
    -> Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBool
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBool
    lift2B FPOp
    FP_ObjEqual        ((a -> a -> Bool) -> Maybe (a -> a -> Bool)
    forall a. a -> Maybe a
    Just a -> a -> Bool
    forall a. RealFloat a => a -> a -> Bool
    fpIsEqualObjectH)   Maybe SRoundingMode
    forall a. Maybe a
    Nothing
      fpIsNormal         = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsNormal        a -> Bool
    forall a. RealFloat a => a -> Bool
    fpIsNormalizedH
      fpIsSubnormal      = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsSubnormal     a -> Bool
    forall a. RealFloat a => a -> Bool
    isDenormalized
      fpIsZero           = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsZero          (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    0)
      fpIsInfinite       = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsInfinite      a -> Bool
    forall a. RealFloat a => a -> Bool
    isInfinite
      fpIsNaN            = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsNaN           a -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN
      fpIsNegative       = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsNegative      (\a
    x -> a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < a
    0 Bool -> Bool -> Bool
    ||       a -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero a
    x)
      fpIsPositive       = FPOp -> (a -> Bool) -> SBV a -> SBool
    forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    FP_IsPositive      (\a
    x -> a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    0 Bool -> Bool -> Bool
    && Bool -> Bool
    not (a -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero a
    x))
      fpIsNegativeZero SBV a
    x = SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsZero SBV a
    x SBool -> SBool -> SBool
    .&& SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegative SBV a
    x
      fpIsPositiveZero SBV a
    x = SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsZero SBV a
    x SBool -> SBool -> SBool
    .&& SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsPositive SBV a
    x
      fpIsPoint        SBV a
    x = SBool -> SBool
    sNot (SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV a
    x SBool -> SBool -> SBool
    .|| SBV a -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsInfinite SBV a
    x)

    -- | SFloat instance
    instance IEEEFloating Float

    -- | SDouble instance
    instance IEEEFloating Double

    -- | Conversion to and from floats
    class SymVal a => IEEEFloatConvertible a where
      -- | Convert from an IEEE74 single precision float.
      fromSFloat :: SRoundingMode -> SFloat -> SBV a
      fromSFloat = SRoundingMode -> SFloat -> SBV a
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat

      -- | Convert to an IEEE-754 Single-precision float.
      toSFloat :: SRoundingMode -> SBV a -> SFloat

      -- default definition if we have an integral like
      default toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat
      toSFloat = (RoundingMode -> a -> Maybe Float)
    -> SRoundingMode -> SBV a -> SFloat
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((a -> Maybe Float) -> RoundingMode -> a -> Maybe Float
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE (Float -> Maybe Float
    forall a. a -> Maybe a
    Just (Float -> Maybe Float) -> (a -> Float) -> a -> Maybe Float
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> Float
    forall a. Fractional a => Rational -> a
    fromRational (Rational -> Float) -> (a -> Rational) -> a -> Float
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Rational
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral))

      -- | Convert from an IEEE74 double precision float.
      fromSDouble :: SRoundingMode -> SDouble -> SBV a
      fromSDouble = SRoundingMode -> SDouble -> SBV a
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat

      -- | Convert to an IEEE-754 Double-precision float.
      toSDouble :: SRoundingMode -> SBV a -> SDouble

      -- default definition if we have an integral like
      default toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble
      toSDouble = (RoundingMode -> a -> Maybe Double)
    -> SRoundingMode -> SBV a -> SDouble
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((a -> Maybe Double) -> RoundingMode -> a -> Maybe Double
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE (Double -> Maybe Double
    forall a. a -> Maybe a
    Just (Double -> Maybe Double) -> (a -> Double) -> a -> Maybe Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational (Rational -> Double) -> (a -> Rational) -> a -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Rational
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral))

      -- | Convert from an arbitrary floating point.
      fromSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a
      fromSFloatingPoint = SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV a
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat

      -- | Convert to an arbitrary floating point.
      toSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb

      -- -- default definition if we have an integral like
      default toSFloatingPoint :: (Integral a, ValidFloat eb sb) => SRoundingMode -> SBV a -> SFloatingPoint eb sb
      toSFloatingPoint = (RoundingMode -> a -> Maybe (FloatingPoint eb sb))
    -> SRoundingMode -> SBV a -> SBV (FloatingPoint eb sb)
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((a -> Maybe (FloatingPoint eb sb))
    -> RoundingMode -> a -> Maybe (FloatingPoint eb sb)
    forall a b. a -> b -> a
    const (FloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just (FloatingPoint eb sb -> Maybe (FloatingPoint eb sb))
    -> (a -> FloatingPoint eb sb) -> a -> Maybe (FloatingPoint eb sb)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> FloatingPoint eb sb
    forall a. Fractional a => Rational -> a
    fromRational (Rational -> FloatingPoint eb sb)
    -> (a -> Rational) -> a -> FloatingPoint eb sb
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Rational
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral))

    -- Run the function if the conversion is in RNE. Otherwise return Nothing.
    onlyWhenRNE :: (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE :: forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE a -> Maybe b
    f RoundingMode
    RoundNearestTiesToEven a
    v = a -> Maybe b
    f a
    v
    onlyWhenRNE a -> Maybe b
    _ RoundingMode
    _                      a
    _ = Maybe b
    forall a. Maybe a
    Nothing

    -- | A generic from-float converter. Note that this function does no constant folding since
    -- it's behavior is undefined when the input float is out-of-bounds or not a point.
    genericFromFloat :: forall a r. (IEEEFloating a, IEEEFloatConvertible r)
                     => SRoundingMode            -- Rounding mode
                     -> SBV a                    -- Input float/double
                     -> SBV r
    genericFromFloat :: forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SBV a
    f = SVal -> SBV r
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kTo (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r)))
      where kFrom :: Kind
    kFrom = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    f
            kTo :: Kind
    kTo   = Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @r)
            r :: State -> IO SV
    r State
    st  = do SV
    msv <- State -> SRoundingMode -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SRoundingMode
    rm
                       SV
    xsv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    f
                       State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kTo (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> SV -> FPOp
    FP_Cast Kind
    kFrom Kind
    kTo SV
    msv)) [SV
    xsv])

    -- | A generic to-float converter, which will constant-fold as necessary, but only in the sRNE mode for regular floats.
    genericToFloat :: forall a r. (IEEEFloatConvertible a, IEEEFloating r)
                   => (RoundingMode -> a -> Maybe r)     -- How to convert concretely, if possible
                   -> SRoundingMode                      -- Rounding mode
                   -> SBV a                              -- Input convertible
                   -> SBV r
    genericToFloat :: forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat RoundingMode -> a -> Maybe r
    converter SRoundingMode
    rm SBV a
    i
      | Just a
    w <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    i, Just RoundingMode
    crm <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm, Just r
    result <- RoundingMode -> a -> Maybe r
    converter RoundingMode
    crm a
    w
      = r -> SBV r
    forall a. SymVal a => a -> SBV a
    literal r
    result
      | Bool
    True
      = SVal -> SBV r
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kTo (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r)))
      where kFrom :: Kind
    kFrom = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    i
            kTo :: Kind
    kTo   = Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @r)
            r :: State -> IO SV
    r State
    st  = do SV
    msv <- State -> SRoundingMode -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SRoundingMode
    rm
                       SV
    xsv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    i
                       State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kTo (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> SV -> FPOp
    FP_Cast Kind
    kFrom Kind
    kTo SV
    msv)) [SV
    xsv])

    instance IEEEFloatConvertible Int8
    instance IEEEFloatConvertible Int16
    instance IEEEFloatConvertible Int32
    instance IEEEFloatConvertible Int64
    instance IEEEFloatConvertible Word8
    instance IEEEFloatConvertible Word16
    instance IEEEFloatConvertible Word32
    instance IEEEFloatConvertible Word64
    instance IEEEFloatConvertible Integer

    -- For float and double, skip the conversion if the same and do the constant folding, unlike all others.
    instance IEEEFloatConvertible Float where
      toSFloat :: SRoundingMode -> SFloat -> SFloat
    toSFloat  SRoundingMode
    _ SFloat
    f = SFloat
    f
      toSDouble :: SRoundingMode -> SFloat -> SDouble
    toSDouble     = (RoundingMode -> Float -> Maybe Double)
    -> SRoundingMode -> SFloat -> SDouble
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((Float -> Maybe Double) -> RoundingMode -> Float -> Maybe Double
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE (Double -> Maybe Double
    forall a. a -> Maybe a
    Just (Double -> Maybe Double)
    -> (Float -> Double) -> Float -> Maybe Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Float -> Double
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp))

      toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SFloat -> SFloatingPoint eb sb
    toSFloatingPoint SRoundingMode
    rm SFloat
    f = SRoundingMode -> SDouble -> SFloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SDouble -> SFloatingPoint eb sb
    forall a (eb :: Nat) (sb :: Nat).
    (IEEEFloatConvertible a, ValidFloat eb sb) =>
    SRoundingMode -> SBV a -> SFloatingPoint eb sb
    toSFloatingPoint SRoundingMode
    rm (SDouble -> SFloatingPoint eb sb)
    -> SDouble -> SFloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ SRoundingMode -> SFloat -> SDouble
    forall a.
    IEEEFloatConvertible a =>
    SRoundingMode -> SBV a -> SDouble
    toSDouble SRoundingMode
    rm SFloat
    f

      fromSFloat :: SRoundingMode -> SFloat -> SFloat
    fromSFloat  SRoundingMode
    _  SFloat
    f = SFloat
    f
      fromSDouble :: SRoundingMode -> SDouble -> SFloat
    fromSDouble SRoundingMode
    rm SDouble
    f
        | Just RoundingMode
    RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm
        , Just Double
    fv                     <- SDouble -> Maybe Double
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SDouble
    f
        = Float -> SFloat
    forall a. SymVal a => a -> SBV a
    literal (Double -> Float
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp Double
    fv)
        | Bool
    True
        = SRoundingMode -> SDouble -> SFloat
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SDouble
    f

    instance IEEEFloatConvertible Double where
      toSFloat :: SRoundingMode -> SDouble -> SFloat
    toSFloat      = (RoundingMode -> Double -> Maybe Float)
    -> SRoundingMode -> SDouble -> SFloat
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((Double -> Maybe Float) -> RoundingMode -> Double -> Maybe Float
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE (Float -> Maybe Float
    forall a. a -> Maybe a
    Just (Float -> Maybe Float)
    -> (Double -> Float) -> Double -> Maybe Float
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Double -> Float
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp))
      toSDouble :: SRoundingMode -> SDouble -> SDouble
    toSDouble SRoundingMode
    _ SDouble
    d = SDouble
    d

      toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SDouble -> SFloatingPoint eb sb
    toSFloatingPoint SRoundingMode
    rm SDouble
    sd
        | Just Double
    d <- SDouble -> Maybe Double
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SDouble
    sd, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) (Double -> BigFloat
    bfFromDouble Double
    d))
        | Bool
    True
        = SBV (FloatingPoint eb sb)
    res
        where (Kind
    k, Int
    ei, Int
    si) = case SBV (FloatingPoint eb sb) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV (FloatingPoint eb sb)
    res of
                             kr :: Kind
    kr@(KFP Int
    eb Int
    sb) -> (Kind
    kr, Int
    eb, Int
    sb)
                             Kind
    kr             -> [Char] -> (Kind, Int, Int)
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> (Kind, Int, Int)) -> [Char] -> (Kind, Int, Int)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected kind in toSFloatingPoint: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SRoundingMode, SDouble) -> [Char]
    forall a. Show a => a -> [Char]
    show (Kind
    kr, SRoundingMode
    rm, SDouble
    sd)
              res :: SBV (FloatingPoint eb sb)
    res = SVal -> SBV (FloatingPoint eb sb)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (FloatingPoint eb sb))
    -> SVal -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
              r :: State -> IO SV
    r State
    st = do SV
    msv <- State -> SRoundingMode -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SRoundingMode
    rm
                        SV
    xsv <- State -> SDouble -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SDouble
    sd
                        State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> SV -> FPOp
    FP_Cast Kind
    KDouble Kind
    k SV
    msv)) [SV
    xsv])

      fromSDouble :: SRoundingMode -> SDouble -> SDouble
    fromSDouble SRoundingMode
    _  SDouble
    d = SDouble
    d
      fromSFloat :: SRoundingMode -> SFloat -> SDouble
    fromSFloat  SRoundingMode
    rm SFloat
    d
        | Just RoundingMode
    RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm
        , Just Float
    dv                     <- SFloat -> Maybe Float
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloat
    d
        = Double -> SDouble
    forall a. SymVal a => a -> SBV a
    literal (Float -> Double
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp Float
    dv)
        | Bool
    True
        = SRoundingMode -> SFloat -> SDouble
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SFloat
    d

    convertWhenExactRational :: Fractional a => AlgReal -> Maybe a
    convertWhenExactRational :: forall a. Fractional a => AlgReal -> Maybe a
    convertWhenExactRational AlgReal
    r
      | AlgReal -> Bool
    isExactRational AlgReal
    r = a -> Maybe a
    forall a. a -> Maybe a
    Just (Rational -> a
    forall a. Fractional a => Rational -> a
    fromRational (AlgReal -> Rational
    forall a. Real a => a -> Rational
    toRational AlgReal
    r))
      | Bool
    True              = Maybe a
    forall a. Maybe a
    Nothing

    -- For AlgReal; be careful to only process exact rationals concretely
    instance IEEEFloatConvertible AlgReal where
      toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat
    toSFloat         = (RoundingMode -> AlgReal -> Maybe Float)
    -> SRoundingMode -> SBV AlgReal -> SFloat
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((AlgReal -> Maybe Float) -> RoundingMode -> AlgReal -> Maybe Float
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE AlgReal -> Maybe Float
    forall a. Fractional a => AlgReal -> Maybe a
    convertWhenExactRational)
      toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble
    toSDouble        = (RoundingMode -> AlgReal -> Maybe Double)
    -> SRoundingMode -> SBV AlgReal -> SDouble
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((AlgReal -> Maybe Double)
    -> RoundingMode -> AlgReal -> Maybe Double
    forall a b. (a -> Maybe b) -> RoundingMode -> a -> Maybe b
    onlyWhenRNE AlgReal -> Maybe Double
    forall a. Fractional a => AlgReal -> Maybe a
    convertWhenExactRational)
      toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb
    toSFloatingPoint = (RoundingMode -> AlgReal -> Maybe (FloatingPoint eb sb))
    -> SRoundingMode -> SBV AlgReal -> SBV (FloatingPoint eb sb)
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat ((AlgReal -> Maybe (FloatingPoint eb sb))
    -> RoundingMode -> AlgReal -> Maybe (FloatingPoint eb sb)
    forall a b. a -> b -> a
    const       AlgReal -> Maybe (FloatingPoint eb sb)
    forall a. Fractional a => AlgReal -> Maybe a
    convertWhenExactRational)

    -- Arbitrary floats can handle all rounding modes in concrete mode
    instance ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) where
      toSFloat :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloat
    toSFloat SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v)) <- SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV (FloatingPoint eb sb)
    i, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = Float -> SFloat
    forall a. SymVal a => a -> SBV a
    literal (Float -> SFloat) -> Float -> SFloat
    forall a b. (a -> b) -> a -> b
    $ Double -> Float
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp (Double -> Float) -> Double -> Float
    forall a b. (a -> b) -> a -> b
    $ (Double, Status) -> Double
    forall a b. (a, b) -> a
    fst (RoundMode -> BigFloat -> (Double, Status)
    bfToDouble RoundMode
    brm ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v)))
        | Bool
    True
        = (RoundingMode -> FloatingPoint eb sb -> Maybe Float)
    -> SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloat
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (\RoundingMode
    _ FloatingPoint eb sb
    _ -> Maybe Float
    forall a. Maybe a
    Nothing) SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
              si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

      fromSFloat :: SRoundingMode -> SFloat -> SBV (FloatingPoint eb sb)
    fromSFloat SRoundingMode
    rm SFloat
    i
        | Just Float
    f <- SFloat -> Maybe Float
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloat
    i, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) (Double -> BigFloat
    bfFromDouble (Float -> Double
    forall a b. (RealFloat a, RealFloat b) => a -> b
    fp2fp Float
    f :: Double)))
        | Bool
    True
        = SRoundingMode -> SFloat -> SBV (FloatingPoint eb sb)
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SFloat
    i
        where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
              si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

      toSDouble :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SDouble
    toSDouble SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v)) <- SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV (FloatingPoint eb sb)
    i, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = Double -> SDouble
    forall a. SymVal a => a -> SBV a
    literal (Double -> SDouble) -> Double -> SDouble
    forall a b. (a -> b) -> a -> b
    $ (Double, Status) -> Double
    forall a b. (a, b) -> a
    fst (RoundMode -> BigFloat -> (Double, Status)
    bfToDouble RoundMode
    brm ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v)))
        | Bool
    True
        = (RoundingMode -> FloatingPoint eb sb -> Maybe Double)
    -> SRoundingMode -> SBV (FloatingPoint eb sb) -> SDouble
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (\RoundingMode
    _ FloatingPoint eb sb
    _ -> Maybe Double
    forall a. Maybe a
    Nothing) SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
              si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

      fromSDouble :: SRoundingMode -> SDouble -> SBV (FloatingPoint eb sb)
    fromSDouble SRoundingMode
    rm SDouble
    i
        | Just Double
    f <- SDouble -> Maybe Double
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SDouble
    i, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) (Double -> BigFloat
    bfFromDouble Double
    f))
        | Bool
    True
        = SRoundingMode -> SDouble -> SBV (FloatingPoint eb sb)
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SDouble
    i
        where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
              si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

      toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb sb
    toSFloatingPoint SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v)) <- SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV (FloatingPoint eb sb)
    i, Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si (BigFloat -> FP) -> BigFloat -> FP
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfRoundFloat (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v)
        | Bool
    True
        = (RoundingMode
     -> FloatingPoint eb sb -> Maybe (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (\RoundingMode
    _ FloatingPoint eb sb
    _ -> Maybe (FloatingPoint eb sb)
    forall a. Maybe a
    Nothing) SRoundingMode
    rm SBV (FloatingPoint eb sb)
    i
        where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
              si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

      -- From and To are the same when the source is an arbitrary float!
      fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SFloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    fromSFloatingPoint = SRoundingMode
    -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb sb
    forall a (eb :: Nat) (sb :: Nat).
    (IEEEFloatConvertible a, ValidFloat eb sb) =>
    SRoundingMode -> SBV a -> SFloatingPoint eb sb
    toSFloatingPoint

    -- | Concretely evaluate one arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
    concEval1 :: SymVal a => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
    concEval1 :: forall a.
    SymVal a =>
    Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
    concEval1 Maybe (a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a = do a -> a
    op <- Maybe (a -> a)
    mbOp
                               a
    v  <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
                               case SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SRoundingMode -> Maybe RoundingMode)
    -> Maybe SRoundingMode -> Maybe RoundingMode
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe SRoundingMode
    mbRm of
                                       Maybe RoundingMode
    Nothing                     -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a -> a
    op a
    v)
                                       Just RoundingMode
    RoundNearestTiesToEven -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a -> a
    op a
    v)
                                       Maybe RoundingMode
    _                           -> Maybe (SBV a)
    forall a. Maybe a
    Nothing

    -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
    concEval2 :: SymVal a => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    concEval2 :: forall a.
    SymVal a =>
    Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    concEval2 Maybe (a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b = do a -> a -> a
    op <- Maybe (a -> a -> a)
    mbOp
                                 a
    v1 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
                                 a
    v2 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    b
                                 case SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SRoundingMode -> Maybe RoundingMode)
    -> Maybe SRoundingMode -> Maybe RoundingMode
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe SRoundingMode
    mbRm of
                                         Maybe RoundingMode
    Nothing                     -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a
    v1 a -> a -> a
    `op` a
    v2)
                                         Just RoundingMode
    RoundNearestTiesToEven -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a
    v1 a -> a -> a
    `op` a
    v2)
                                         Maybe RoundingMode
    _                           -> Maybe (SBV a)
    forall a. Maybe a
    Nothing

    -- | Concretely evaluate a bool producing two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
    concEval2B :: SymVal a => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
    concEval2B :: forall a.
    SymVal a =>
    Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
    concEval2B Maybe (a -> a -> Bool)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b = do a -> a -> Bool
    op <- Maybe (a -> a -> Bool)
    mbOp
                                  a
    v1 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
                                  a
    v2 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    b
                                  case SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SRoundingMode -> Maybe RoundingMode)
    -> Maybe SRoundingMode -> Maybe RoundingMode
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe SRoundingMode
    mbRm of
                                          Maybe RoundingMode
    Nothing                     -> (SBool -> Maybe SBool
    forall a. a -> Maybe a
    Just (SBool -> Maybe SBool) -> (Bool -> SBool) -> Bool -> Maybe SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal) (a
    v1 a -> a -> Bool
    `op` a
    v2)
                                          Just RoundingMode
    RoundNearestTiesToEven -> (SBool -> Maybe SBool
    forall a. a -> Maybe a
    Just (SBool -> Maybe SBool) -> (Bool -> SBool) -> Bool -> Maybe SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal) (a
    v1 a -> a -> Bool
    `op` a
    v2)
                                          Maybe RoundingMode
    _                           -> Maybe SBool
    forall a. Maybe a
    Nothing

    -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data
    concEval3 :: SymVal a => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
    concEval3 :: forall a.
    SymVal a =>
    Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
    concEval3 Maybe (a -> a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b SBV a
    c = do a -> a -> a -> a
    op <- Maybe (a -> a -> a -> a)
    mbOp
                                   a
    v1 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
                                   a
    v2 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    b
                                   a
    v3 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    c
                                   case SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SRoundingMode -> Maybe RoundingMode)
    -> Maybe SRoundingMode -> Maybe RoundingMode
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe SRoundingMode
    mbRm of
                                           Maybe RoundingMode
    Nothing                     -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a -> a -> a -> a
    op a
    v1 a
    v2 a
    v3)
                                           Just RoundingMode
    RoundNearestTiesToEven -> (SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal) (a -> a -> a -> a
    op a
    v1 a
    v2 a
    v3)
                                           Maybe RoundingMode
    _                           -> Maybe (SBV a)
    forall a. Maybe a
    Nothing

    -- | Add the converted rounding mode if given as an argument
    addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    _  Maybe SRoundingMode
    Nothing   [SV]
    as = [SV] -> IO [SV]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SV]
    as
    addRM State
    st (Just SRoundingMode
    rm) [SV]
    as = do SV
    svm <- State -> SRoundingMode -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SRoundingMode
    rm
                               [SV] -> IO [SV]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    svm SV -> [SV] -> [SV]
    forall a. a -> [a] -> [a]
    : [SV]
    as)

    -- | Lift a 1 arg FP-op
    lift1 :: SymVal a => FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1 :: forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1 FPOp
    w Maybe (a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a
      | Just SBV a
    cv <- Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
    forall a.
    SymVal a =>
    Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
    concEval1 Maybe (a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a
      = SBV a
    cv
      | Bool
    True
      = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k    = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    a
            r :: State -> IO SV
    r State
    st = do SV
    sva  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      [SV]
    args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    st Maybe SRoundingMode
    mbRm [SV
    sva]
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV]
    args)

    -- | Lift an FP predicate
    lift1B :: SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B :: forall a. SymVal a => FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B FPOp
    w a -> Bool
    f SBV a
    a
       | Just a
    v <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal (Bool -> SBool) -> Bool -> SBool
    forall a b. (a -> b) -> a -> b
    $ a -> Bool
    f a
    v
       | Bool
    True                  = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
       where r :: State -> IO SV
    r State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                       State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV
    sva])

    -- | Lift a 2 arg FP-op
    lift2 :: SymVal a => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a
    lift2 :: forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 FPOp
    w Maybe (a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      | Just SBV a
    cv <- Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    forall a.
    SymVal a =>
    Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    concEval2 Maybe (a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      = SBV a
    cv
      | Bool
    True
      = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k    = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    a
            r :: State -> IO SV
    r State
    st = do SV
    sva  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    b
                      [SV]
    args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    st Maybe SRoundingMode
    mbRm [SV
    sva, SV
    svb]
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV]
    args)

    -- | Lift min/max: Note that we protect against constant folding if args are alternating sign 0's, since
    -- SMTLib is deliberately nondeterministic in this case
    liftMM :: (SymVal a, RealFloat a) => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a
    liftMM :: forall a.
    (SymVal a, RealFloat a) =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    liftMM FPOp
    w Maybe (a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      | Just a
    v1 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
      , Just a
    v2 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    b
      , Bool -> Bool
    not ((a -> Bool
    isN0 a
    v1 Bool -> Bool -> Bool
    && a -> Bool
    isP0 a
    v2) Bool -> Bool -> Bool
    || (a -> Bool
    isP0 a
    v1 Bool -> Bool -> Bool
    && a -> Bool
    isN0 a
    v2))          -- If not +0/-0 or -0/+0
      , Just SBV a
    cv <- Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    forall a.
    SymVal a =>
    Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    concEval2 Maybe (a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      = SBV a
    cv
      | Bool
    True
      = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where isN0 :: a -> Bool
    isN0   = a -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero
            isP0 :: a -> Bool
    isP0 a
    x = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    0 Bool -> Bool -> Bool
    && Bool -> Bool
    not (a -> Bool
    isN0 a
    x)
            k :: Kind
    k    = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    a
            r :: State -> IO SV
    r State
    st = do SV
    sva  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    b
                      [SV]
    args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    st Maybe SRoundingMode
    mbRm [SV
    sva, SV
    svb]
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV]
    args)

    -- | Lift a 2 arg FP-op, producing bool
    lift2B :: SymVal a => FPOp -> Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBool
    lift2B :: forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBool
    lift2B FPOp
    w Maybe (a -> a -> Bool)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      | Just SBool
    cv <- Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
    forall a.
    SymVal a =>
    Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
    concEval2B Maybe (a -> a -> Bool)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b
      = SBool
    cv
      | Bool
    True
      = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where r :: State -> IO SV
    r State
    st = do SV
    sva  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    b
                      [SV]
    args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    st Maybe SRoundingMode
    mbRm [SV
    sva, SV
    svb]
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV]
    args)

    -- | Lift a 3 arg FP-op
    lift3 :: SymVal a => FPOp -> Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
    lift3 :: forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    lift3 FPOp
    w Maybe (a -> a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b SBV a
    c
      | Just SBV a
    cv <- Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
    forall a.
    SymVal a =>
    Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
    concEval3 Maybe (a -> a -> a -> a)
    mbOp Maybe SRoundingMode
    mbRm SBV a
    a SBV a
    b SBV a
    c
      = SBV a
    cv
      | Bool
    True
      = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k    = SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    a
            r :: State -> IO SV
    r State
    st = do SV
    sva  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    b
                      SV
    svc  <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    c
                      [SV]
    args <- State -> Maybe SRoundingMode -> [SV] -> IO [SV]
    addRM State
    st Maybe SRoundingMode
    mbRm [SV
    sva, SV
    svb, SV
    svc]
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    w) [SV]
    args)

    -- | Convert an 'SFloat' to an 'SWord32', preserving the bit-correspondence. Note that since the
    -- representation for @NaN@s are not unique, this function will return a symbolic value when given a
    -- concrete @NaN@.
    --
    -- Implementation note: Since there's no corresponding function in SMTLib for conversion to
    -- bit-representation due to partiality, we use a translation trick by allocating a new word variable,
    -- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map
    -- it to a simple conversion.
    sFloatAsSWord32 :: SFloat -> SWord32
    sFloatAsSWord32 :: SFloat -> SWord32
    sFloatAsSWord32 (SBV SVal
    v) = SVal -> SWord32
    forall a. SVal -> SBV a
    SBV (SVal -> SWord32) -> SVal -> SWord32
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    svFloatAsSWord32 SVal
    v

    -- | Convert an 'SDouble' to an 'SWord64', preserving the bit-correspondence. Note that since the
    -- representation for @NaN@s are not unique, this function will return a symbolic value when given a
    -- concrete @NaN@.
    --
    -- See the implementation note for 'sFloatAsSWord32', as it applies here as well.
    sDoubleAsSWord64 :: SDouble -> SWord64
    sDoubleAsSWord64 :: SDouble -> SWord64
    sDoubleAsSWord64 (SBV SVal
    v) = SVal -> SWord64
    forall a. SVal -> SBV a
    SBV (SVal -> SWord64) -> SVal -> SWord64
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    svDoubleAsSWord64 SVal
    v

    -- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
    -- 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
    blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
    blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
    blastSFloat = SWord32 -> (SBool, [SBool], [SBool])
    forall {a}. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
    extract (SWord32 -> (SBool, [SBool], [SBool]))
    -> (SFloat -> SWord32) -> SFloat -> (SBool, [SBool], [SBool])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SFloat -> SWord32
    sFloatAsSWord32
     where extract :: SBV a -> (SBool, [SBool], [SBool])
    extract SBV a
    x = (SBV a -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SBV a
    x Int
    31, SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [Int
    30, Int
    29 .. Int
    23], SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [Int
    22, Int
    21 .. Int
    0])

    -- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
    -- 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
    blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
    blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
    blastSDouble = SWord64 -> (SBool, [SBool], [SBool])
    forall {a}. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
    extract (SWord64 -> (SBool, [SBool], [SBool]))
    -> (SDouble -> SWord64) -> SDouble -> (SBool, [SBool], [SBool])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SDouble -> SWord64
    sDoubleAsSWord64
     where extract :: SBV a -> (SBool, [SBool], [SBool])
    extract SBV a
    x = (SBV a -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SBV a
    x Int
    63, SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [Int
    62, Int
    61 .. Int
    52], SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [Int
    51, Int
    50 .. Int
    0])

    -- | Extract the sign\/exponent\/mantissa of an arbitrary precision float. The output will have
    -- @eb@ bits in the second argument for exponent, and @sb-1@ bits in the third for mantissa.
    blastSFloatingPoint :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb))
                        => SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
    blastSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
    blastSFloatingPoint = SBV (WordN (eb + sb)) -> (SBool, [SBool], [SBool])
    extract (SBV (WordN (eb + sb)) -> (SBool, [SBool], [SBool]))
    -> (SFloatingPoint eb sb -> SBV (WordN (eb + sb)))
    -> SFloatingPoint eb sb
    -> (SBool, [SBool], [SBool])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SFloatingPoint eb sb -> SBV (WordN (eb + sb))
    forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsSWord
      where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
            si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)
            extract :: SBV (WordN (eb + sb)) -> (SBool, [SBool], [SBool])
    extract SBV (WordN (eb + sb))
    x = (SBV (WordN (eb + sb)) -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SBV (WordN (eb + sb))
    x (Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1), SBV (WordN (eb + sb)) -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV (WordN (eb + sb))
    x [Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2, Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    3 .. Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1], SBV (WordN (eb + sb)) -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV (WordN (eb + sb))
    x [Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2, Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    3 .. Int
    0])

    -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
    sWord32AsSFloat :: SWord32 -> SFloat
    sWord32AsSFloat :: SWord32 -> SFloat
    sWord32AsSFloat SWord32
    fVal
      | Just Word32
    f <- SWord32 -> Maybe Word32
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SWord32
    fVal = Float -> SFloat
    forall a. SymVal a => a -> SBV a
    literal (Float -> SFloat) -> Float -> SFloat
    forall a b. (a -> b) -> a -> b
    $ Word32 -> Float
    wordToFloat Word32
    f
      | Bool
    True                     = SVal -> SFloat
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KFloat (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y)))
      where y :: State -> IO SV
    y State
    st = do SV
    xsv <- State -> SWord32 -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SWord32
    fVal
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KFloat (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret (SWord32 -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SWord32
    fVal) Kind
    KFloat)) [SV
    xsv])

    -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
    sWord64AsSDouble :: SWord64 -> SDouble
    sWord64AsSDouble :: SWord64 -> SDouble
    sWord64AsSDouble SWord64
    dVal
      | Just Word64
    d <- SWord64 -> Maybe Word64
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SWord64
    dVal = Double -> SDouble
    forall a. SymVal a => a -> SBV a
    literal (Double -> SDouble) -> Double -> SDouble
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Double
    wordToDouble Word64
    d
      | Bool
    True                     = SVal -> SDouble
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KDouble (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y)))
      where y :: State -> IO SV
    y State
    st = do SV
    xsv <- State -> SWord64 -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SWord64
    dVal
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KDouble (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret (SWord64 -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SWord64
    dVal) Kind
    KDouble)) [SV
    xsv])

    -- | Convert a float to a comparable 'SWord32'. The trick is to ignore the
    -- sign of -0, and if it's a negative value flip all the bits, and otherwise
    -- only flip the sign bit. This is known as the lexicographic ordering on floats
    -- and it works as long as you do not have a @NaN@.
    sFloatAsComparableSWord32 :: SFloat -> SWord32
    sFloatAsComparableSWord32 :: SFloat -> SWord32
    sFloatAsComparableSWord32 SFloat
    f = SBool -> SWord32 -> SWord32 -> SWord32
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SFloat -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegativeZero SFloat
    f) (SFloat -> SWord32
    sFloatAsComparableSWord32 SFloat
    0) ([SBool] -> SWord32
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord32) -> [SBool] -> SWord32
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot SBool
    sb SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : SBool -> [SBool] -> [SBool] -> [SBool]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    sb ((SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    rest) [SBool]
    rest)
      where (SBool
    sb : [SBool]
    rest) = SWord32 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE (SWord32 -> [SBool]) -> SWord32 -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ SFloat -> SWord32
    sFloatAsSWord32 SFloat
    f

    -- | Inverse transformation to 'sFloatAsComparableSWord32'.
    sComparableSWord32AsSFloat :: SWord32 -> SFloat
    sComparableSWord32AsSFloat :: SWord32 -> SFloat
    sComparableSWord32AsSFloat SWord32
    w = SWord32 -> SFloat
    sWord32AsSFloat (SWord32 -> SFloat) -> SWord32 -> SFloat
    forall a b. (a -> b) -> a -> b
    $ SBool -> SWord32 -> SWord32 -> SWord32
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    sb ([SBool] -> SWord32
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord32) -> [SBool] -> SWord32
    forall a b. (a -> b) -> a -> b
    $ SBool
    sFalse SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool]
    rest) ([SBool] -> SWord32
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord32) -> [SBool] -> SWord32
    forall a b. (a -> b) -> a -> b
    $ (SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    allBits)
      where allBits :: [SBool]
    allBits@(SBool
    sb : [SBool]
    rest) = SWord32 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SWord32
    w

    -- | Convert a double to a comparable 'SWord64'. The trick is to ignore the
    -- sign of -0, and if it's a negative value flip all the bits, and otherwise
    -- only flip the sign bit. This is known as the lexicographic ordering on doubles
    -- and it works as long as you do not have a @NaN@.
    sDoubleAsComparableSWord64 :: SDouble -> SWord64
    sDoubleAsComparableSWord64 :: SDouble -> SWord64
    sDoubleAsComparableSWord64 SDouble
    d = SBool -> SWord64 -> SWord64 -> SWord64
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SDouble -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegativeZero SDouble
    d) (SDouble -> SWord64
    sDoubleAsComparableSWord64 SDouble
    0) ([SBool] -> SWord64
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord64) -> [SBool] -> SWord64
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot SBool
    sb SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : SBool -> [SBool] -> [SBool] -> [SBool]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    sb ((SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    rest) [SBool]
    rest)
      where (SBool
    sb : [SBool]
    rest) = SWord64 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE (SWord64 -> [SBool]) -> SWord64 -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ SDouble -> SWord64
    sDoubleAsSWord64 SDouble
    d

    -- | Inverse transformation to 'sDoubleAsComparableSWord64'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
    -- Otherwise, it's faithful:
    sComparableSWord64AsSDouble :: SWord64 -> SDouble
    sComparableSWord64AsSDouble :: SWord64 -> SDouble
    sComparableSWord64AsSDouble SWord64
    w = SWord64 -> SDouble
    sWord64AsSDouble (SWord64 -> SDouble) -> SWord64 -> SDouble
    forall a b. (a -> b) -> a -> b
    $ SBool -> SWord64 -> SWord64 -> SWord64
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    sb ([SBool] -> SWord64
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord64) -> [SBool] -> SWord64
    forall a b. (a -> b) -> a -> b
    $ SBool
    sFalse SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool]
    rest) ([SBool] -> SWord64
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SWord64) -> [SBool] -> SWord64
    forall a b. (a -> b) -> a -> b
    $ (SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    allBits)
      where allBits :: [SBool]
    allBits@(SBool
    sb : [SBool]
    rest) = SWord64 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SWord64
    w

    -- | 'Float' instance for 'Metric' goes through the lexicographic ordering on 'Word32'.
    -- It implicitly makes sure that the value is not @NaN@.
    instance Metric Float where

       type MetricSpace Float = Word32
       toMetricSpace :: SFloat -> SBV (MetricSpace Float)
    toMetricSpace          = SFloat -> SWord32
    SFloat -> SBV (MetricSpace Float)
    sFloatAsComparableSWord32
       fromMetricSpace :: SBV (MetricSpace Float) -> SFloat
    fromMetricSpace        = SWord32 -> SFloat
    SBV (MetricSpace Float) -> SFloat
    sComparableSWord32AsSFloat

       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SFloat -> m ()
    msMinimize [Char]
    nm SFloat
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SFloat -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SFloat
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord32 -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord32 -> SVal) -> Objective SWord32 -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord32 -> Objective SWord32
    forall a. [Char] -> a -> Objective a
    Minimize [Char]
    nm (SFloat -> SBV (MetricSpace Float)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SFloat
    o)

       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SFloat -> m ()
    msMaximize [Char]
    nm SFloat
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SFloat -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SFloat
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord32 -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord32 -> SVal) -> Objective SWord32 -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord32 -> Objective SWord32
    forall a. [Char] -> a -> Objective a
    Maximize [Char]
    nm (SFloat -> SBV (MetricSpace Float)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SFloat
    o)

    -- | 'Double' instance for 'Metric' goes through the lexicographic ordering on 'Word64'.
    -- It implicitly makes sure that the value is not @NaN@.
    instance Metric Double where

       type MetricSpace Double = Word64
       toMetricSpace :: SDouble -> SBV (MetricSpace Double)
    toMetricSpace           = SDouble -> SWord64
    SDouble -> SBV (MetricSpace Double)
    sDoubleAsComparableSWord64
       fromMetricSpace :: SBV (MetricSpace Double) -> SDouble
    fromMetricSpace         = SWord64 -> SDouble
    SBV (MetricSpace Double) -> SDouble
    sComparableSWord64AsSDouble

       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SDouble -> m ()
    msMinimize [Char]
    nm SDouble
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SDouble -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SDouble
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord64 -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord64 -> SVal) -> Objective SWord64 -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord64 -> Objective SWord64
    forall a. [Char] -> a -> Objective a
    Minimize [Char]
    nm (SDouble -> SBV (MetricSpace Double)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SDouble
    o)

       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SDouble -> m ()
    msMaximize [Char]
    nm SDouble
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SDouble -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SDouble
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord64 -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord64 -> SVal) -> Objective SWord64 -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord64 -> Objective SWord64
    forall a. [Char] -> a -> Objective a
    Maximize [Char]
    nm (SDouble -> SBV (MetricSpace Double)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SDouble
    o)

    -- | Real instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
    instance ValidFloat eb sb => Real (FloatingPoint eb sb) where
      toRational :: FloatingPoint eb sb -> Rational
    toRational (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    r)) = case BigFloat -> BFRep
    bfToRep BigFloat
    r of
                                                BFRep
    BFNaN     -> Double -> Rational
    forall a. Real a => a -> Rational
    toRational (Double
    0Double -> Double -> Double
    forall a. Fractional a => a -> a -> a
    /Double
    0 :: Double)
                                                BFRep Sign
    s BFNum
    n -> case BFNum
    n of
                                                               BFNum
    Zero    -> Integer
    0 Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    1
                                                               BFNum
    Inf     -> (if Sign
    s Sign -> Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sign
    Neg then -Integer
    1 else Integer
    1) Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    0
                                                               Num Integer
    x Int64
    y -> -- The value here is x * 2^y
                                                                          let v :: Integer
                                                                              v :: Integer
    v   = Integer
    2 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer -> Integer
    forall a. Num a => a -> a
    abs (Int64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int64
    y :: Integer)
                                                                              sgn :: Rational -> Rational
    sgn = if Sign
    s Sign -> Sign -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sign
    Neg then ((-Rational
    1) Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    *) else Rational -> Rational
    forall a. a -> a
    id
                                                                          in if Int64
    y Int64 -> Int64 -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int64
    0
                                                                                then Rational -> Rational
    sgn (Rational -> Rational) -> Rational -> Rational
    forall a b. (a -> b) -> a -> b
    $ Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    v Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    1
                                                                                else Rational -> Rational
    sgn (Rational -> Rational) -> Rational -> Rational
    forall a b. (a -> b) -> a -> b
    $ Integer
    x Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    v

    -- | RealFrac instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
    instance ValidFloat eb sb => RealFrac (FloatingPoint eb sb) where
      properFraction :: forall b.
    Integral b =>
    FloatingPoint eb sb -> (b, FloatingPoint eb sb)
    properFraction (FloatingPoint FP
    f) = (b
    a, FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint FP
    b)
         where (b
    a, FP
    b) = FP -> (b, FP)
    forall b. Integral b => FP -> (b, FP)
    forall a b. (RealFrac a, Integral b) => a -> (b, a)
    properFraction FP
    f

    -- | RealFloat instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
    instance ValidFloat eb sb => RealFloat (FloatingPoint eb sb) where
      floatRadix :: FloatingPoint eb sb -> Integer
    floatRadix     (FloatingPoint FP
    f) = FP -> Integer
    forall a. RealFloat a => a -> Integer
    floatRadix     FP
    f
      floatDigits :: FloatingPoint eb sb -> Int
    floatDigits    (FloatingPoint FP
    f) = FP -> Int
    forall a. RealFloat a => a -> Int
    floatDigits    FP
    f
      floatRange :: FloatingPoint eb sb -> (Int, Int)
    floatRange     (FloatingPoint FP
    f) = FP -> (Int, Int)
    forall a. RealFloat a => a -> (Int, Int)
    floatRange     FP
    f
      isNaN :: FloatingPoint eb sb -> Bool
    isNaN          (FloatingPoint FP
    f) = FP -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN          FP
    f
      isInfinite :: FloatingPoint eb sb -> Bool
    isInfinite     (FloatingPoint FP
    f) = FP -> Bool
    forall a. RealFloat a => a -> Bool
    isInfinite     FP
    f
      isDenormalized :: FloatingPoint eb sb -> Bool
    isDenormalized (FloatingPoint FP
    f) = FP -> Bool
    forall a. RealFloat a => a -> Bool
    isDenormalized FP
    f
      isNegativeZero :: FloatingPoint eb sb -> Bool
    isNegativeZero (FloatingPoint FP
    f) = FP -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero FP
    f
      isIEEE :: FloatingPoint eb sb -> Bool
    isIEEE         (FloatingPoint FP
    f) = FP -> Bool
    forall a. RealFloat a => a -> Bool
    isIEEE         FP
    f
      decodeFloat :: FloatingPoint eb sb -> (Integer, Int)
    decodeFloat    (FloatingPoint FP
    f) = FP -> (Integer, Int)
    forall a. RealFloat a => a -> (Integer, Int)
    decodeFloat    FP
    f

      encodeFloat :: Integer -> Int -> FloatingPoint eb sb
    encodeFloat Integer
    m Int
    n = FloatingPoint eb sb
    res
         where res :: FloatingPoint eb sb
    res = FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (FP -> FloatingPoint eb sb) -> FP -> FloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> Integer -> Int -> FP
    fpEncodeFloat Int
    ei Int
    si Integer
    m Int
    n
               ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
               si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

    -- | Convert a float to the word containing the corresponding bit pattern
    sFloatingPointAsSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsSWord :: forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsSWord (SBV SVal
    v) = SVal -> SBV (WordN (eb + sb))
    forall a. SVal -> SBV a
    SBV (SVal -> SVal
    svFloatingPointAsSWord SVal
    v)

    -- | Convert a float to the correct size word, that can be used in lexicographic ordering. Used in optimization.
    sFloatingPointAsComparableSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsComparableSWord :: forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsComparableSWord SFloatingPoint eb sb
    f = SBool
    -> SBV (WordN (eb + sb))
    -> SBV (WordN (eb + sb))
    -> SBV (WordN (eb + sb))
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SFloatingPoint eb sb -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegativeZero SFloatingPoint eb sb
    f) SBV (WordN (eb + sb))
    posZero ([SBool] -> SBV (WordN (eb + sb))
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV (WordN (eb + sb)))
    -> [SBool] -> SBV (WordN (eb + sb))
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot SBool
    sb SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : SBool -> [SBool] -> [SBool] -> [SBool]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    sb ((SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    rest) [SBool]
    rest)
      where posZero :: SBV (WordN (eb + sb))
    posZero     = SFloatingPoint eb sb -> SBV (WordN (eb + sb))
    forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsComparableSWord (SFloatingPoint eb sb
    0 :: SFloatingPoint eb sb)
            (SBool
    sb : [SBool]
    rest) = SBV (WordN (eb + sb)) -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE (SFloatingPoint eb sb -> SBV (WordN (eb + sb))
    forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsSWord SFloatingPoint eb sb
    f :: SWord (eb + sb))

    -- | Inverse transformation to 'sFloatingPointAsComparableSWord'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
    -- Otherwise, it's faithful:
    sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
    sComparableSWordAsSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
    SWord (eb + sb) -> SFloatingPoint eb sb
    sComparableSWordAsSFloatingPoint SBV (WordN (eb + sb))
    w = SBV (WordN (eb + sb)) -> SFloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat).
    (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
    SWord (eb + sb) -> SFloatingPoint eb sb
    sWordAsSFloatingPoint (SBV (WordN (eb + sb)) -> SFloatingPoint eb sb)
    -> SBV (WordN (eb + sb)) -> SFloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ SBool
    -> SBV (WordN (eb + sb))
    -> SBV (WordN (eb + sb))
    -> SBV (WordN (eb + sb))
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    signBit ([SBool] -> SBV (WordN (eb + sb))
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV (WordN (eb + sb)))
    -> [SBool] -> SBV (WordN (eb + sb))
    forall a b. (a -> b) -> a -> b
    $ SBool
    sFalse SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [SBool]
    rest) ([SBool] -> SBV (WordN (eb + sb))
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV (WordN (eb + sb)))
    -> [SBool] -> SBV (WordN (eb + sb))
    forall a b. (a -> b) -> a -> b
    $ (SBool -> SBool) -> [SBool] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> SBool
    sNot [SBool]
    allBits)
      where allBits :: [SBool]
    allBits@(SBool
    signBit : [SBool]
    rest) = SBV (WordN (eb + sb)) -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SBV (WordN (eb + sb))
    w

    -- | Convert a word to an arbitrary float, by reinterpreting the bits of the word as the corresponding bits of the float.
    sWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
    sWordAsSFloatingPoint :: forall (eb :: Nat) (sb :: Nat).
    (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
    SWord (eb + sb) -> SFloatingPoint eb sb
    sWordAsSFloatingPoint SWord (eb + sb)
    sw
       | Just (WordN (eb + sb)
    f :: WordN (eb + sb)) <- SWord (eb + sb) -> Maybe (WordN (eb + sb))
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SWord (eb + sb)
    sw
       = let ext :: Int -> Bool
    ext Int
    i = WordN (eb + sb)
    f WordN (eb + sb) -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    i
             exts :: [Int] -> [Bool]
    exts  = (Int -> Bool) -> [Int] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Bool
    ext
             (Bool
    s, [Bool]
    ebits, [Bool]
    sigbits) = (Int -> Bool
    ext (Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1), [Int] -> [Bool]
    exts [Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2, Int
    ei Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    3 .. Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1], [Int] -> [Bool]
    exts [Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2, Int
    si Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    3 .. Int
    0])

             cvt :: [Bool] -> Integer
             cvt :: [Bool] -> Integer
    cvt = (Bool -> Integer -> Integer) -> Integer -> [Bool] -> Integer
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\Bool
    b Integer
    sofar -> Integer
    2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    sofar Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + if Bool
    b then Integer
    1 else Integer
    0) Integer
    0 ([Bool] -> Integer) -> ([Bool] -> [Bool]) -> [Bool] -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Bool] -> [Bool]
    forall a. [a] -> [a]
    reverse

             eIntV :: Integer
    eIntV = [Bool] -> Integer
    cvt [Bool]
    ebits
             sIntV :: Integer
    sIntV = [Bool] -> Integer
    cvt [Bool]
    sigbits
             fp :: FP
    fp    = Bool -> (Integer, Int) -> (Integer, Int) -> FP
    fpFromRawRep Bool
    s (Integer
    eIntV, Int
    ei) (Integer
    sIntV, Int
    si)
         in FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint FP
    fp
       | Bool
    True
       = SVal -> SBV (FloatingPoint eb sb)
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kTo (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y)))
       where ei :: Int
    ei   = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
             si :: Int
    si   = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)
             kTo :: Kind
    kTo  = Int -> Int -> Kind
    KFP Int
    ei Int
    si
             y :: State -> IO SV
    y State
    st = do SV
    xsv <- State -> SWord (eb + sb) -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SWord (eb + sb)
    sw
                       State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kTo (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret (SWord (eb + sb) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SWord (eb + sb)
    sw) Kind
    kTo)) [SV
    xsv])

    instance (BVIsNonZero (eb + sb), KnownNat (eb + sb), ValidFloat eb sb) => Metric (FloatingPoint eb sb) where

       type MetricSpace (FloatingPoint eb sb) = WordN (eb + sb)
       toMetricSpace :: SBV (FloatingPoint eb sb)
    -> SBV (MetricSpace (FloatingPoint eb sb))
    toMetricSpace                          = SBV (FloatingPoint eb sb)
    -> SBV (MetricSpace (FloatingPoint eb sb))
    SBV (FloatingPoint eb sb) -> SWord (eb + sb)
    forall (eb :: Nat) (sb :: Nat).
    (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
    SFloatingPoint eb sb -> SWord (eb + sb)
    sFloatingPointAsComparableSWord
       fromMetricSpace :: SBV (MetricSpace (FloatingPoint eb sb))
    -> SBV (FloatingPoint eb sb)
    fromMetricSpace                        = SBV (MetricSpace (FloatingPoint eb sb))
    -> SBV (FloatingPoint eb sb)
    SWord (eb + sb) -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) =>
    SWord (eb + sb) -> SFloatingPoint eb sb
    sComparableSWordAsSFloatingPoint

       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SBV (FloatingPoint eb sb) -> m ()
    msMinimize [Char]
    nm SBV (FloatingPoint eb sb)
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SBV (FloatingPoint eb sb) -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV (FloatingPoint eb sb)
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord (eb + sb) -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord (eb + sb) -> SVal)
    -> Objective (SWord (eb + sb)) -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord (eb + sb) -> Objective (SWord (eb + sb))
    forall a. [Char] -> a -> Objective a
    Minimize [Char]
    nm (SBV (FloatingPoint eb sb)
    -> SBV (MetricSpace (FloatingPoint eb sb))
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV (FloatingPoint eb sb)
    o)

       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    [Char] -> SBV (FloatingPoint eb sb) -> m ()
    msMaximize [Char]
    nm SBV (FloatingPoint eb sb)
    o = do SBool -> m ()
    forall a. QuantifiedBool a => a -> m ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SBV (FloatingPoint eb sb) -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV (FloatingPoint eb sb)
    o
                            Objective SVal -> m ()
    forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
    addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
    forall a b. (a -> b) -> a -> b
    $ SWord (eb + sb) -> SVal
    forall a. SBV a -> SVal
    unSBV (SWord (eb + sb) -> SVal)
    -> Objective (SWord (eb + sb)) -> Objective SVal
    forall a b. (a -> b) -> Objective a -> Objective b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Char] -> SWord (eb + sb) -> Objective (SWord (eb + sb))
    forall a. [Char] -> a -> Objective a
    Maximize [Char]
    nm (SBV (FloatingPoint eb sb)
    -> SBV (MetricSpace (FloatingPoint eb sb))
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV (FloatingPoint eb sb)
    o)

    -- Map SBV's rounding modes to LibBF's
    rmToRM :: SRoundingMode -> Maybe RoundMode
    rmToRM :: SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    srm = RoundingMode -> RoundMode
    cvt (RoundingMode -> RoundMode)
    -> Maybe RoundingMode -> Maybe RoundMode
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    srm
      where cvt :: RoundingMode -> RoundMode
    cvt RoundingMode
    RoundNearestTiesToEven = RoundMode
    NearEven
            cvt RoundingMode
    RoundNearestTiesToAway = RoundMode
    NearAway
            cvt RoundingMode
    RoundTowardPositive    = RoundMode
    ToPosInf
            cvt RoundingMode
    RoundTowardNegative    = RoundMode
    ToNegInf
            cvt RoundingMode
    RoundTowardZero        = RoundMode
    ToZero

    -- | Lift a 1 arg Big-float op
    lift1FP :: forall eb sb. ValidFloat eb sb =>
               (BFOpts -> BigFloat -> (BigFloat, Status))
            -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
            -> SRoundingMode
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
    lift1FP :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift1FP BFOpts -> BigFloat -> (BigFloat, Status)
    bfOp Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
    mkDef SRoundingMode
    rm SFloatingPoint eb sb
    a
      | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    a
      , Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
      = FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SFloatingPoint eb sb)
    -> FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> (BigFloat, Status)
    bfOp (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v)))
      | Bool
    True
      = Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
    mkDef (SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just SRoundingMode
    rm) SFloatingPoint eb sb
    a
      where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
            si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

    -- | Lift a 2 arg Big-float op
    lift2FP :: forall eb sb. ValidFloat eb sb =>
               (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
            -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
            -> SRoundingMode
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
    lift2FP :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfOp Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    mkDef SRoundingMode
    rm SFloatingPoint eb sb
    a SFloatingPoint eb sb
    b
      | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v1)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    a
      , Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v2)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    b
      , Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
      = FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SFloatingPoint eb sb)
    -> FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfOp (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v1 BigFloat
    v2)))
      | Bool
    True
      = Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    mkDef (SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just SRoundingMode
    rm) SFloatingPoint eb sb
    a SFloatingPoint eb sb
    b
      where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
            si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

    -- | Lift a 3 arg Big-float op
    lift3FP :: forall eb sb. ValidFloat eb sb =>
               (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
            -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
            -> SRoundingMode
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
            -> SFloatingPoint eb sb
    lift3FP :: forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift3FP BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfOp Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    mkDef SRoundingMode
    rm SFloatingPoint eb sb
    a SFloatingPoint eb sb
    b SFloatingPoint eb sb
    c
      | Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v1)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    a
      , Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v2)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    b
      , Just (FloatingPoint (FP Int
    _ Int
    _ BigFloat
    v3)) <- SFloatingPoint eb sb -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SFloatingPoint eb sb
    c
      , Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
      = FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SFloatingPoint eb sb)
    -> FloatingPoint eb sb -> SFloatingPoint eb sb
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfOp (Int -> Int -> RoundMode -> BFOpts
    forall a. Integral a => a -> a -> RoundMode -> BFOpts
    mkBFOpts Int
    ei Int
    si RoundMode
    brm) BigFloat
    v1 BigFloat
    v2 BigFloat
    v3)))
      | Bool
    True
      = Maybe SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    mkDef (SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just SRoundingMode
    rm) SFloatingPoint eb sb
    a SFloatingPoint eb sb
    b SFloatingPoint eb sb
    c
      where ei :: Int
    ei = Proxy eb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @eb)
            si :: Int
    si = Proxy sb -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @sb)

    -- Sized-floats have a special instance, since it can handle arbitrary rounding modes when it matters.
    instance ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) where
      fpAdd :: SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    fpAdd  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfAdd      (FPOp
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 FPOp
    FP_Add  ((FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    forall a. Num a => a -> a -> a
    (+)))
      fpSub :: SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    fpSub  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfSub      (FPOp
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 FPOp
    FP_Sub  ((FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just (-)))
      fpMul :: SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    fpMul  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfMul      (FPOp
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 FPOp
    FP_Mul  ((FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    forall a. Num a => a -> a -> a
    (*)))
      fpDiv :: SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    fpDiv  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift2FP BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfDiv      (FPOp
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 FPOp
    FP_Div  ((FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe
         (FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb
    forall a. Fractional a => a -> a -> a
    (/)))
      fpFMA :: SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    fpFMA  = (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb)
        -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift3FP BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
    bfFMA      (FPOp
    -> Maybe
         (FloatingPoint eb sb
          -> FloatingPoint eb sb
          -> FloatingPoint eb sb
          -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp
    -> Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    lift3 FPOp
    FP_FMA  Maybe
      (FloatingPoint eb sb
       -> FloatingPoint eb sb
       -> FloatingPoint eb sb
       -> FloatingPoint eb sb)
    forall a. Maybe a
    Nothing)
      fpSqrt :: SRoundingMode
    -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
    fpSqrt = (BFOpts -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb))
    -> SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall (eb :: Nat) (sb :: Nat).
    ValidFloat eb sb =>
    (BFOpts -> BigFloat -> (BigFloat, Status))
    -> (Maybe SRoundingMode
        -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
    -> SRoundingMode
    -> SFloatingPoint eb sb
    -> SFloatingPoint eb sb
    lift1FP BFOpts -> BigFloat -> (BigFloat, Status)
    bfSqrt     (FPOp
    -> Maybe (FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1 FPOp
    FP_Sqrt ((FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe (FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just FloatingPoint eb sb -> FloatingPoint eb sb
    forall a. Floating a => a -> a
    sqrt))

      fpRoundToIntegral :: SRoundingMode
    -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
    fpRoundToIntegral SRoundingMode
    rm SBV (FloatingPoint eb sb)
    a
        | Just (FloatingPoint (FP Int
    ei Int
    si BigFloat
    v)) <- SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV (FloatingPoint eb sb)
    a
        , Just RoundMode
    brm <- SRoundingMode -> Maybe RoundMode
    rmToRM SRoundingMode
    rm
        = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a. SymVal a => a -> SBV a
    literal (FloatingPoint eb sb -> SBV (FloatingPoint eb sb))
    -> FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
    forall a b. (a -> b) -> a -> b
    $ FP -> FloatingPoint eb sb
    forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
    FloatingPoint (Int -> Int -> BigFloat -> FP
    FP Int
    ei Int
    si ((BigFloat, Status) -> BigFloat
    forall a b. (a, b) -> a
    fst (RoundMode -> BigFloat -> (BigFloat, Status)
    bfRoundInt RoundMode
    brm BigFloat
    v)))
        | Bool
    True
        = FPOp
    -> Maybe (FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe SRoundingMode
    -> SBV (FloatingPoint eb sb)
    -> SBV (FloatingPoint eb sb)
    forall a.
    SymVal a =>
    FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1 FPOp
    FP_RoundToIntegral ((FloatingPoint eb sb -> FloatingPoint eb sb)
    -> Maybe (FloatingPoint eb sb -> FloatingPoint eb sb)
    forall a. a -> Maybe a
    Just FloatingPoint eb sb -> FloatingPoint eb sb
    forall a. RealFloat a => a -> a
    fpRoundToIntegralH) (SRoundingMode -> Maybe SRoundingMode
    forall a. a -> Maybe a
    Just SRoundingMode
    rm) SBV (FloatingPoint eb sb)
    a

      -- All other operations are agnostic to the rounding mode, hence the defaults are sufficient:
      --
      --       fpAbs            :: SBV a -> SBV a
      --       fpNeg            :: SBV a -> SBV a
      --       fpRem            :: SBV a -> SBV a -> SBV a
      --       fpMin            :: SBV a -> SBV a -> SBV a
      --       fpMax            :: SBV a -> SBV a -> SBV a
      --       fpIsEqualObject  :: SBV a -> SBV a -> SBool
      --       fpIsNormal       :: SBV a -> SBool
      --       fpIsSubnormal    :: SBV a -> SBool
      --       fpIsZero         :: SBV a -> SBool
      --       fpIsInfinite     :: SBV a -> SBool
      --       fpIsNaN          :: SBV a -> SBool
      --       fpIsNegative     :: SBV a -> SBool
      --       fpIsPositive     :: SBV a -> SBool
      --       fpIsNegativeZero :: SBV a -> SBool
      --       fpIsPositiveZero :: SBV a -> SBool
      --       fpIsPoint        :: SBV a -> SBool

    {- HLint ignore module "Reduce duplication" -}