-----------------------------------------------------------------------------
-- |
-- 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 String
"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 [ (String
"fpIsNegativeZero", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNegativeZero SFloat
x)
                                        , (String
"fpIsPositiveZero", SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPositiveZero SFloat
x)
                                        , (String
"fpIsNormal",       SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNormal       SFloat
x)
                                        , (String
"fpIsSubnormal",    SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsSubnormal    SFloat
x)
                                        , (String
"fpIsPoint",        SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsPoint        SFloat
x)
                                        , (String
"fpIsNaN",          SFloat -> SBool
forall a. IEEEFloating a => SBV a -> SBool
fpIsNaN          SFloat
x)
                                        ]

                  case Maybe (String, SMTResult)
mbR of
                    Maybe (String, SMTResult)
Nothing     -> String -> Query (String, Float)
forall a. HasCallStack => String -> a
error String
"Cannot find a FP number x such that x == x + 1"  -- Won't happen!
                    Just (String
s, SMTResult
_) -> 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 String
"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
.== SInteger
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 [ (String
"negative"   , SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
0)
                                        , (String
"less than 8", SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
8)
                                        ]

                  case Maybe (String, SMTResult)
mbR of
                    Maybe (String, SMTResult)
Nothing     -> String -> Query (String, Integer)
forall a. HasCallStack => String -> a
error String
"Cannot find a solution!" -- Won't happen!
                    Just (String
s, SMTResult
_) -> 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)