-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Queries.Enums
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates the use of enumeration values during queries.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Queries.Enums where

import Data.SBV
import Data.SBV.Control

-- | Days of the week. We make it symbolic using the 'mkSymbolicEnumeration' splice.
data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
         deriving (Day -> Day -> Bool
(Day -> Day -> Bool) -> (Day -> Day -> Bool) -> Eq Day
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Day -> Day -> Bool
== :: Day -> Day -> Bool
$c/= :: Day -> Day -> Bool
/= :: Day -> Day -> Bool
Eq, Eq Day
Eq Day =>
(Day -> Day -> Ordering)
-> (Day -> Day -> Bool)
-> (Day -> Day -> Bool)
-> (Day -> Day -> Bool)
-> (Day -> Day -> Bool)
-> (Day -> Day -> Day)
-> (Day -> Day -> Day)
-> Ord Day
Day -> Day -> Bool
Day -> Day -> Ordering
Day -> Day -> Day
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Day -> Day -> Ordering
compare :: Day -> Day -> Ordering
$c< :: Day -> Day -> Bool
< :: Day -> Day -> Bool
$c<= :: Day -> Day -> Bool
<= :: Day -> Day -> Bool
$c> :: Day -> Day -> Bool
> :: Day -> Day -> Bool
$c>= :: Day -> Day -> Bool
>= :: Day -> Day -> Bool
$cmax :: Day -> Day -> Day
max :: Day -> Day -> Day
$cmin :: Day -> Day -> Day
min :: Day -> Day -> Day
Ord, Day
Day -> Day -> Bounded Day
forall a. a -> a -> Bounded a
$cminBound :: Day
minBound :: Day
$cmaxBound :: Day
maxBound :: Day
Bounded, Int -> Day
Day -> Int
Day -> [Day]
Day -> Day
Day -> Day -> [Day]
Day -> Day -> Day -> [Day]
(Day -> Day)
-> (Day -> Day)
-> (Int -> Day)
-> (Day -> Int)
-> (Day -> [Day])
-> (Day -> Day -> [Day])
-> (Day -> Day -> [Day])
-> (Day -> Day -> Day -> [Day])
-> Enum Day
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Day -> Day
succ :: Day -> Day
$cpred :: Day -> Day
pred :: Day -> Day
$ctoEnum :: Int -> Day
toEnum :: Int -> Day
$cfromEnum :: Day -> Int
fromEnum :: Day -> Int
$cenumFrom :: Day -> [Day]
enumFrom :: Day -> [Day]
$cenumFromThen :: Day -> Day -> [Day]
enumFromThen :: Day -> Day -> [Day]
$cenumFromTo :: Day -> Day -> [Day]
enumFromTo :: Day -> Day -> [Day]
$cenumFromThenTo :: Day -> Day -> Day -> [Day]
enumFromThenTo :: Day -> Day -> Day -> [Day]
Enum)

-- | Make 'Day' a symbolic value.
mkSymbolicEnumeration ''Day

-- | A trivial query to find three consecutive days that's all before 'Thursday'. The point
-- here is that we can perform queries on such enumerated values and use 'getValue' on them
-- and return their values from queries just like any other value. We have:
--
-- >>> findDays
-- [Monday,Tuesday,Wednesday]
findDays :: IO [Day]
findDays :: IO [Day]
findDays = Symbolic [Day] -> IO [Day]
forall a. Symbolic a -> IO a
runSMT (Symbolic [Day] -> IO [Day]) -> Symbolic [Day] -> IO [Day]
forall a b. (a -> b) -> a -> b
$ do (SDay
d1 :: SDay) <- String -> Symbolic SDay
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d1"
                       (SDay
d2 :: SDay) <- String -> Symbolic SDay
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d2"
                       (SDay
d3 :: SDay) <- String -> Symbolic SDay
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d3"

                       -- Assert that they are ordered
                       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
$ SDay
d1 SDay -> SDay -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SDay
d2
                       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
$ SDay
d2 SDay -> SDay -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SDay
d3

                       -- Assert that last day is before 'Thursday'
                       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
$ SDay
d3 SDay -> SDay -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SDay
sThursday

                       -- Constraints can be given before or after
                       -- the query mode starts. We will assert that
                       -- they are different after we start interacting
                       -- with the solver. Note that we can query the
                       -- values based on other values obtained too,
                       -- if we want to guide the search.

                       Query [Day] -> Symbolic [Day]
forall a. Query a -> Symbolic a
query (Query [Day] -> Symbolic [Day]) -> Query [Day] -> Symbolic [Day]
forall a b. (a -> b) -> a -> b
$ do SBool -> QueryT IO ()
forall a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [SDay] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct [SDay
d1, SDay
d2, SDay
d3]

                                  CheckSatResult
cs <- Query CheckSatResult
checkSat
                                  case CheckSatResult
cs of
                                    CheckSatResult
Sat -> do Day
a <- SDay -> Query Day
forall a. SymVal a => SBV a -> Query a
getValue SDay
d1
                                              Day
b <- SDay -> Query Day
forall a. SymVal a => SBV a -> Query a
getValue SDay
d2
                                              Day
c <- SDay -> Query Day
forall a. SymVal a => SBV a -> Query a
getValue SDay
d3
                                              [Day] -> Query [Day]
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Day
a, Day
b, Day
c]

                                    CheckSatResult
_   -> String -> Query [Day]
forall a. HasCallStack => String -> a
error String
"Impossible, can't find days!"