{-# 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
data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
mkSymbolicEnumeration ''Day
instance Metric Day where
type MetricSpace Day = Word8
toMetricSpace x = ite (x .== sMon) 0
$ ite (x .== sTue) 1
$ ite (x .== sWed) 2
$ ite (x .== sThu) 3
$ ite (x .== sFri) 4
$ ite (x .== sSat) 5
6
fromMetricSpace x = ite (x .== 0) sMon
$ ite (x .== 1) sTue
$ ite (x .== 2) sWed
$ ite (x .== 3) sThu
$ ite (x .== 4) sFri
$ ite (x .== 5) sSat
sSun
isWeekend :: SDay -> SBool
isWeekend = (`sElem` weekend)
where weekend = [sSat, sSun]
almostWeekend :: IO OptimizeResult
almostWeekend = optimize Lexicographic $ do
day <- free "almostWeekend"
constrain $ sNot (isWeekend day)
maximize "last-day" day
weekendJustOver :: IO OptimizeResult
weekendJustOver = optimize Lexicographic $ do
day <- free "weekendJustOver"
constrain $ sNot (isWeekend day)
minimize "first-day" day
firstWeekend :: IO OptimizeResult
firstWeekend = optimize Lexicographic $ do
day <- free "firstWeekend"
constrain $ isWeekend day
minimize "first-weekend" day