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

    -- | The type synonym 'SDay' is the symbolic variant of 'Day'. (Similar to 'SInteger'/'Integer'
    -- and others.)
    type SDay = SBV 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 (SBV Day
    d1 :: SDay) <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "d1"
                           (SBV Day
    d2 :: SDay) <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "d2"
                           (SBV Day
    d3 :: SDay) <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "d3"

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

                           -- Assert that last day is before 'Thursday'
                           SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Day
    d3 SBV Day -> SBV Day -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Thursday

                           -- 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 (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SBV Day] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct [SBV Day
    d1, SBV Day
    d2, SBV Day
    d3]

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

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