{-# LANGUAGE FlexibleContexts #-}

-- |
-- 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
  ( pevalFPTraitTerm,
    sbvFPTraitTerm,
    pevalFPUnaryTerm,
    sbvFPUnaryTerm,
    pevalFPBinaryTerm,
    sbvFPBinaryTerm,
    pevalFPRoundingUnaryTerm,
    sbvFPRoundingUnaryTerm,
    pevalFPRoundingBinaryTerm,
    sbvFPRoundingBinaryTerm,
    pevalFPFMATerm,
    sbvFPFMATerm,
  )
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, FPRoundingMode, ValidFP)
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),
    SupportedPrim,
    Term (ConTerm),
    conTerm,
    fpBinaryTerm,
    fpFMATerm,
    fpRoundingBinaryTerm,
    fpRoundingUnaryTerm,
    fpTraitTerm,
    fpUnaryTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

-- | Partially evaluate a floating-point trait term.
pevalFPTraitTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPTrait ->
  Term (FP eb sb) ->
  Term Bool
pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
fpTraitTerm FPTrait
trait)
  where
    doPevalFPTraitTerm :: Term t -> Maybe (Term Bool)
doPevalFPTraitTerm (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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

-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects
-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.
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 #-}

-- | Lowering an floating-point trait term to sbv.
sbvFPTraitTerm ::
  (ValidFP eb sb) =>
  FPTrait ->
  SBV.SFloatingPoint eb sb ->
  SBV.SBool
sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPTrait -> SFloatingPoint eb sb -> SBool
sbvFPTraitTerm FPTrait
FPIsNaN = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN
sbvFPTraitTerm FPTrait
FPIsPositive = SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsPositive
sbvFPTraitTerm FPTrait
FPIsNegative = SBV (FloatingPoint eb sb) -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SBool
goodFpIsNegative
sbvFPTraitTerm FPTrait
FPIsInfinite = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite
sbvFPTraitTerm FPTrait
FPIsPositiveInfinite = \SBV (FloatingPoint eb sb)
f ->
  SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint 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)
f
sbvFPTraitTerm FPTrait
FPIsNegativeInfinite = \SBV (FloatingPoint eb sb)
f ->
  SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint 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)
f
sbvFPTraitTerm FPTrait
FPIsPositiveZero =
  \SBV (FloatingPoint eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint 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)
f
sbvFPTraitTerm FPTrait
FPIsNegativeZero =
  \SBV (FloatingPoint eb sb)
f -> SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero SBV (FloatingPoint 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)
f
sbvFPTraitTerm FPTrait
FPIsZero = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsZero
sbvFPTraitTerm FPTrait
FPIsNormal = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNormal
sbvFPTraitTerm FPTrait
FPIsSubnormal = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsSubnormal
sbvFPTraitTerm FPTrait
FPIsPoint = SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsPoint

