Documentation.SBV.Examples.Optimization.Enumerate

Demonstrates how enumerations can be used with optimization, by properly defining your metric values.

Documentation

data Day

A simple enumeration

Constructors

Mon

Tue

Wed

Thu

Fri

Sat

Sun

Instances

Eq Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

(==) :: Day -> Day -> Bool

(/=) :: Day -> Day -> Bool

Data Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Day -> c Day

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Day

toConstr :: Day -> Constr

dataTypeOf :: Day -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Day)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Day)

gmapT :: (forall b. Data b => b -> b) -> Day -> Day

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r

gmapQ :: (forall d. Data d => d -> u) -> Day -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Day -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Day -> m Day

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day

Ord Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

compare :: Day -> Day -> Ordering

(<) :: Day -> Day -> Bool

(<=) :: Day -> Day -> Bool

(>) :: Day -> Day -> Bool

(>=) :: Day -> Day -> Bool

max :: Day -> Day -> Day

min :: Day -> Day -> Day

Read Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

readsPrec :: Int -> ReadS Day

readList :: ReadS [Day]

readPrec :: ReadPrec Day

readListPrec :: ReadPrec [Day]

Show Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

showsPrec :: Int -> Day -> ShowS

show :: Day -> String

showList :: [Day] -> ShowS

HasKind Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

kindOf :: Day -> Kind

hasSign :: Day -> Bool

intSizeOf :: Day -> Int

isBoolean :: Day -> Bool

isBounded :: Day -> Bool

isReal :: Day -> Bool

isFloat :: Day -> Bool

isDouble :: Day -> Bool

isUnbounded :: Day -> Bool

isUserSort :: Day -> Bool

isChar :: Day -> Bool

isString :: Day -> Bool

isList :: Day -> Bool

isSet :: Day -> Bool

isTuple :: Day -> Bool

isMaybe :: Day -> Bool

isEither :: Day -> Bool

showType :: Day -> String

SymVal Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Day)

literal :: Day -> SBV Day

fromCV :: CV -> Day

isConcretely :: SBV Day -> (Day -> Bool) -> Bool

forall :: MonadSymbolic m => String -> m (SBV Day)

forall_ :: MonadSymbolic m => m (SBV Day)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Day]

exists :: MonadSymbolic m => String -> m (SBV Day)

exists_ :: MonadSymbolic m => m (SBV Day)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Day]

free :: MonadSymbolic m => String -> m (SBV Day)

free_ :: MonadSymbolic m => m (SBV Day)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Day]

symbolic :: MonadSymbolic m => String -> m (SBV Day)

symbolics :: MonadSymbolic m => [String] -> m [SBV Day]

unliteral :: SBV Day -> Maybe Day

isConcrete :: SBV Day -> Bool

isSymbolic :: SBV Day -> Bool

SatModel Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

parseCVs :: [CV] -> Maybe (Day, [CV])

cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV])

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

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Associated Types

type MetricSpace Day

Methods

toMetricSpace :: SBV Day -> SBV (MetricSpace Day)

fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m ()

type MetricSpace Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

type MetricSpace Day = Word8

type SDay = SBV Day

Make Day a symbolic value.

sSun :: SBV Day

sSat :: SBV Day

sFri :: SBV Day

sThu :: SBV Day

sWed :: SBV Day

sTue :: SBV Day

sMon :: SBV Day

isWeekend :: SDay -> SBool

Identify weekend days

almostWeekend :: IO OptimizeResult

Using optimization, find the latest day that is not a weekend. We have:

>>> almostWeekend
Optimal model:
  almostWeekend = Fri :: Day
  last-day      =   4 :: Word8

weekendJustOver :: IO OptimizeResult

Using optimization, find the first day after the weekend. We have:

>>> weekendJustOver
Optimal model:
  weekendJustOver = Mon :: Day
  first-day       =   0 :: Word8

firstWeekend :: IO OptimizeResult

Using optimization, find the first weekend day: We have:

>>> firstWeekend
Optimal model:
  firstWeekend  = Sat :: Day
  first-weekend =   5 :: Word8