{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Misc.Floating where
import Data.SBV
assocPlus :: SFloat -> SFloat -> SFloat -> SBool
assocPlus :: SFloat -> SFloat -> SFloat -> SBool
assocPlus x :: SFloat
x y :: SFloat
y z :: SFloat
z = SFloat
x SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ (SFloat
y SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ SFloat
z) SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SFloat
x SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ SFloat
y) SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ SFloat
z
assocPlusRegular :: IO ThmResult
assocPlusRegular :: IO ThmResult
assocPlusRegular = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do [x :: SFloat
x, y :: SFloat
y, z :: SFloat
z] <- [String] -> Symbolic [SFloat]
sFloats ["x", "y", "z"]
let lhs :: SFloat
lhs = SFloat
xSFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+(SFloat
ySFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+SFloat
z)
rhs :: SFloat
rhs = (SFloat
xSFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+SFloat
y)SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+SFloat
z
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
lhs
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
rhs
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SFloat
lhs SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SFloat
rhs
nonZeroAddition :: IO ThmResult
nonZeroAddition :: IO ThmResult
nonZeroAddition = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do [a :: SFloat
a, b :: SFloat
b] <- [String] -> Symbolic [SFloat]
sFloats ["a", "b"]
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
a
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
b
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat
a SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ SFloat
b SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SFloat
a
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SFloat
b SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 0
multInverse :: IO ThmResult
multInverse :: IO ThmResult
multInverse = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do SDouble
a <- String -> Symbolic SDouble
sDouble "a"
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SDouble -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SDouble
a
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SDouble -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint (1SDouble -> SDouble -> SDouble
forall a. Fractional a => a -> a -> a
/SDouble
a)
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SDouble
a SDouble -> SDouble -> SDouble
forall a. Num a => a -> a -> a
* (1SDouble -> SDouble -> SDouble
forall a. Fractional a => a -> a -> a
/SDouble
a) SDouble -> SDouble -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 1
roundingAdd :: IO SatResult
roundingAdd :: IO SatResult
roundingAdd = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SRoundingMode
m :: SRoundingMode <- String -> Symbolic SRoundingMode
forall a. SymVal a => String -> Symbolic (SBV a)
free "rm"
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SRoundingMode
m SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= RoundingMode -> SRoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundNearestTiesToEven
SFloat
x <- String -> Symbolic SFloat
sFloat "x"
SFloat
y <- String -> Symbolic SFloat
sFloat "y"
let lhs :: SFloat
lhs = SRoundingMode -> SFloat -> SFloat -> SFloat
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
fpAdd SRoundingMode
m SFloat
x SFloat
y
let rhs :: SFloat
rhs = SFloat
x SFloat -> SFloat -> SFloat
forall a. Num a => a -> a -> a
+ SFloat
y
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
lhs
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
rhs
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SFloat
lhs SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SFloat
rhs