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

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

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

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

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

import Data.Proxy

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

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

import Data.SBV.Utils.Numeric

import Data.Ratio

import GHC.TypeLits

import LibBF

import Data.SBV.Core.Operations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | SFloat instance
instance IEEEFloating Float

-- | SDouble instance
instance IEEEFloating Double

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

  -- | Convert to an IEEE-754 Single-precision float.
  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 -> SBV Float
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 -> SBV Double -> SBV a
forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat

  -- | Convert to an IEEE-754 Double-precision float.
  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 -> SBV Double
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 -> SFloatingPoint 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 -> SFloatingPoint 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 :: (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 :: SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SBV a
f = SVal -> SBV r
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kTo (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
  where kFrom :: Kind
kFrom = SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
f
        kTo :: Kind
kTo   = Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
        r :: State -> IO SV
r State
st  = do SV
msv <- State -> SRoundingMode -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                   SV
xsv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
f
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
kFrom Kind
kTo SV
msv)) [SV
xsv])

-- | A generic to-float converter, which will constant-fold as necessary, but only in the sRNE mode 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 :: (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 (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
        r :: State -> IO SV
r State
st  = do SV
msv <- State -> SRoundingMode -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                   SV
xsv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
i
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
kFrom Kind
kTo SV
msv)) [SV
xsv])

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

-- For float and double, skip the conversion if the same and do the constant folding, unlike all others.
instance IEEEFloatConvertible Float where
  toSFloat :: SRoundingMode -> SBV Float -> SBV Float
toSFloat  SRoundingMode
_ SBV Float
f = SBV Float
f
  toSDouble :: SRoundingMode -> SBV Float -> SBV Double
toSDouble     = (RoundingMode -> Float -> Maybe Double)
-> SRoundingMode -> SBV Float -> SBV Double
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 :: SRoundingMode -> SBV Float -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm SBV Float
f = SRoundingMode -> SBV Double -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm (SBV Double -> SFloatingPoint eb sb)
-> SBV Double -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ SRoundingMode -> SBV Float -> SBV Double
forall a.
IEEEFloatConvertible a =>
SRoundingMode -> SBV a -> SBV Double
toSDouble SRoundingMode
rm SBV Float
f

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

instance IEEEFloatConvertible Double where
  toSFloat :: SRoundingMode -> SBV Double -> SBV Float
toSFloat      = (RoundingMode -> Double -> Maybe Float)
-> SRoundingMode -> SBV Double -> SBV Float
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 -> SBV Double -> SBV Double
toSDouble SRoundingMode
_ SBV Double
d = SBV Double
d

  toSFloatingPoint :: SRoundingMode -> SBV Double -> SFloatingPoint eb sb
toSFloatingPoint SRoundingMode
rm SBV Double
sd
    | Just Double
d <- SBV Double -> Maybe Double
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV Double
sd, 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 (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
    = SFloatingPoint eb sb
res
    where (Kind
k, Int
ei, Int
si) = case SFloatingPoint eb sb -> Kind
forall a. HasKind a => a -> Kind
kindOf SFloatingPoint 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, SBV Double) -> [Char]
forall a. Show a => a -> [Char]
show (Kind
kr, SRoundingMode
rm, SBV Double
sd)
          res :: SFloatingPoint eb sb
res = SVal -> SFloatingPoint eb sb
forall a. SVal -> SBV a
SBV (SVal -> SFloatingPoint eb sb) -> SVal -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
          r :: State -> IO SV
r State
st = do SV
msv <- State -> SRoundingMode -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SRoundingMode
rm
                    SV
xsv <- State -> SBV Double -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV Double
sd
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> SV -> FPOp
FP_Cast Kind
KDouble Kind
k SV
msv)) [SV
xsv])

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

