{-# 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
type SDay = SBV Day
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)
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]
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
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
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