-----------------------------------------------------------------------------
-- |
-- 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
        x1 <- String -> Symbolic SReal
sReal String
"x1"
        x2 <- sReal "x2"

        constrain $ x1 `inRange` ( 3, 3.14)
        constrain $ x2 `inRange` (-7, 5)

        let pi' = SReal
3.14159265
            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
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

        pure $ lhs .<= rhs