convertWhenExactRational :: Fractional a => AlgReal -> Maybe a
convertWhenExactRational :: 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 -> SBV Float
toSFloat         = (RoundingMode -> AlgReal -> Maybe Float)
-> SRoundingMode -> SBV AlgReal -> SBV Float
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 -> SBV Double
toSDouble        = (RoundingMode -> AlgReal -> Maybe Double)
-> SRoundingMode -> SBV AlgReal -> SBV Double
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 :: SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb
toSFloatingPoint = (RoundingMode -> AlgReal -> Maybe (FloatingPoint eb sb))
-> SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb
forall a r.
(IEEEFloatConvertible a, IEEEFloating r) =>
(RoundingMode -> a -> Maybe r) -> SRoundingMode -> SBV a -> SBV r
genericToFloat ((AlgReal -> Maybe (FloatingPoint eb sb))
-> RoundingMode -> AlgReal -> Maybe (FloatingPoint eb sb)
forall a b. a -> b -> a
const       AlgReal -> Maybe (FloatingPoint eb sb)
forall a. Fractional a => AlgReal -> Maybe a
convertWhenExactRational)

-- Arbitrary floats can handle all rounding modes in concrete mode
instance ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) where
  toSFloat :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV Float
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 -> SBV Float
forall a. SymVal a => a -> SBV a
literal (Float -> SBV Float) -> Float -> SBV Float
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) -> SBV Float
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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)

  fromSFloat :: SRoundingMode -> SBV Float -> SBV (FloatingPoint eb sb)
fromSFloat SRoundingMode
rm SBV Float
i
    | Just Float
f <- SBV Float -> Maybe Float
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV Float
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 -> SBV Float -> SBV (FloatingPoint eb sb)
forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SBV Float
i
    where ei :: Int
ei = Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)

  toSDouble :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV Double
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 -> SBV Double
forall a. SymVal a => a -> SBV a
literal (Double -> SBV Double) -> Double -> SBV Double
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) -> SBV Double
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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)

  fromSDouble :: SRoundingMode -> SBV Double -> SBV (FloatingPoint eb sb)
fromSDouble SRoundingMode
rm SBV Double
i
    | Just Double
f <- SBV Double -> Maybe Double
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV Double
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 -> SBV Double -> SBV (FloatingPoint eb sb)
forall a r.
(IEEEFloating a, IEEEFloatConvertible r) =>
SRoundingMode -> SBV a -> SBV r
genericFromFloat SRoundingMode
rm SBV Double
i
    where ei :: Int
ei = Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
          si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)

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

  -- From and To are the same when the source is an arbitrary float!
  fromSFloatingPoint :: SRoundingMode -> SFloatingPoint eb sb -> SBV (FloatingPoint eb sb)
fromSFloatingPoint = SRoundingMode -> SFloatingPoint eb sb -> SBV (FloatingPoint 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 :: Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)
concEval1 Maybe (a -> a)
mbOp Maybe SRoundingMode
mbRm SBV a
a = do a -> a
op <- Maybe (a -> a)
mbOp
                           a
v  <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a
                           case SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
unliteral (SRoundingMode -> Maybe RoundingMode)
-> Maybe SRoundingMode -> Maybe RoundingMode
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SRoundingMode
mbRm of
                                   Maybe RoundingMode
Nothing                     -> (SBV a -> Maybe (SBV a)
forall a. a -> Maybe a
Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) (a -> a
op a
v)
                                   Just RoundingMode
