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

  fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day
fromMetricSpace SBV (MetricSpace Day)
x = forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
0) SBV Day
sMon
                    forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
1) SBV Day
sTue
                    forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
2) SBV Day
sWed
                    forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
3) SBV Day
sThu
                    forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
4) SBV Day
sFri
                    forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV (MetricSpace Day)
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
5) SBV Day
sSat
                                    SBV Day
sSun

-- | Identify weekend days
isWeekend :: SDay -> SBool
isWeekend :: SBV Day -> SBool
isWeekend = (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
--   last-day      =   4 :: Word8
almostWeekend :: IO OptimizeResult
almostWeekend :: IO OptimizeResult
almostWeekend = forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
optimize OptimizeStyle
Lexicographic forall a b. (a -> b) -> a -> b
$ do
                    SBV Day
day <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"almostWeekend"
                    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBV Day -> SBool
isWeekend SBV Day
day)
                    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
maximize String
"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 = forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
optimize OptimizeStyle
Lexicographic forall a b. (a -> b) -> a -> b
$ do
                      SBV Day
day <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"weekendJustOver"
                      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBV Day -> SBool
isWeekend SBV Day
day)
                      forall a. Metric a => String -> SBV a -> SymbolicT IO ()
minimize String
"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 = forall a. Provable a => OptimizeStyle -> a -> IO OptimizeResult
optimize OptimizeStyle
Lexicographic forall a b. (a -> b) -> a -> b
$ do
                      SBV Day
day <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"firstWeekend"
                      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Day -> SBool
isWeekend SBV Day
day
                      forall a. Metric a => String -> SBV a -> SymbolicT IO ()
minimize String
"first-weekend" SBV Day
day