-----------------------------------------------------------------------------
-- |
-- 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 = 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 String
"d1"
                       (SBV Day
d2 :: SDay) <- String -> Symbolic (SBV Day)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"d2"
                       (SBV Day
d3 :: SDay) <- String -> Symbolic (SBV Day)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"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
.< SBV Day
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 (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
                                    CheckSatResult
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]

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