RoundNearestTiesToEven -> (SBV a -> Maybe (SBV a)
forall a. a -> Maybe a
Just (SBV a -> Maybe (SBV a)) -> (a -> SBV a) -> a -> Maybe (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) (a -> a
op a
v)
                                   Maybe RoundingMode
_                           -> Maybe (SBV a)
forall a. Maybe a
Nothing

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

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

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

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

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

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


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

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

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

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

-- | Convert an 'SFloat' to an 'SWord32', preserving the bit-correspondence. Note that since the
-- representation for @NaN@s are not unique, this function will return a symbolic value when given a
-- concrete @NaN@.
--
-- Implementation note: Since there's no corresponding function in SMTLib for conversion to
-- bit-representation due to partiality, we use a translation trick by allocating a new word variable,
-- converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map
-- it to a simple conversion.
sFloatAsSWord32 :: SFloat -> SWord32
sFloatAsSWord32 :: SBV Float -> SBV Word32
sFloatAsSWord32 (SBV SVal
v) = SVal -> SBV Word32
forall a. SVal -> SBV a
SBV (SVal -> SBV Word32) -> SVal -> SBV Word32
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 :: SBV Double -> SBV Word64
sDoubleAsSWord64 (SBV SVal
v) = SVal -> SBV Word64
forall a. SVal -> SBV a
SBV (SVal -> SBV Word64) -> SVal -> SBV Word64
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 :: SBV Float -> (SBool, [SBool], [SBool])
blastSFloat = SBV Word32 -> (SBool, [SBool], [SBool])
forall a. SFiniteBits a => SBV a -> (SBool, [SBool], [SBool])
extract (SBV Word32 -> (SBool, [SBool], [SBool]))
-> (SBV Float -> SBV Word32)
-> SBV Float
-> (SBool, [SBool], [SBool])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV Float -> SBV Word32
sFloatAsSWord32
 where extract :: SBV a -> (SBool, [SBool], [SBool])
extract SBV a
x = (SBV a -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SBV a
x Int
31, SBV a -> [Int] -> [SBool]
forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
30, Int
29 .. Int
23], SBV a -> [Int] -> [SBool]
forall a. SFiniteBits a => SBV a -> [Int] -> [SBool]
sExtractBits SBV a
x [Int
22, Int
21 .. Int
0])

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

-- | 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 :: 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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 :: SBV Word32 -> SBV Float
sWord32AsSFloat SBV Word32
fVal
  | Just Word32
f <- SBV Word32 -> Maybe Word32
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV Word32
fVal = Float -> SBV Float
forall a. SymVal a => a -> SBV a
literal (Float -> SBV Float) -> Float -> SBV Float
forall a b. (a -> b) -> a -> b
$ Word32 -> Float
wordToFloat Word32
f
  | Bool
True                     = SVal -> SBV Float
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KFloat (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y)))
  where y :: State -> IO SV
y State
st = do SV
xsv <- State -> SBV Word32 -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV Word32
fVal
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KFloat (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret (SBV Word32 -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV Word32
fVal) Kind
KFloat)) [SV
xsv])

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

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

-- | Inverse transformation to 'sFloatAsComparableSWord32'.
sComparableSWord32AsSFloat :: SWord32 -> SFloat
sComparableSWord32AsSFloat :: SBV Word32 -> SBV Float
sComparableSWord32AsSFloat SBV Word32
w = SBV Word32 -> SBV Float
sWord32AsSFloat (SBV Word32 -> SBV Float) -> SBV Word32 -> SBV Float
forall a b. (a -> b) -> a -> b
$ SBool -> SBV Word32 -> SBV Word32 -> SBV Word32
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb ([SBool] -> SBV Word32
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV Word32) -> [SBool] -> SBV Word32
forall a b. (a -> b) -> a -> b
$ SBool
sFalse SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool]
rest) ([SBool] -> SBV Word32
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV Word32) -> [SBool] -> SBV Word32
forall a b. (a -> b) -> a -> b
$ (SBool -> SBool) -> [SBool] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
allBits)
  where allBits :: [SBool]
allBits@(SBool
sb : [SBool]
rest) = SBV Word32 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV Word32
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 :: SBV Double -> SBV Word64
sDoubleAsComparableSWord64 SBV Double
d = SBool -> SBV Word64 -> SBV Word64 -> SBV Word64
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Double -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SBV Double
d) (SBV Double -> SBV Word64
sDoubleAsComparableSWord64 SBV Double
0) ([SBool] -> SBV Word64
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV Word64) -> [SBool] -> SBV Word64
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot SBool
sb SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: SBool -> [SBool] -> [SBool] -> [SBool]
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb ((SBool -> SBool) -> [SBool] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
rest) [SBool]
rest)
  where (SBool
sb : [SBool]
rest) = SBV Word64 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE (SBV Word64 -> [SBool]) -> SBV Word64 -> [SBool]
forall a b. (a -> b) -> a -> b
$ SBV Double -> SBV Word64
sDoubleAsSWord64 SBV Double
d

