    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Optimization.Enumerate
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates how enumerations can be used with optimization,
    -- by properly defining your metric values.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Optimization.Enumerate where

    import Data.SBV

    -- | A simple enumeration
    data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun

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

    -- | Give a name to the symbolic variants of 'Day', for convenience
    type SDay = SBV Day

    -- | Make day an optimizable value, by mapping it to 'Word8' in the most
    -- obvious way. We can map it to any value the underlying solver can optimize,
    -- but 'Word8' is the simplest and it'll fit the bill.
    instance Metric Day where
      type MetricSpace Day = Word8

      toMetricSpace :: SBV Day -> SBV (MetricSpace Day)
    toMetricSpace x :: SBV Day
    x   = SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Mon) 0
                        (SBV Word8 -> SBV (MetricSpace Day))
    -> SBV Word8 -> SBV (MetricSpace Day)
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Tue) 1
                        (SBV Word8 -> SBV Word8) -> SBV Word8 -> SBV Word8
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Wed) 2
                        (SBV Word8 -> SBV Word8) -> SBV Word8 -> SBV Word8
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Thu) 3
                        (SBV Word8 -> SBV Word8) -> SBV Word8 -> SBV Word8
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Fri) 4
                        (SBV Word8 -> SBV Word8) -> SBV Word8 -> SBV Word8
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Word8 -> SBV Word8 -> SBV Word8
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Day
    x SBV Day -> SBV Day -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Sat) 5
                                                  6

      fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day
    fromMetricSpace x :: SBV (MetricSpace Day)
    x = SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 0) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Mon)
                        (SBV Day -> SBV Day) -> SBV Day -> SBV Day
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 1) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Tue)
                        (SBV Day -> SBV Day) -> SBV Day -> SBV Day
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 2) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Wed)
                        (SBV Day -> SBV Day) -> SBV Day -> SBV Day
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 3) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Thu)
                        (SBV Day -> SBV Day) -> SBV Day -> SBV Day
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 4) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Fri)
                        (SBV Day -> SBV Day) -> SBV Day -> SBV Day
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBV Day -> SBV Day -> SBV Day
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV Word8
    SBV (MetricSpace Day)
    x SBV Word8 -> SBV Word8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 5) (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Sat)
                                        (Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal Day
    Sun)

    -- | Identify weekend days
    isWeekend :: SDay -> SBool
    isWeekend :: SBV Day -> SBool
    isWeekend = (SBV Day -> [SBV Day] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SBV Day]
    weekend)
      where weekend :: [SBV Day]
    weekend = (Day -> SBV Day) -> [Day] -> [SBV Day]
    forall a b. (a -> b) -> [a] -> [b]
    map Day -> SBV Day
    forall a. SymVal a => a -> SBV a
    literal [Day
    Sat, Day
    Sun]

    -- | Using optimization, find the latest day that is not a weekend.
    -- We have:
    --
    -- >>> almostWeekend
    -- Optimal model:
    --   almostWeekend = Fri :: Day
    --   last-day      =   4 :: Word8
    almostWeekend :: IO OptimizeResult
    almostWeekend :: IO OptimizeResult
    almostWeekend = OptimizeStyle -> SymbolicT IO () -> IO OptimizeResult
    forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
    optimize OptimizeStyle
    Lexicographic (SymbolicT IO () -> IO OptimizeResult)
    -> SymbolicT IO () -> IO OptimizeResult
    forall a b. (a -> b) -> a -> b
    $ do
                        SBV Day
    day <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "almostWeekend"
                        SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBV Day -> SBool
    isWeekend SBV Day
    day)
                        String -> SBV Day -> SymbolicT IO ()
    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
    maximize "last-day" SBV Day
    day

    -- | Using optimization, find the first day after the weekend.
    -- We have:
    --
    -- >>> weekendJustOver
    -- Optimal model:
    --   weekendJustOver = Mon :: Day
    --   first-day       =   0 :: Word8
    weekendJustOver :: IO OptimizeResult
    weekendJustOver :: IO OptimizeResult
    weekendJustOver = OptimizeStyle -> SymbolicT IO () -> IO OptimizeResult
    forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
    optimize OptimizeStyle
    Lexicographic (SymbolicT IO () -> IO OptimizeResult)
    -> SymbolicT IO () -> IO OptimizeResult
    forall a b. (a -> b) -> a -> b
    $ do
                          SBV Day
    day <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "weekendJustOver"
                          SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBV Day -> SBool
    isWeekend SBV Day
    day)
                          String -> SBV Day -> SymbolicT IO ()
    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
    minimize "first-day" SBV Day
    day

    -- | Using optimization, find the first weekend day:
    -- We have:
    --
    -- >>> firstWeekend
    -- Optimal model:
    --   firstWeekend  = Sat :: Day
    --   first-weekend =   5 :: Word8
    firstWeekend :: IO OptimizeResult
    firstWeekend :: IO OptimizeResult
    firstWeekend = OptimizeStyle -> SymbolicT IO () -> IO OptimizeResult
    forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
    optimize OptimizeStyle
    Lexicographic (SymbolicT IO () -> IO OptimizeResult)
    -> SymbolicT IO () -> IO OptimizeResult
    forall a b. (a -> b) -> a -> b
    $ do
                          SBV Day
    day <- String -> Symbolic (SBV Day)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "firstWeekend"
                          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 -> SBool
    isWeekend SBV Day
    day
                          String -> SBV Day -> SymbolicT IO ()
    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
    minimize "first-weekend" SBV Day
    day