-----------------------------------------------------------------------------
-- |
-- 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. Provable 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 (m :: * -> *). SolverContext m => SBool -> 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 (m :: * -> *). SolverContext m => SBool -> 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 (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