Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.Optimization.Enumerate
Description
Demonstrates how enumerations can be used with optimization, by properly defining your metric values.
Synopsis
- data Day
- type SDay = SBV Day
- isWeekend :: SDay -> SBool
- almostWeekend :: IO OptimizeResult
- weekendJustOver :: IO OptimizeResult
- firstWeekend :: IO OptimizeResult
Documentation
A simple enumeration
Instances
Eq Day Source # | |
Data Day Source # | |
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 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 Source # | |
Read Day Source # | |
Show Day Source # | |
HasKind Day Source # | |
Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods kindOf :: Day -> Kind Source # hasSign :: Day -> Bool Source # intSizeOf :: Day -> Int Source # isBoolean :: Day -> Bool Source # isBounded :: Day -> Bool Source # isReal :: Day -> Bool Source # isFloat :: Day -> Bool Source # isDouble :: Day -> Bool Source # isUnbounded :: Day -> Bool Source # isUninterpreted :: Day -> Bool Source # isChar :: Day -> Bool Source # isString :: Day -> Bool Source # isList :: Day -> Bool Source # isTuple :: Day -> Bool Source # isMaybe :: Day -> Bool Source # | |
SymVal Day Source # | |
Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Day) Source # literal :: Day -> SBV Day Source # isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Day) Source # forall_ :: MonadSymbolic m => m (SBV Day) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Day] Source # exists :: MonadSymbolic m => String -> m (SBV Day) Source # exists_ :: MonadSymbolic m => m (SBV Day) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Day] Source # free :: MonadSymbolic m => String -> m (SBV Day) Source # free_ :: MonadSymbolic m => m (SBV Day) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Day] Source # symbolic :: MonadSymbolic m => String -> m (SBV Day) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Day] Source # unliteral :: SBV Day -> Maybe Day Source # isConcrete :: SBV Day -> Bool Source # isSymbolic :: SBV Day -> Bool Source # | |
SatModel Day Source # | Make |
Metric Day Source # | Make day an optimizable value, by mapping it to |
Defined in Documentation.SBV.Examples.Optimization.Enumerate Associated Types type MetricSpace Day Source # Methods toMetricSpace :: SBV Day -> SBV (MetricSpace Day) Source # fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m () Source # | |
type MetricSpace Day Source # | |
almostWeekend :: IO OptimizeResult Source #
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 Source #
Using optimization, find the first day after the weekend. We have:
>>>
weekendJustOver
Optimal model: weekendJustOver = Mon :: Day first-day = 0 :: Word8
firstWeekend :: IO OptimizeResult Source #
Using optimization, find the first weekend day: We have:
>>>
firstWeekend
Optimal model: firstWeekend = Sat :: Day first-weekend = 5 :: Word8