{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Queries.CaseSplit where
import Data.SBV
import Data.SBV.Control
csDemo1 :: IO (String, Float)
csDemo1 :: IO (String, Float)
csDemo1 = Symbolic (String, Float) -> IO (String, Float)
forall a. Symbolic a -> IO a
runSMT (Symbolic (String, Float) -> IO (String, Float))
-> Symbolic (String, Float) -> IO (String, Float)
forall a b. (a -> b) -> a -> b
$ do
SFloat
x <- String -> Symbolic SFloat
sFloat "x"
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SFloat
x SFloat -> SFloat -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SFloat
x
Query (String, Float) -> Symbolic (String, Float)
forall a. Query a -> Symbolic a
query (Query (String, Float) -> Symbolic (String, Float))
-> Query (String, Float) -> Symbolic (String, Float)
forall a b. (a -> b) -> a -> b
$ do Maybe (String, SMTResult)
mbR <- Bool -> [(String, SBool)] -> Query (Maybe (String, SMTResult))
caseSplit Bool
True [ ("fpIsNegativeZero", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SFloat
x)
, ("fpIsPositiveZero", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPositiveZero SFloat
x)
, ("fpIsNormal", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNormal SFloat
x)
, ("fpIsSubnormal", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsSubnormal SFloat
x)
, ("fpIsPoint", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint SFloat
x)
, ("fpIsNaN", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN SFloat
x)
]
case Maybe (String, SMTResult)
mbR of
Nothing -> String -> Query (String, Float)
forall a. HasCallStack => String -> a
error "Cannot find a FP number x such that x == x + 1"
Just (s :: String
s, _) -> do Float
xv <- SFloat -> Query Float
forall a. SymVal a => SBV a -> Query a
getValue SFloat
x
(String, Float) -> Query (String, Float)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, Float
xv)
csDemo2 :: IO (String, Integer)
csDemo2 :: IO (String, Integer)
csDemo2 = Symbolic (String, Integer) -> IO (String, Integer)
forall a. Symbolic a -> IO a
runSMT (Symbolic (String, Integer) -> IO (String, Integer))
-> Symbolic (String, Integer) -> IO (String, Integer)
forall a b. (a -> b) -> a -> b
$ do
SInteger
x <- String -> Symbolic SInteger
sInteger "x"
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 10
Query (String, Integer) -> Symbolic (String, Integer)
forall a. Query a -> Symbolic a
query (Query (String, Integer) -> Symbolic (String, Integer))
-> Query (String, Integer) -> Symbolic (String, Integer)
forall a b. (a -> b) -> a -> b
$ do Maybe (String, SMTResult)
mbR <- Bool -> [(String, SBool)] -> Query (Maybe (String, SMTResult))
caseSplit Bool
True [ ("negative" , SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< 0)
, ("less than 8", SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< 8)
]
case Maybe (String, SMTResult)
mbR of
Nothing -> String -> Query (String, Integer)
forall a. HasCallStack => String -> a
error "Cannot find a solution!"
Just (s :: String
s, _) -> do Integer
xv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
x
(String, Integer) -> Query (String, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, Integer
xv)