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

-- | 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 = RoundTowardNegative :: RoundingMode
  --   s1 =           -44297675 :: Int32
  --
  -- Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
  --
  -- >>> toRational (-44297675 :: Float)
  -- (-44297676) % 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 = RoundNearestTiesToAway :: RoundingMode
  --   s1 =   -3871901667041025751 :: 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 (-3871901667041025751 :: Double)
  -- (-3871901667041025536) % 1
  --
  -- In this case the numerator is off by 15.
  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 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 (Proxy r
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.
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 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
RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm, Just 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 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  SRoundingMode
_ 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  SRoundingMode
_  SBV Float
f = SBV Float
f
  fromSDouble :: SRoundingMode -> SBV Double -> SBV Float
fromSDouble SRoundingMode
rm SBV Double
f
    | Just RoundingMode
RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm
    , Just 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 SRoundingMode
_ SBV Double
d = SBV Double
d

  fromSDouble :: SRoundingMode -> SBV Double -> SBV Double
fromSDouble SRoundingMode
_  SBV Double
d = SBV Double
d
  fromSFloat :: SRoundingMode -> SBV Float -> SBV Double
fromSFloat  SRoundingMode
rm SBV Float
d
    | Just RoundingMode
RoundNearestTiesToEven <- SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
unliteral SRoundingMode
rm
    , Just 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 (\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 (\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 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 :: 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 :: 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 :: 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 (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 (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 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: SBV Float -> SBV Word32
sFloatAsSWord32 SBV Float
fVal
  | Just 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 Int
32
        y :: State -> IO SV
y 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 (\State
_ -> 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 SBV Double
fVal
  | Just 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 Int
64
        y :: State -> IO SV
y 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 (\State
_ -> 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 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 :: 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 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])

-- | Reinterpret the bits in a 32-bit word as a single-precision floating point number
sWord32AsSFloat :: SWord32 -> SFloat
sWord32AsSFloat :: SBV Word32 -> SBV Float
sWord32AsSFloat SBV Word32
fVal
  | Just 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 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 SBV Word64
dVal
  | Just 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 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 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 SBV Float
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 (SBool
sb : [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 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 SBV Double
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 (SBool
sb : [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 String
nm 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 String
nm 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 String
nm 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 String
nm 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) #-}