-----------------------------------------------------------------------------
-- |
-- 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 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
.== SBV Day
sMon) SBV Word8
0
                    (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
.== SBV Day
sTue) SBV Word8
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
.== SBV Day
sWed) SBV Word8
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
.== SBV Day
sThu) SBV Word8
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
.== SBV Day
sFri) SBV Word8
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
.== SBV Day
sSat) SBV Word8
5
                                       SBV Word8
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

-- | 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
--   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 String
"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 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 = 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 String
"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 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 = 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 String
"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 String
"first-weekend" SBV Day
day