    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Queries.CaseSplit
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A couple of demonstrations for the 'caseSplit' function.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Queries.CaseSplit where

    import Data.SBV
    import Data.SBV.Control

    -- | A simple floating-point problem, but we do the sat-analysis via a case-split.
    -- Due to the nature of floating-point numbers, a case-split on the characteristics
    -- of the number (such as NaN, negative-zero, etc. is most suitable.)
    --
    -- We have:
    --
    -- >>> csDemo1
    -- Case fpIsNegativeZero: Starting
    -- Case fpIsNegativeZero: Unsatisfiable
    -- Case fpIsPositiveZero: Starting
    -- Case fpIsPositiveZero: Unsatisfiable
    -- Case fpIsNormal: Starting
    -- Case fpIsNormal: Unsatisfiable
    -- Case fpIsSubnormal: Starting
    -- Case fpIsSubnormal: Unsatisfiable
    -- Case fpIsPoint: Starting
    -- Case fpIsPoint: Unsatisfiable
    -- Case fpIsNaN: Starting
    -- Case fpIsNaN: Satisfiable
    -- ("fpIsNaN",NaN)
    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 -- yes, in the FP land, this does hold

           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"  -- Won't happen!
                        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)

    -- | Demonstrates the "coverage" case.
    --
    -- We have:
    --
    -- >>> csDemo2
    -- Case negative: Starting
    -- Case negative: Unsatisfiable
    -- Case less than 8: Starting
    -- Case less than 8: Unsatisfiable
    -- Case Coverage: Starting
    -- Case Coverage: Satisfiable
    -- ("Coverage",10)
    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!" -- Won't happen!
                        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)