| Copyright | (c) Sirui Lu 2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
Description
Synopsis
- pevalFPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPTrait -> Term (FP eb sb) -> Term Bool
- sbvFPTraitTerm :: ValidFP eb sb => FPTrait -> SFloatingPoint eb sb -> SBool
- pevalFPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
- sbvFPUnaryTerm :: ValidFP eb sb => FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb
- pevalFPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
- sbvFPBinaryTerm :: ValidFP eb sb => FPBinaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb
- pevalFPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
- sbvFPRoundingUnaryTerm :: ValidFP eb sb => FPRoundingUnaryOp -> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
- pevalFPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
- sbvFPRoundingBinaryTerm :: ValidFP eb sb => FPRoundingBinaryOp -> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb
- 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)
- sbvFPFMATerm :: ValidFP eb sb => SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb
Documentation
pevalFPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPTrait -> Term (FP eb sb) -> Term Bool Source #
Partially evaluate a floating-point trait term.
sbvFPTraitTerm :: ValidFP eb sb => FPTrait -> SFloatingPoint eb sb -> SBool Source #
Lowering an floating-point trait term to sbv.
pevalFPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source #
Partially evaluate a floating-point unary term.
sbvFPUnaryTerm :: ValidFP eb sb => FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source #
Lowering an floating-point unary term to sbv.
pevalFPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #
Partially evaluate a floating-point binary term.
sbvFPBinaryTerm :: ValidFP eb sb => FPBinaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source #
Lowering an floating-point binary term to sbv.
pevalFPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) Source #
Partially evaluate a floating-point rounding unary term.
sbvFPRoundingUnaryTerm :: ValidFP eb sb => FPRoundingUnaryOp -> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source #
Lowering an floating-point rounding unary term to sbv.
pevalFPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #
Partially evaluate a floating-point rounding binary term.
sbvFPRoundingBinaryTerm :: ValidFP eb sb => FPRoundingBinaryOp -> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source #
Lowering an floating-point rounding binary term to sbv.
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) Source #
Partially evaluate a floating-point fused multiply-add term.
sbvFPFMATerm :: ValidFP eb sb => SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source #
Lowering an floating-point fused multiply-add term to sbv.