    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.DeltaSat.DeltaSat
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The encoding of the Flyspec example from the dReal web page
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.DeltaSat.DeltaSat where

    import Data.SBV

    -- | Encode the delta-sat problem as given in <http://dreal.github.io/>
    -- We have:
    --
    -- >>> flyspeck
    -- Unsatisfiable
    flyspeck :: IO SatResult
    flyspeck :: IO SatResult
    flyspeck = SymbolicT IO SBool -> IO SatResult
    forall a. Satisfiable a => a -> IO SatResult
    dsat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do
            SReal
    x1 <- String -> Symbolic SReal
    sReal String
    "x1"
            SReal
    x2 <- String -> Symbolic SReal
    sReal String
    "x2"

            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
    $ SReal
    x1 SReal -> (SReal, SReal) -> SBool
    forall a. OrdSymbolic a => a -> (a, a) -> SBool
    `inRange` ( SReal
    3, SReal
    3.14)
            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
    $ SReal
    x2 SReal -> (SReal, SReal) -> SBool
    forall a. OrdSymbolic a => a -> (a, a) -> SBool
    `inRange` (-SReal
    7, SReal
    5)

            let pi' :: SReal
    pi' = SReal
    3.14159265
                lhs :: SReal
    lhs = SReal
    2 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal
    pi' SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    - SReal
    2 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal
    x1 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal -> SReal
    forall a. Floating a => a -> a
    asin (SReal -> SReal
    forall a. Floating a => a -> a
    cos SReal
    0.979 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal -> SReal
    forall a. Floating a => a -> a
    sin (SReal
    pi' SReal -> SReal -> SReal
    forall a. Fractional a => a -> a -> a
    / SReal
    x1))
                rhs :: SReal
    rhs = -SReal
    0.591 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    - SReal
    0.0331 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal
    x2 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + SReal
    0.506 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + SReal
    1

            SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SReal
    lhs SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SReal
    rhs