-----------------------------------------------------------------------------
-- |
-- 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 = forall a. Provable a => a -> IO SatResult
dsat forall a b. (a -> b) -> a -> b
$ do
        SReal
x1 <- String -> Symbolic SReal
sReal String
"x1"
        SReal
x2 <- String -> Symbolic SReal
sReal String
"x2"

        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x1 forall a. OrdSymbolic a => a -> (a, a) -> SBool
`inRange` ( SReal
3, SReal
3.14)
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x2 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 forall a. Num a => a -> a -> a
* SReal
pi' forall a. Num a => a -> a -> a
- SReal
2 forall a. Num a => a -> a -> a
* SReal
x1 forall a. Num a => a -> a -> a
* forall a. Floating a => a -> a
asin (forall a. Floating a => a -> a
cos SReal
0.979 forall a. Num a => a -> a -> a
* forall a. Floating a => a -> a
sin (SReal
pi' forall a. Fractional a => a -> a -> a
/ SReal
x1))
            rhs :: SReal
rhs = -SReal
0.591 forall a. Num a => a -> a -> a
- SReal
0.0331 forall a. Num a => a -> a -> a
* SReal
x2 forall a. Num a => a -> a -> a
+ SReal
0.506 forall a. Num a => a -> a -> a
+ SReal
1

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