{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternSynonyms #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP () where

import qualified Data.SBV as SBV
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPOp
      ( fpMaximum,
        fpMaximumNumber,
        fpMinimum,
        fpMinimumNumber,
        fpRem
      ),
    IEEEFPRoundingOp
      ( fpAdd,
        fpDiv,
        fpFMA,
        fpMul,
        fpRoundToIntegral,
        fpSqrt,
        fpSub
      ),
  )
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( FPBinaryOp (FPMaximum, FPMaximumNumber, FPMinimum, FPMinimumNumber, FPRem),
    FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),
    FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),
    FPTrait
      ( FPIsInfinite,
        FPIsNaN,
        FPIsNegative,
        FPIsNegativeInfinite,
        FPIsNegativeZero,
        FPIsNormal,
        FPIsPoint,
        FPIsPositive,
        FPIsPositiveInfinite,
        FPIsPositiveZero,
        FPIsSubnormal,
        FPIsZero
      ),
    FPUnaryOp (FPAbs, FPNeg),
    PEvalFPTerm
      ( pevalFPBinaryTerm,
        pevalFPFMATerm,
        pevalFPRoundingBinaryTerm,
        pevalFPRoundingUnaryTerm,
        pevalFPTraitTerm,
        pevalFPUnaryTerm,
        sbvFPBinaryTerm,
        sbvFPFMATerm,
        sbvFPRoundingBinaryTerm,
        sbvFPRoundingUnaryTerm,
        sbvFPTraitTerm,
        sbvFPUnaryTerm
      ),
    conTerm,
    fpBinaryTerm,
    fpFMATerm,
    fpRoundingBinaryTerm,
    fpRoundingUnaryTerm,
    fpTraitTerm,
    fpUnaryTerm,
    pattern ConTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

instance PEvalFPTerm FP where
  pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
trait =
    PartialRuleUnary (FP eb sb) Bool
-> TotalRuleUnary (FP eb sb) Bool -> TotalRuleUnary (FP eb sb) Bool
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (FP eb sb) Bool
forall {t}. RealFloat t => Term t -> Maybe (Term Bool)
doPevalFPTraitTerm (FPTrait -> TotalRuleUnary (FP eb sb) Bool
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
FPTrait -> Term (fp eb sb) -> Term Bool
fpTraitTerm FPTrait
trait)
    where
      doPevalFPTraitTerm :: Term t -> Maybe (Term Bool)
doPevalFPTraitTerm (ConTerm t
a) = case FPTrait
trait of
        FPTrait
FPIsNaN -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a
        FPTrait
FPIsPositive ->
          Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
            Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$
              Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a) Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
>= t
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
        FPTrait
FPIsNegative ->
          Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a) Bool -> Bool -> Bool
&& (t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
0 Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
        FPTrait
FPIsInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a
        FPTrait
FPIsPositiveInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0
        FPTrait
FPIsNegativeInfinite -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
&& t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
0
        FPTrait
FPIsPositiveZero ->
          Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a)
        FPTrait
FPIsNegativeZero -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero t
a
        FPTrait
FPIsZero -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
        FPTrait
FPIsNormal ->
          Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
            Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$
              Bool -> Bool
not (t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isDenormalized t
a)
        FPTrait
FPIsSubnormal -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ t -> Bool
forall a. RealFloat a => a -> Bool
isDenormalized t
a
        FPTrait
FPIsPoint -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (t -> Bool
forall a. RealFloat a => a -> Bool
isNaN t
a Bool -> Bool -> Bool
|| t -> Bool
forall a. RealFloat a => a -> Bool
isInfinite t
a)
      doPevalFPTraitTerm Term t
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing
  pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm = FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb)
