1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
-----------------------------------------------------------------------------
-- |
-- 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 = dsat $ do
x1 <- sReal "x1"
x2 <- sReal "x2"
constrain $ x1 `inRange` ( 3, 3.14)
constrain $ x2 `inRange` (-7, 5)
let pi' = 3.14159265
lhs = 2 * pi' - 2 * x1 * asin (cos 0.979 * sin (pi' / x1))
rhs = -0.591 - 0.0331 * x2 + 0.506 + 1
pure $ lhs .<= rhs
|