-- | 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 :: SBV Word64 -> SBV Double
sComparableSWord64AsSDouble SBV Word64
w = SBV Word64 -> SBV Double
sWord64AsSDouble (SBV Word64 -> SBV Double) -> SBV Word64 -> SBV Double
forall a b. (a -> b) -> a -> b
$ SBool -> SBV Word64 -> SBV Word64 -> SBV Word64
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
sb ([SBool] -> SBV Word64
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV Word64) -> [SBool] -> SBV Word64
forall a b. (a -> b) -> a -> b
$ SBool
sFalse SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool]
rest) ([SBool] -> SBV Word64
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV Word64) -> [SBool] -> SBV Word64
forall a b. (a -> b) -> a -> b
$ (SBool -> SBool) -> [SBool] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SBool
sNot [SBool]
allBits)
  where allBits :: [SBool]
allBits@(SBool
sb : [SBool]
rest) = SBV Word64 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV Word64
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 :: SBV Float -> SBV (MetricSpace Float)
toMetricSpace          = SBV Float -> SBV Word32
SBV Float -> SBV (MetricSpace Float)
sFloatAsComparableSWord32
   fromMetricSpace :: SBV (MetricSpace Float) -> SBV Float
fromMetricSpace        = SBV Word32 -> SBV Float
SBV (MetricSpace Float) -> SBV Float
sComparableSWord32AsSFloat

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

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

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

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

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

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

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

-- | RealFrac instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here.
instance ValidFloat eb sb => RealFrac (FloatingPoint eb sb) where
  properFraction :: 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 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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
           si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 :: SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsSWord (SBV SVal
v) = SVal -> SWord (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 :: SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord SFloatingPoint eb sb
f = SBool -> SWord (eb + sb) -> SWord (eb + sb) -> SWord (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) SWord (eb + sb)
posZero ([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
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 :: SWord (eb + sb)
posZero     = SFloatingPoint eb sb -> SWord (eb + sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
sFloatingPointAsComparableSWord (SFloatingPoint eb sb
0 :: SFloatingPoint eb sb)
        (SBool
sb : [SBool]
rest) = SWord (eb + sb) -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE (SFloatingPoint eb sb -> SWord (eb + sb)
forall (eb :: Nat) (sb :: Nat).
(ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) =>
SFloatingPoint eb sb -> SWord (eb + sb)
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 :: 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 :: SWord (eb + sb) -> SFloatingPoint eb sb
sWordAsSFloatingPoint SWord (eb + sb)
sw
   | Just (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 (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 -> 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 FP
fp
   | Bool
True
   = SVal -> SFloatingPoint 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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
         si :: Int
si   = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)
         kTo :: Kind
kTo  = Int -> Int -> Kind
KFP Int
ei Int
si
         y :: State -> IO SV
y State
st = do SV
xsv <- State -> SWord (eb + sb) -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SWord (eb + sb)
sw
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kTo (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP (Kind -> Kind -> FPOp
FP_Reinterpret (SWord (eb + sb) -> Kind
forall a. HasKind a => a -> Kind
kindOf SWord (eb + sb)
sw) Kind
kTo)) [SV
xsv])

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

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

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

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

-- | Lift a 1 arg Big-float op
lift1FP :: forall eb sb. ValidFloat eb sb =>
           (BFOpts -> BigFloat -> (BigFloat, Status))
        -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb)
        -> SRoundingMode
        -> SFloatingPoint eb sb
        -> SFloatingPoint eb sb
lift1FP :: (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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 :: (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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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 :: (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 (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)
        si :: Int
si = Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
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

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