-- | Partially evaluate a floating-point unary term.
pevalFPUnaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPUnaryOp ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
fpUnaryTerm
{-# INLINE pevalFPUnaryTerm #-}

-- | Lowering an floating-point unary term to sbv.
sbvFPUnaryTerm ::
  (ValidFP eb sb) =>
  FPUnaryOp ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPUnaryTerm FPUnaryOp
FPAbs = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpAbs
sbvFPUnaryTerm FPUnaryOp
FPNeg = SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. IEEEFloating a => SBV a -> SBV a
SBV.fpNeg
{-# INLINE sbvFPUnaryTerm #-}

-- | Partially evaluate a floating-point binary term.
pevalFPBinaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPBinaryOp ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
bop (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FP eb sb
l) (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
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 #-}

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)

-- | Lowering an floating-point binary term to sbv.
sbvFPBinaryTerm ::
  (ValidFP eb sb) =>
  FPBinaryOp ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPBinaryOp
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPBinaryTerm FPBinaryOp
FPRem SFloatingPoint eb sb
x SFloatingPoint eb sb
y = SFloatingPoint eb sb
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a. IEEEFloating a => SBV a -> SBV a -> SBV a
SBV.fpRem SFloatingPoint eb sb
x SFloatingPoint eb sb
y
sbvFPBinaryTerm FPBinaryOp
FPMinimum SFloatingPoint eb sb
x SFloatingPoint eb sb
y =
  SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (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.fpIsNaN SFloatingPoint eb sb
y) SFloatingPoint eb sb
forall a. Floating a => a
SBV.nan (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
    SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SFloatingPoint eb sb
x SFloatingPoint eb sb
y) SFloatingPoint eb sb
x SFloatingPoint eb sb
y
sbvFPBinaryTerm FPBinaryOp
FPMinimumNumber SFloatingPoint eb sb
x SFloatingPoint eb sb
y =
  SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SFloatingPoint eb sb
y (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
    SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
y) SFloatingPoint eb sb
x (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
      SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SFloatingPoint eb sb
x SFloatingPoint eb sb
y) SFloatingPoint eb sb
x SFloatingPoint eb sb
y
sbvFPBinaryTerm FPBinaryOp
FPMaximum SFloatingPoint eb sb
x SFloatingPoint eb sb
y =
  SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (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.fpIsNaN SFloatingPoint eb sb
y) SFloatingPoint eb sb
forall a. Floating a => a
SBV.nan (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
    SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SFloatingPoint eb sb
x SFloatingPoint eb sb
y) SFloatingPoint eb sb
y SFloatingPoint eb sb
x
sbvFPBinaryTerm FPBinaryOp
FPMaximumNumber SFloatingPoint eb sb
x SFloatingPoint eb sb
y =
  SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
x) SFloatingPoint eb sb
y (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
    SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SFloatingPoint eb sb
y) SFloatingPoint eb sb
x (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$
      SBool
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool
sbvCmpHandleNegZero SFloatingPoint eb sb
x SFloatingPoint eb sb
y) SFloatingPoint eb sb
y SFloatingPoint eb sb
x
{-# INLINE sbvFPBinaryTerm #-}

-- | Partially evaluate a floating-point rounding unary term.
pevalFPRoundingUnaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPRoundingUnaryOp ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
uop (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingMode
rd) (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
fpRoundingUnaryTerm FPRoundingUnaryOp
uop Term FPRoundingMode
rd Term (FP eb sb)
l
{-# INLINE pevalFPRoundingUnaryTerm #-}

-- | Lowering an floating-point rounding unary term to sbv.
sbvFPRoundingUnaryTerm ::
  (ValidFP eb sb) =>
  FPRoundingUnaryOp ->
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingUnaryOp
-> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPRoundingUnaryTerm FPRoundingUnaryOp
FPSqrt = SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint 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)
forall a. IEEEFloating a => SRoundingMode -> SBV a -> SBV a
SBV.fpRoundToIntegral
{-# INLINE sbvFPRoundingUnaryTerm #-}

-- | Partially evaluate a floating-point rounding binary term.
pevalFPRoundingBinaryTerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  FPRoundingBinaryOp ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
bop (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingMode
rd) (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FP eb sb
l) (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
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 #-}

-- | Lowering an floating-point rounding binary term to sbv.
sbvFPRoundingBinaryTerm ::
  (ValidFP eb sb) =>
  FPRoundingBinaryOp ->
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
FPRoundingBinaryOp
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
FPAdd = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint 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)
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)
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)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
SBV.fpDiv
{-# INLINE sbvFPRoundingBinaryTerm #-}

-- | Partially evaluate a floating-point fused multiply-add term.
pevalFPFMATerm ::
  (ValidFP eb sb, SupportedPrim (FP eb sb)) =>
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb) ->
  Term (FP eb sb)
pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm
  (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FPRoundingMode
rd)
  (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FP eb sb
x)
  (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ FP eb sb
y)
  (ConTerm WeakThreadId
_ Digest
_ Digest
_ Ident
_ 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).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
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 #-}

-- | Lowering an floating-point fused multiply-add term to sbv.
sbvFPFMATerm ::
  (ValidFP eb sb) =>
  SBV.SRoundingMode ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb ->
  SBV.SFloatingPoint eb sb
sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPFMATerm = SRoundingMode
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
SBV.fpFMA
{-# INLINE sbvFPFMATerm #-}