    -----------------------------------------------------------------------------
    -- |
    -- 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 FlexibleInstances    #-}
    {-# LANGUAGE Rank2Types           #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeFamilies         #-}

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

    module Data.SBV.Core.Floating (
             IEEEFloating(..), IEEEFloatConvertible(..)
           , sFloatAsSWord32, sDoubleAsSWord64, sWord32AsSFloat, sWord64AsSDouble
           , blastSFloat, blastSDouble
           , sFloatAsComparableSWord32, sDoubleAsComparableSWord64
           ) where

    import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord)

    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.Data
    import Data.SBV.Core.Model
    import Data.SBV.Core.Symbolic (addSValOptGoal)

    import Data.SBV.Utils.Numeric

    -- For doctest use only
    --
    -- $setup
    -- >>> :set -XTypeApplications
    -- >>> :set -XRankNTypes
    -- >>> :set -XScopedTypeVariables
    -- >>> import Data.SBV.Provers.Prover (prove)

    -- | 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
    == 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      (\x :: a
    x -> a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < 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      (\x :: a
    x -> a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 Bool -> Bool -> Bool
    && Bool -> Bool
    not (a -> Bool
    forall a. RealFloat a => a -> Bool
    isNegativeZero a
    x))
      fpIsNegativeZero x :: 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 x :: 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        x :: 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

    -- | Capture convertability from/to FloatingPoint representations.
    --
    -- Conversions to float: 'toSFloat' and 'toSDouble' simply return the
    -- nearest representable float from the given type based on the rounding
    -- mode provided.
    --
    -- Conversions from float: 'fromSFloat' and 'fromSDouble' functions do
    -- the reverse conversion. However some care is needed when given values
    -- that are not representable in the integral target domain. For instance,
    -- converting an 'SFloat' to an 'SInt8' is problematic. The rules are as follows:
    --
    -- If the input value is a finite point and when rounded in the given rounding mode to an
    -- integral value lies within the target bounds, then that result is returned.
    -- (This is the regular interpretation of rounding in IEEE754.)
    --
    -- Otherwise (i.e., if the integral value in the float or double domain) doesn't
    -- fit into the target type, then the result is unspecified. Note that if the input
    -- is @+oo@, @-oo@, or @NaN@, then the result is unspecified.
    --
    -- Due to the unspecified nature of conversions, SBV will never constant fold
    -- conversions from floats to integral values. That is, you will always get a
    -- symbolic value as output. (Conversions from floats to other floats will be
    -- constant folded. Conversions from integral values to floats will also be
    -- constant folded.)
    --
    -- Note that unspecified really means unspecified: In particular, SBV makes
    -- no guarantees about matching the behavior between what you might get in
    -- Haskell, via SMT-Lib, or the C-translation. If the input value is out-of-bounds
    -- as defined above, or is @NaN@ or @oo@ or @-oo@, then all bets are off. In particular
    -- C and SMTLib are decidedly undefine this case, though that doesn't mean they do the
    -- same thing! Same goes for Haskell, which seems to convert via Int64, but we do
    -- not model that behavior in SBV as it doesn't seem to be intentional nor well documented.
    --
    -- You can check for @NaN@, @oo@ and @-oo@, using the predicates 'fpIsNaN', 'fpIsInfinite',
    -- and 'fpIsPositive', 'fpIsNegative' predicates, respectively; and do the proper conversion
    -- based on your needs. (0 is a good choice, as are min/max bounds of the target type.)
    --
    -- Currently, SBV provides no predicates to check if a value would lie within range for a
    -- particular conversion task, as this depends on the rounding mode and the types involved
    -- and can be rather tricky to determine. (See <http://github.com/LeventErkok/sbv/issues/456>
    -- for a discussion of the issues involved.) In a future release, we hope to be able to
    -- provide underflow and overflow predicates for these conversions as well.
    class SymVal a => IEEEFloatConvertible a where
      -- | Convert from an IEEE74 single precision float.
      fromSFloat :: SRoundingMode -> SFloat -> SBV a
      fromSFloat = SRoundingMode -> SBV Float -> SBV a
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat

      -- | Convert to an IEEE-754 Single-precision float.
      --
      -- >>> :{
      -- roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
      -- roundTrip m x = fromSFloat m (toSFloat m x) .== x
      -- :}
      --
      -- >>> prove $ roundTrip @Int8
      -- Q.E.D.
      -- >>> prove $ roundTrip @Word8
      -- Q.E.D.
      -- >>> prove $ roundTrip @Int16
      -- Q.E.D.
      -- >>> prove $ roundTrip @Word16
      -- Q.E.D.
      -- >>> prove $ roundTrip @Int32
      -- Falsifiable. Counter-example:
      --   s0 = RoundNearestTiesToEven :: RoundingMode
      --   s1 =             -264306721 :: Int32
      --
      -- Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
      --
      -- >>> toRational (-264306721 :: Float)
      -- (-264306720) % 1
      --
      -- Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as
      -- the magnitude increases to be able to cover all the integer values representable.
      toSFloat :: SRoundingMode -> SBV a -> SFloat

      -- default definition if we have an integral like
      default toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat
      toSFloat = (a -> Maybe Float) -> SRoundingMode -> SBV a -> SBV Float
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (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 -> SBV Double -> SBV a
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat

      -- | Convert to an IEEE-754 Double-precision float.
      --
      -- >>> :{
      -- roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
      -- roundTrip m x = fromSDouble m (toSDouble m x) .== x
      -- :}
      --
      -- >>> prove $ roundTrip @Int8
      -- Q.E.D.
      -- >>> prove $ roundTrip @Word8
      -- Q.E.D.
      -- >>> prove $ roundTrip @Int16
      -- Q.E.D.
      -- >>> prove $ roundTrip @Word16
      -- Q.E.D.
      -- >>> prove $ roundTrip @Int32
      -- Q.E.D.
      -- >>> prove $ roundTrip @Word32
      -- Q.E.D.
      -- >>> prove $ roundTrip @Int64
      -- Falsifiable. Counter-example:
      --   s0 =  RoundTowardNegative :: RoundingMode
      --   s1 = -8069753317450726624 :: Int64
      --
      -- Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the
      -- integer value for all possible values:
      --
      -- >>>  toRational ( -8069753317450726624 :: Double)
      -- (-8069753317450726400) % 1
      --
      -- In this case the numerator is off by 224!
      toSDouble :: SRoundingMode -> SBV a -> SDouble

      -- default definition if we have an integral like
      default toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble
      toSDouble = (a -> Maybe Double) -> SRoundingMode -> SBV a -> SBV Double
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (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)

    -- | 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 :: SRoundingMode -> SBV a -> SBV r
    genericFromFloat rm :: SRoundingMode
    rm f :: 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 (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)
            r :: State -> IO SV
    r st :: 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.
    genericToFloat :: forall a r. (IEEEFloatConvertible a, IEEEFloating r)
                   => (a -> Maybe r)     -- How to convert concretely, if possible
                   -> SRoundingMode      -- Rounding mode
                   -> SBV a              -- Input convertible
                   -> SBV r
    genericToFloat :: (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat converter :: a -> Maybe r
    converter rm :: SRoundingMode
    rm i :: SBV a
    i
      | Just w :: a
    w <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    i, Just RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm, Just result :: r
    result <- a -> Maybe r
    converter 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 (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)
            r :: State -> IO SV
    r st :: 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 -> SBV Float -> SBV Float
    toSFloat  _ f :: SBV Float
    f = SBV Float
    f
      toSDouble :: SRoundingMode -> SBV Float -> SBV Double
    toSDouble     = (Float -> Maybe Double) -> SRoundingMode -> SBV Float -> SBV Double
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (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)

      fromSFloat :: SRoundingMode -> SBV Float -> SBV Float
    fromSFloat  _  f :: SBV Float
    f = SBV Float
    f
      fromSDouble :: SRoundingMode -> SBV Double -> SBV Float
    fromSDouble rm :: SRoundingMode
    rm f :: SBV Double
    f
        | Just RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm
        , Just fv :: Double
    fv                     <- SBV Double -> Maybe Double
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV Double
    f
        = Float -> SBV Float
    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 -> SBV Double -> SBV Float
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SBV Double
    f

    instance IEEEFloatConvertible Double where
      toSFloat :: SRoundingMode -> SBV Double -> SBV Float
    toSFloat      = (Double -> Maybe Float) -> SRoundingMode -> SBV Double -> SBV Float
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (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 -> SBV Double -> SBV Double
    toSDouble _ d :: SBV Double
    d = SBV Double
    d

      fromSDouble :: SRoundingMode -> SBV Double -> SBV Double
    fromSDouble _  d :: SBV Double
    d = SBV Double
    d
      fromSFloat :: SRoundingMode -> SBV Float -> SBV Double
    fromSFloat  rm :: SRoundingMode
    rm d :: SBV Float
    d
        | Just RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SRoundingMode
    rm
        , Just dv :: Float
    dv                     <- SBV Float -> Maybe Float
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV Float
    d
        = Double -> SBV Double
    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 -> SBV Float -> SBV Double
    forall a r.
    (IEEEFloating a, IEEEFloatConvertible r) =>
    SRoundingMode -> SBV a -> SBV r
    genericFromFloat SRoundingMode
    rm SBV Float
    d

    -- For AlgReal; be careful to only process exact rationals concretely
    instance IEEEFloatConvertible AlgReal where
      toSFloat :: SRoundingMode -> SBV AlgReal -> SBV Float
    toSFloat  = (AlgReal -> Maybe Float)
    -> SRoundingMode -> SBV AlgReal -> SBV Float
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (\r :: AlgReal
    r -> if AlgReal -> Bool
    isExactRational AlgReal
    r then Float -> Maybe Float
    forall a. a -> Maybe a
    Just (Rational -> Float
    forall a. Fractional a => Rational -> a
    fromRational (AlgReal -> Rational
    forall a. Real a => a -> Rational
    toRational AlgReal
    r)) else Maybe Float
    forall a. Maybe a
    Nothing)
      toSDouble :: SRoundingMode -> SBV AlgReal -> SBV Double
    toSDouble = (AlgReal -> Maybe Double)
    -> SRoundingMode -> SBV AlgReal -> SBV Double
    forall a r.
    (IEEEFloatConvertible a, IEEEFloating r) =>
    (a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
    genericToFloat (\r :: AlgReal
    r -> if AlgReal -> Bool
    isExactRational AlgReal
    r then Double -> Maybe Double
    forall a. a -> Maybe a
    Just (Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational (AlgReal -> Rational
    forall a. Real a => a -> Rational
    toRational AlgReal
    r)) else Maybe Double
    forall a. Maybe a
    Nothing)

    -- | 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 :: Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
    concEval1 mbOp :: Maybe (a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: 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
                                 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 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 (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 :: Maybe (a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)
    concEval2 mbOp :: Maybe (a -> a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: 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
                                    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 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 (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 :: Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool
    concEval2B mbOp :: Maybe (a -> a -> Bool)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: 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
                                     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 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 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 :: Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)
    concEval3 mbOp :: Maybe (a -> a -> a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: SBV a
    b c :: 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
                                     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 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 (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 _  Nothing   as :: [SV]
    as = [SV] -> IO [SV]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SV]
    as
    addRM st :: State
    st (Just rm :: SRoundingMode
    rm) as :: [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 (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 :: FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a
    lift1 w :: FPOp
    w mbOp :: Maybe (a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a
      | Just cv :: 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 st :: 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 :: FPOp -> (a -> Bool) -> SBV a -> SBool
    lift1B w :: FPOp
    w f :: a -> Bool
    f a :: SBV a
    a
       | Just v :: 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 st :: 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 :: FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    lift2 w :: FPOp
    w mbOp :: Maybe (a -> a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: SBV a
    b
      | Just cv :: 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 st :: 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 :: FPOp
    -> Maybe (a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    liftMM w :: FPOp
    w mbOp :: Maybe (a -> a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: SBV a
    b
      | Just v1 :: a
    v1 <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a
      , Just v2 :: 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 cv :: 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 x :: a
    x = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == 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 st :: 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 :: FPOp
    -> Maybe (a -> a -> Bool)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBool
    lift2B w :: FPOp
    w mbOp :: Maybe (a -> a -> Bool)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: SBV a
    b
      | Just cv :: 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 st :: 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 :: FPOp
    -> Maybe (a -> a -> a -> a)
    -> Maybe SRoundingMode
    -> SBV a
    -> SBV a
    -> SBV a
    -> SBV a
    lift3 w :: FPOp
    w mbOp :: Maybe (a -> a -> a -> a)
    mbOp mbRm :: Maybe SRoundingMode
    mbRm a :: SBV a
    a b :: SBV a
    b c :: SBV a
    c
      | Just cv :: 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 st :: 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 :: SBV Float -> SBV Word32
    sFloatAsSWord32 fVal :: SBV Float
    fVal
      | Just f :: Float
    f <- SBV Float -> Maybe Float
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV Float
    fVal, Bool -> Bool
    not (Float -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN Float
    f)
      = Word32 -> SBV Word32
    forall a. SymVal a => a -> SBV a
    literal (Float -> Word32
    CN.floatToWord Float
    f)
      | Bool
    True
      = SVal -> SBV Word32
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    w32 (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 w32 :: Kind
    w32  = Bool -> Int -> Kind
    KBounded Bool
    False 32
            y :: State -> IO SV
    y st :: State
    st = do Bool
    cg <- State -> IO Bool
    isCodeGenMode State
    st
                      if Bool
    cg
                         then do SV
    f <- State -> SBV Float -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV Float
    fVal
                                 State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    w32 (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret Kind
    KFloat Kind
    w32)) [SV
    f])
                         else do SV
    n   <- State -> Kind -> IO SV
    internalVariable State
    st Kind
    w32
                                 SV
    ysw <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KFloat (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret Kind
    w32 Kind
    KFloat)) [SV
    n])
                                 State -> Bool -> [(String, String)] -> SVal -> IO ()
    internalConstraint State
    st Bool
    False [] (SVal -> IO ()) -> SVal -> IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SVal
    forall a. SBV a -> SVal
    unSBV (SBool -> SVal) -> SBool -> SVal
    forall a b. (a -> b) -> a -> b
    $ SBV Float
    fVal SBV Float -> SBV Float -> SBool
    forall a. IEEEFloating a => SBV a -> SBV a -> SBool
    `fpIsEqualObject` SVal -> SBV Float
    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 (\_ -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    ysw))))
                                 SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    n

    -- | 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 :: SBV Double -> SBV Word64
    sDoubleAsSWord64 fVal :: SBV Double
    fVal
      | Just f :: Double
    f <- SBV Double -> Maybe Double
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV Double
    fVal, Bool -> Bool
    not (Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN Double
    f)
      = Word64 -> SBV Word64
    forall a. SymVal a => a -> SBV a
    literal (Double -> Word64
    CN.doubleToWord Double
    f)
      | Bool
    True
      = SVal -> SBV Word64
    forall a. SVal -> SBV a
    SBV (Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    w64 (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 w64 :: Kind
    w64  = Bool -> Int -> Kind
    KBounded Bool
    False 64
            y :: State -> IO SV
    y st :: State
    st = do Bool
    cg <- State -> IO Bool
    isCodeGenMode State
    st
                      if Bool
    cg
                         then do SV
    f <- State -> SBV Double -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV Double
    fVal
                                 State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    w64 (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret Kind
    KDouble Kind
    w64)) [SV
    f])
                         else do SV
    n   <- State -> Kind -> IO SV
    internalVariable State
    st Kind
    w64
                                 SV
    ysw <- State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KDouble (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret Kind
    w64 Kind
    KDouble)) [SV
    n])
                                 State -> Bool -> [(String, String)] -> SVal -> IO ()
    internalConstraint State
    st Bool
    False [] (SVal -> IO ()) -> SVal -> IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SVal
    forall a. SBV a -> SVal
    unSBV (SBool -> SVal) -> SBool -> SVal
    forall a b. (a -> b) -> a -> b
    $ SBV Double
    fVal SBV Double -> SBV Double -> SBool
    forall a. IEEEFloating a => SBV a -> SBV a -> SBool
    `fpIsEqualObject` SVal -> SBV Double
    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 (\_ -> SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    ysw))))
                                 SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    n

    -- | 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 :: SBV Float -> (SBool, [SBool], [SBool])
    blastSFloat = SBV Word32 -> (SBool, [SBool], [SBool])
    forall a. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
    extract (SBV Word32 -> (SBool, [SBool], [SBool]))
    -> (SBV Float -> SBV Word32)
    -> SBV Float
    -> (SBool, [SBool], [SBool])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV Float -> SBV Word32
    sFloatAsSWord32
     where extract :: SBV a -> (SBool, [SBool], [SBool])
    extract x :: SBV a
    x = (SBV a -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SBV a
    x 31, SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [30, 29 .. 23], SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [22, 21 .. 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 :: SBV Double -> (SBool, [SBool], [SBool])
    blastSDouble = SBV Word64 -> (SBool, [SBool], [SBool])
    forall a. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
    extract (SBV Word64 -> (SBool, [SBool], [SBool]))
    -> (SBV Double -> SBV Word64)
    -> SBV Double
    -> (SBool, [SBool], [SBool])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV Double -> SBV Word64
    sDoubleAsSWord64
     where extract :: SBV a -> (SBool, [SBool], [SBool])
    extract x :: SBV a
    x = (SBV a -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SBV a
    x 63, SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [62, 61 .. 52], SBV a -> [Int] -> [SBool]
    forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
    sExtractBits SBV a
    x [51, 50 .. 0])

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

    -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
    sWord64AsSDouble :: SWord64 -> SDouble
    sWord64AsSDouble :: SBV Word64 -> SBV Double
    sWord64AsSDouble dVal :: SBV Word64
    dVal
      | Just d :: Word64
    d <- SBV Word64 -> Maybe Word64
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV Word64
    dVal = Double -> SBV Double
    forall a. SymVal a => a -> SBV a
    literal (Double -> SBV Double) -> Double -> SBV Double
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Double
    CN.wordToDouble Word64
    d
      | Bool
    True                     = SVal -> SBV Double
    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 st :: State
    st = do SV
    xsv <- State -> SBV Word64 -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV Word64
    dVal
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KDouble (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP (Kind -> Kind -> FPOp
    FP_Reinterpret (SBV Word64 -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV Word64
    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 :: SBV Float -> SBV Word32
    sFloatAsComparableSWord32 f :: SBV Float
    f = SBool -> SBV Word32 -> SBV Word32 -> SBV Word32
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Float -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegativeZero SBV Float
    f) (SBV Float -> SBV Word32
    sFloatAsComparableSWord32 0) ([SBool] -> SBV Word32
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV Word32) -> [SBool] -> SBV Word32
    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 (sb :: SBool
    sb : rest :: [SBool]
    rest) = SBV Word32 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE (SBV Word32 -> [SBool]) -> SBV Word32 -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ SBV Float -> SBV Word32
    sFloatAsSWord32 SBV Float
    f

    -- | 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 :: SBV Double -> SBV Word64
    sDoubleAsComparableSWord64 d :: SBV Double
    d = SBool -> SBV Word64 -> SBV Word64 -> SBV Word64
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Double -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNegativeZero SBV Double
    d) (SBV Double -> SBV Word64
    sDoubleAsComparableSWord64 0) ([SBool] -> SBV Word64
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool] -> SBV Word64) -> [SBool] -> SBV Word64
    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 (sb :: SBool
    sb : rest :: [SBool]
    rest) = SBV Word64 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE (SBV Word64 -> [SBool]) -> SBV Word64 -> [SBool]
    forall a b. (a -> b) -> a -> b
    $ SBV Double -> SBV Word64
    sDoubleAsSWord64 SBV Double
    d

    -- | '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 :: SBV Float -> SBV (MetricSpace Float)
    toMetricSpace          = SBV Float -> SBV Word32
    SBV Float -> SBV (MetricSpace Float)
    sFloatAsComparableSWord32
       fromMetricSpace :: SBV (MetricSpace Float) -> SBV Float
    fromMetricSpace        = SBV Word32 -> SBV Float
    SBV (MetricSpace Float) -> SBV Float
    sWord32AsSFloat

       msMinimize :: String -> SBV Float -> m ()
    msMinimize nm :: String
    nm o :: SBV Float
    o = do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> 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 Float -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV Float
    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
    $ SBV Word32 -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV Word32 -> SVal) -> Objective (SBV Word32) -> Objective SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` String -> SBV Word32 -> Objective (SBV Word32)
    forall a. String -> a -> Objective a
    Minimize String
    nm (SBV Float -> SBV (MetricSpace Float)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV Float
    o)

       msMaximize :: String -> SBV Float -> m ()
    msMaximize nm :: String
    nm o :: SBV Float
    o = do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> 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 Float -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV Float
    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
    $ SBV Word32 -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV Word32 -> SVal) -> Objective (SBV Word32) -> Objective SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` String -> SBV Word32 -> Objective (SBV Word32)
    forall a. String -> a -> Objective a
    Maximize String
    nm (SBV Float -> SBV (MetricSpace Float)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV Float
    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 :: SBV Double -> SBV (MetricSpace Double)
    toMetricSpace           = SBV Double -> SBV Word64
    SBV Double -> SBV (MetricSpace Double)
    sDoubleAsComparableSWord64
       fromMetricSpace :: SBV (MetricSpace Double) -> SBV Double
    fromMetricSpace         = SBV Word64 -> SBV Double
    SBV (MetricSpace Double) -> SBV Double
    sWord64AsSDouble

       msMinimize :: String -> SBV Double -> m ()
    msMinimize nm :: String
    nm o :: SBV Double
    o = do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> 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 Double -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV Double
    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
    $ SBV Word64 -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV Word64 -> SVal) -> Objective (SBV Word64) -> Objective SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` String -> SBV Word64 -> Objective (SBV Word64)
    forall a. String -> a -> Objective a
    Minimize String
    nm (SBV Double -> SBV (MetricSpace Double)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV Double
    o)

       msMaximize :: String -> SBV Double -> m ()
    msMaximize nm :: String
    nm o :: SBV Double
    o = do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> 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 Double -> SBool
    forall a. IEEEFloating a => SBV a -> SBool
    fpIsNaN SBV Double
    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
    $ SBV Word64 -> SVal
    forall a. SBV a -> SVal
    unSBV (SBV Word64 -> SVal) -> Objective (SBV Word64) -> Objective SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` String -> SBV Word64 -> Objective (SBV Word64)
    forall a. String -> a -> Objective a
    Maximize String
    nm (SBV Double -> SBV (MetricSpace Double)
    forall a. Metric a => SBV a -> SBV (MetricSpace a)
    toMetricSpace SBV Double
    o)

    {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}