-----------------------------------------------------------------------------
-- |
-- 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

-- | 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 = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do (SDay
d1 :: SDay) <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d1"
                       (SDay
d2 :: SDay) <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d2"
                       (SDay
d3 :: SDay) <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d3"

                       -- Assert that they are ordered
                       forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SDay
d1 forall a. OrdSymbolic a => a -> a -> SBool
.<= SDay
d2
                       forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SDay
d2 forall a. OrdSymbolic a => a -> a -> SBool
.<= SDay
d3

                       -- Assert that last day is before 'Thursday'
                       forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SDay
d3 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.

                       forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ 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 <- forall a. SymVal a => SBV a -> Query a
getValue SDay
d1
                                              Day
b <- forall a. SymVal a => SBV a -> Query a
getValue SDay
d2
                                              Day
c <- forall a. SymVal a => SBV a -> Query a
getValue SDay
d3
                                              forall (m :: * -> *) a. Monad m => a -> m a
return [Day
a, Day
b, Day
c]

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