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

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

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

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

import Control.Monad (when)

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

import Data.Proxy

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

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

import Data.SBV.Utils.Numeric

import Data.Ratio

import GHC.TypeLits

import LibBF

import Data.SBV.Core.Operations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | SFloat instance
instance IEEEFloating Float

-- | SDouble instance
instance IEEEFloating Double

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SFloat -> m ()
msMinimize [Char]
nm SFloat
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SFloat
o
                        let nm' :: [Char]
nm' = Proxy Float -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Float) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SFloat -> SVal
forall a. SBV a -> SVal
unSBV SFloat
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord32 -> SVal
forall a. SBV a -> SVal
unSBV (SWord32 -> SVal) -> Objective SWord32 -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord32 -> Objective SWord32
forall a. [Char] -> a -> Objective a
Minimize [Char]
nm' (SFloat -> SBV (MetricSpace Float)
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SFloat
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SFloat -> m ()
msMaximize [Char]
nm SFloat
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SFloat
o
                        let nm' :: [Char]
nm' = Proxy Float -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Float) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SFloat -> SVal
forall a. SBV a -> SVal
unSBV SFloat
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord32 -> SVal
forall a. SBV a -> SVal
unSBV (SWord32 -> SVal) -> Objective SWord32 -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord32 -> Objective SWord32
forall a. [Char] -> a -> Objective a
Maximize [Char]
nm' (SFloat -> SBV (MetricSpace Float)
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SFloat
o)

   annotateForMS :: Proxy Float -> [Char] -> [Char]
annotateForMS Proxy Float
_ [Char]
s = [Char]
"toMetricSpace(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

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

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

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SDouble -> m ()
msMinimize [Char]
nm SDouble
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SDouble -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SDouble
o
                        let nm' :: [Char]
nm' = Proxy Double -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Double) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SDouble -> SVal
forall a. SBV a -> SVal
unSBV SDouble
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord64 -> SVal
forall a. SBV a -> SVal
unSBV (SWord64 -> SVal) -> Objective SWord64 -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord64 -> Objective SWord64
forall a. [Char] -> a -> Objective a
Minimize [Char]
nm' (SDouble -> SBV (MetricSpace Double)
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SDouble
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SDouble -> m ()
msMaximize [Char]
nm SDouble
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SDouble -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SDouble
o
                        let nm' :: [Char]
nm' = Proxy Double -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Double) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SDouble -> SVal
forall a. SBV a -> SVal
unSBV SDouble
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord64 -> SVal
forall a. SBV a -> SVal
unSBV (SWord64 -> SVal) -> Objective SWord64 -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord64 -> Objective SWord64
forall a. [Char] -> a -> Objective a
Maximize [Char]
nm' (SDouble -> SBV (MetricSpace Double)
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SDouble
o)

   annotateForMS :: Proxy Double -> [Char] -> [Char]
annotateForMS Proxy Double
_ [Char]
s = [Char]
"toMetricSpace(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

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

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

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

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

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

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

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

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

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

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

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

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

   msMinimize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SBV (FloatingPoint eb sb) -> m ()
msMinimize [Char]
nm SBV (FloatingPoint eb sb)
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SBV (FloatingPoint eb sb)
o
                        let nm' :: [Char]
nm' = Proxy (FloatingPoint eb sb) -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(FloatingPoint eb sb)) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SBV (FloatingPoint eb sb) -> SVal
forall a. SBV a -> SVal
unSBV SBV (FloatingPoint eb sb)
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord (eb + sb) -> SVal
forall a. SBV a -> SVal
unSBV (SWord (eb + sb) -> SVal)
-> Objective (SWord (eb + sb)) -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord (eb + sb) -> Objective (SWord (eb + sb))
forall a. [Char] -> a -> Objective a
Minimize [Char]
nm' (SBV (FloatingPoint eb sb)
-> SBV (MetricSpace (FloatingPoint eb sb))
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SBV (FloatingPoint eb sb)
o)

   msMaximize :: forall (m :: * -> *).
(MonadSymbolic m, SolverContext m) =>
[Char] -> SBV (FloatingPoint eb sb) -> m ()
msMaximize [Char]
nm SBV (FloatingPoint eb sb)
o = do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SBV (FloatingPoint eb sb)
o
                        let nm' :: [Char]
nm' = Proxy (FloatingPoint eb sb) -> [Char] -> [Char]
forall a. Metric a => Proxy a -> [Char] -> [Char]
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(FloatingPoint eb sb)) [Char]
nm
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
nm' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
nm) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => [Char] -> SVal -> m ()
sObserve [Char]
nm (SBV (FloatingPoint eb sb) -> SVal
forall a. SBV a -> SVal
unSBV SBV (FloatingPoint eb sb)
o)
                        Objective SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal (Objective SVal -> m ()) -> Objective SVal -> m ()
forall a b. (a -> b) -> a -> b
$ SWord (eb + sb) -> SVal
forall a. SBV a -> SVal
unSBV (SWord (eb + sb) -> SVal)
-> Objective (SWord (eb + sb)) -> Objective SVal
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> SWord (eb + sb) -> Objective (SWord (eb + sb))
forall a. [Char] -> a -> Objective a
Maximize [Char]
nm' (SBV (FloatingPoint eb sb)
-> SBV (MetricSpace (FloatingPoint eb sb))
forall a. Metric a => SBV a -> SBV (MetricSpace a)
toMetricSpace SBV (FloatingPoint eb sb)
o)

   annotateForMS :: Proxy (FloatingPoint eb sb) -> [Char] -> [Char]
annotateForMS Proxy (FloatingPoint eb sb)
_ [Char]
s = [Char]
"toMetricSpace(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

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

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

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

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

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

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

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

{- HLint ignore module "Reduce duplication" -}