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