fpUnaryTerm
  {-# INLINE pevalFPUnaryTerm #-}
  pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
bop (ConTerm FP eb sb
l) (ConTerm FP eb sb
r) =
    case FPBinaryOp
bop of
      FPBinaryOp
FPMaximum -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> FP eb sb -> FP eb sb
forall a. IEEEFPOp a => a -> a -> a
fpMaximum FP eb sb
l FP eb sb
r
      FPBinaryOp
FPMaximumNumber -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> FP eb sb -> FP eb sb
forall a. IEEEFPOp a => a -> a -> a
fpMaximumNumber FP eb sb
l FP eb sb
r
      FPBinaryOp
FPMinimum -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> FP eb sb -> FP eb sb
forall a. IEEEFPOp a => a -> a -> a
fpMinimum FP eb sb
l FP eb sb
r
      FPBinaryOp
FPMinimumNumber -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> FP eb sb -> FP eb sb
forall a. IEEEFPOp a => a -> a -> a
fpMinimumNumber FP eb sb
l FP eb sb
r
      FPBinaryOp
FPRem -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FP eb sb -> FP eb sb -> FP eb sb
forall a. IEEEFPOp a => a -> a -> a
fpRem FP eb sb
l FP eb sb
r
  pevalFPBinaryTerm FPBinaryOp
FPMaximum Term (FP eb sb)
l Term (FP eb sb)
r | Term (FP eb sb)
l Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
r = Term (FP eb sb)
l
  pevalFPBinaryTerm FPBinaryOp
FPMaximumNumber Term (FP eb sb)
l Term (FP eb sb)
r | Term (FP eb sb)
l Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
r = Term (FP eb sb)
l
  pevalFPBinaryTerm FPBinaryOp
FPMinimum Term (FP eb sb)
l Term (FP eb sb)
r | Term (FP eb sb)
l Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
r = Term (FP eb sb)
l
  pevalFPBinaryTerm FPBinaryOp
FPMinimumNumber Term (FP eb sb)
l Term (FP eb sb)
r | Term (FP eb sb)
l Term (FP eb sb) -> Term (FP eb sb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (FP eb sb)
r = Term (FP eb sb)
l
  pevalFPBinaryTerm FPBinaryOp
bop Term (FP eb sb)
l Term (FP eb sb)
r = FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
fpBinaryTerm FPBinaryOp
bop Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE pevalFPBinaryTerm #-}
  pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
uop (ConTerm FPRoundingMode
rd) (ConTerm FP eb sb
l) =
    case FPRoundingUnaryOp
uop of
      FPRoundingUnaryOp
FPSqrt -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a
fpSqrt FPRoundingMode
rd FP eb sb
l
      FPRoundingUnaryOp
FPRoundToIntegral -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a
fpRoundToIntegral FPRoundingMode
rd FP eb sb
l
  pevalFPRoundingUnaryTerm FPRoundingUnaryOp
uop Term FPRoundingMode
rd Term (FP eb sb)
l = FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb)
fpRoundingUnaryTerm FPRoundingUnaryOp
uop Term FPRoundingMode
rd Term (FP eb sb)
l
  {-# INLINE pevalFPRoundingUnaryTerm #-}
  pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
bop (ConTerm FPRoundingMode
rd) (ConTerm FP eb sb
l) (ConTerm FP eb sb
r) =
    case FPRoundingBinaryOp
bop of
      FPRoundingBinaryOp
FPAdd -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a -> a
fpAdd FPRoundingMode
rd FP eb sb
l FP eb sb
r
      FPRoundingBinaryOp
FPSub -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a -> a
fpSub FPRoundingMode
rd FP eb sb
l FP eb sb
r
      FPRoundingBinaryOp
FPMul -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a -> a
fpMul FPRoundingMode
rd FP eb sb
l FP eb sb
r
      FPRoundingBinaryOp
FPDiv -> FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a -> a
fpDiv FPRoundingMode
rd FP eb sb
l FP eb sb
r
  pevalFPRoundingBinaryTerm FPRoundingBinaryOp
bop Term FPRoundingMode
rd Term (FP eb sb)
l Term (FP eb sb)
r = FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
fpRoundingBinaryTerm FPRoundingBinaryOp
bop Term FPRoundingMode
rd Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE pevalFPRoundingBinaryTerm #-}
  pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm (ConTerm FPRoundingMode
rd) (ConTerm FP eb sb
x) (ConTerm FP eb sb
y) (ConTerm FP eb sb
z) =
    FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb
forall a mode. IEEEFPRoundingOp a mode => mode -> a -> a -> a -> a
fpFMA FPRoundingMode
rd FP eb sb
x FP eb sb
y FP eb sb
z
  pevalFPFMATerm Term FPRoundingMode
rd Term (FP eb sb)
x Term (FP eb sb)
y Term (FP eb sb)
z = Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> *).
(ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) =>
Term FPRoundingMode
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
-> Term (fp eb sb)
fpFMATerm Term FPRoundingMode
rd Term (FP eb sb)
x Term (FP eb sb)
y Term (FP eb sb)
z
  {-# INLINE pevalFPFMATerm #-}

  sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPTrait -> SBVType (FP eb sb) -> SBVType Bool
sbvFPTraitTerm FPTrait
FPIsNaN = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN
  sbvFPTraitTerm FPTrait
FPIsPositive = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive
  sbvFPTraitTerm FPTrait
FPIsNegative = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative
  sbvFPTraitTerm FPTrait
FPIsInfinite = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite
  sbvFPTraitTerm FPTrait
FPIsPositiveInfinite = \SBVType (FP eb sb)
f ->
    SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f
  sbvFPTraitTerm FPTrait
FPIsNegativeInfinite = \SBVType (FP eb sb)
f ->
    SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f
  sbvFPTraitTerm FPTrait
FPIsPositiveZero =
    \SBVType (FP eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f
  sbvFPTraitTerm FPTrait
FPIsNegativeZero =
    \SBVType (FP eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f SBool -> SBool -> SBool
SBV..&& SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
f
  sbvFPTraitTerm FPTrait
FPIsZero = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero
  sbvFPTraitTerm FPTrait
FPIsNormal = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNormal
  sbvFPTraitTerm FPTrait
FPIsSubnormal = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsSubnormal
  sbvFPTraitTerm FPTrait
FPIsPoint = SBV (FloatingPoint eb sb) -> SBool
SBVType (FP eb sb) -> SBVType Bool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsPoint

  sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb)
sbvFPUnaryTerm FPUnaryOp
FPAbs = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpAbs
  sbvFPUnaryTerm FPUnaryOp
FPNeg = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpNeg
  {-# INLINE sbvFPUnaryTerm #-}

  sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPBinaryOp
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
sbvFPBinaryTerm FPBinaryOp
FPRem SBVType (FP eb sb)
x SBVType (FP eb sb)
y = SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a -> SBV a
SBV.fpRem SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y
  sbvFPBinaryTerm FPBinaryOp
FPMinimum SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
forall a. Floating a => a
SBV.nan (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SBool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y
  sbvFPBinaryTerm FPBinaryOp
FPMinimumNumber SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x) SBVType (FP eb sb)
y (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBVType (FP eb sb)
x (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
        SBool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y
  sbvFPBinaryTerm FPBinaryOp
FPMaximum SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
forall a. Floating a => a
SBV.nan (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SBool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x
  sbvFPBinaryTerm FPBinaryOp
FPMaximumNumber SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x) SBVType (FP eb sb)
y (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
      SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBVType (FP eb sb)
x (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
        SBool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y) SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x
  {-# INLINE sbvFPBinaryTerm #-}

  sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingUnaryOp
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
sbvFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt = SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. IEEEFloating a => SRoundingMode -> SBV a -> SBV a
SBV.fpSqrt
  sbvFPRoundingUnaryTerm FPRoundingUnaryOp
FPRoundToIntegral = SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. IEEEFloating a => SRoundingMode -> SBV a -> SBV a
SBV.fpRoundToIntegral
  {-# INLINE sbvFPRoundingUnaryTerm #-}

  sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingBinaryOp
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPAdd = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpAdd
  sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPSub = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpSub
  sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPMul = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpMul
  sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPDiv = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpDiv
  {-# INLINE sbvFPRoundingBinaryTerm #-}

  sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
sbvFPFMATerm = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
SBV.fpFMA
  {-# INLINE sbvFPFMATerm #-}

goodFpIsPositive :: (ValidFP eb sb) => SBV.SFloatingPoint eb sb -> SBV.SBool
goodFpIsPositive :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive SFloatingPoint eb sb
x = SBool -> SBool
SBV.sNot (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SBool -> SBool -> SBool
SBV..&& SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsPositive SFloatingPoint eb sb
x
{-# INLINE goodFpIsPositive #-}

goodFpIsNegative :: (ValidFP eb sb) => SBV.SFloatingPoint eb sb -> SBV.SBool
goodFpIsNegative :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative SFloatingPoint eb sb
x = SBool -> SBool
SBV.sNot (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SBool -> SBool -> SBool
SBV..&& SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNegative SFloatingPoint eb sb
x
{-# INLINE goodFpIsNegative #-}

sbvCmpHandleNegZero ::
  (ValidFP eb sb) =>
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SBool
sbvCmpHandleNegZero :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SFloatingPoint eb sb
x SFloatingPoint eb sb
y =
  SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
    (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SFloatingPoint eb sb
x SBool -> SBool -> SBool
SBV..&& SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SFloatingPoint eb sb
y)
    (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNegativeZero SFloatingPoint eb sb
x)
    (SFloatingPoint eb sb
x SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..< SFloatingPoint eb sb
y)
{-# INLINE sbvCmpHandleNegZero #-}