{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Misc.Floating where
import Data.SBV
assocPlus :: SFloat -> SFloat -> SFloat -> SBool
assocPlus :: SBV Float -> SBV Float -> SBV Float -> SBool
assocPlus SBV Float
x SBV Float
y SBV Float
z = SBV Float
x SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ (SBV Float
y SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
z) SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Float
x SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
y) SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
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 [SBV Float
x, SBV Float
y, SBV Float
z] <- [String] -> Symbolic [SBV Float]
sFloats [String
"x", String
"y", String
"z"]
let lhs :: SBV Float
lhs = SBV Float
xSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+(SBV Float
ySBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
z)
rhs :: SBV Float
rhs = (SBV Float
xSBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
y)SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+SBV Float
z
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
lhs
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
rhs
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Float
lhs SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Float
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 [SBV Float
a, SBV Float
b] <- [String] -> Symbolic [SBV Float]
sFloats [String
"a", String
"b"]
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
a
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
b
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float
a SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
b SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Float
a
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Float
b SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Float
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 SBV Float
a <- String -> Symbolic (SBV Float)
sFloat String
"a"
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
a
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint (SBV Float
1SBV Float -> SBV Float -> SBV Float
forall a. Fractional a => a -> a -> a
/SBV Float
a)
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Float
a SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
* (SBV Float
1SBV Float -> SBV Float -> SBV Float
forall a. Fractional a => a -> a -> a
/SBV Float
a) SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Float
1
roundingAdd :: IO SatResult
roundingAdd :: IO SatResult
roundingAdd = SymbolicT IO SBool -> IO SatResult
forall a. Satisfiable 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 String
"rm"
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> 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
SBV Float
x <- String -> Symbolic (SBV Float)
sFloat String
"x"
SBV Float
y <- String -> Symbolic (SBV Float)
sFloat String
"y"
let lhs :: SBV Float
lhs = SRoundingMode -> SBV Float -> SBV Float -> SBV Float
forall a.
IEEEFloating a =>
SRoundingMode -> SBV a -> SBV a -> SBV a
fpAdd SRoundingMode
m SBV Float
x SBV Float
y
let rhs :: SBV Float
rhs = SBV Float
x SBV Float -> SBV Float -> SBV Float
forall a. Num a => a -> a -> a
+ SBV Float
y
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
lhs
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Float -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SBV Float
rhs
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Float
lhs SBV Float -> SBV Float -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Float
rhs
fp54Bounds :: IO OptimizeResult
fp54Bounds :: IO OptimizeResult
fp54Bounds = OptimizeStyle -> SymbolicT IO SBool -> IO OptimizeResult
forall a. Satisfiable a => OptimizeStyle -> a -> IO OptimizeResult
optimize OptimizeStyle
Independent (SymbolicT IO SBool -> IO OptimizeResult)
-> SymbolicT IO SBool -> IO OptimizeResult
forall a b. (a -> b) -> a -> b
$ do SFloatingPoint 5 4
x :: SFloatingPoint 5 4 <- String -> Symbolic (SFloatingPoint 5 4)
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint String
"x"
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloatingPoint 5 4 -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloatingPoint 5 4
x
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloatingPoint 5 4
x SFloatingPoint 5 4 -> SFloatingPoint 5 4 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SFloatingPoint 5 4
0
String -> SFloatingPoint 5 4 -> SymbolicT IO ()
forall a. Metric a => String -> SBV a -> SymbolicT IO ()
maximize String
"max" SFloatingPoint 5 4
x
String -> SFloatingPoint 5 4 -> SymbolicT IO ()
forall a. Metric a => String -> SBV a -> SymbolicT IO ()
minimize String
"min" SFloatingPoint 5 4
x
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBool
sTrue