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

-- | 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 SBV Day
x   = SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sMon) SBV Word8
SBV (MetricSpace Day)
0
                    (SBV (MetricSpace Day) -> SBV (MetricSpace Day))
-> SBV (MetricSpace Day) -> SBV (MetricSpace Day)
forall a b. (a -> b) -> a -> b
$ SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sTue) SBV Word8
SBV (MetricSpace Day)
1
                    (SBV (MetricSpace Day) -> SBV (MetricSpace Day))
-> SBV (MetricSpace Day) -> SBV (MetricSpace Day)
forall a b. (a -> b) -> a -> b
$ SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sWed) SBV Word8
SBV (MetricSpace Day)
2
                    (SBV (MetricSpace Day) -> SBV (MetricSpace Day))
-> SBV (MetricSpace Day) -> SBV (MetricSpace Day)
forall a b. (a -> b) -> a -> b
$ SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sThu) SBV Word8
SBV (MetricSpace Day)
3
                    (SBV (MetricSpace Day) -> SBV (MetricSpace Day))
-> SBV (MetricSpace Day) -> SBV (MetricSpace Day)
forall a b. (a -> b) -> a -> b
$ SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sFri) SBV Word8
SBV (MetricSpace Day)
4
                    (SBV (MetricSpace Day) -> SBV (MetricSpace Day))
-> SBV (MetricSpace Day) -> SBV (MetricSpace Day)
forall a b. (a -> b) -> a -> b
$ SBool
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
-> SBV (MetricSpace Day)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Day
x SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
sSat) SBV Word8
SBV (MetricSpace Day)
5
                                       SBV Word8
SBV (MetricSpace Day)
6

  fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day
fromMetricSpace 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
.== SBV Word8
0) SBV Day
sMon
                    (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
.== SBV Word8
1) SBV Day
sTue
                    (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
.== SBV Word8
2) SBV Day
sWed
                    (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
.== SBV Word8
3) SBV Day
sThu
                    (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
.== SBV Word8
4) SBV Day
sFri
                    (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
.== SBV Word8
5) SBV Day
sSat
                                    SBV Day
sSun

  annotateForMS :: Proxy Day -> ShowS
annotateForMS Proxy Day
_ String
s = String
"DayAsWord8(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | 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 = [SBV Day
sSat, SBV Day
sSun]

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

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

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