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
- = Mon
- | Tue
- | Wed
- | Thu
- | Fri
- | Sat
- | Sun
type SDay = SBV Day
isWeekend :: SDay -> SBool
almostWeekend :: IO OptimizeResult
weekendJustOver :: IO OptimizeResult
firstWeekend :: IO OptimizeResult

Documentation

data Day Source #

A simple enumeration

Constructors

Mon
Tue
Wed
Thu
Fri
Sat
Sun

Instances

Eq Day Source #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods (==) :: Day -> Day -> Bool # (/=) :: Day -> Day -> Bool #
Data Day Source #
Instance details 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 :: (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 #
Instance details 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 Source #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods readsPrec :: Int -> ReadS Day # readList :: ReadS [Day] # readPrec :: ReadPrec Day # readListPrec :: ReadPrec [Day] #
Show Day Source #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods showsPrec :: Int -> Day -> ShowS # show :: Day -> String # showList :: [Day] -> ShowS #
HasKind Day Source #
Instance details 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 # isSet :: Day -> Bool Source # isTuple :: Day -> Bool Source # isMaybe :: Day -> Bool Source # isEither :: Day -> Bool Source # showType :: Day -> String Source #
SymVal Day Source #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Day) Source # literal :: Day -> SBV Day Source # fromCV :: CV -> 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 `Day` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods parseCVs :: [CV] -> Maybe (Day, [CV]) Source # cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) Source #
SMTValue Day Source #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate Methods sexprToVal :: SExpr -> Maybe Day Source #
Metric Day Source #	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 details Defined in Documentation.SBV.Examples.Optimization.Enumerate Associated Types type MetricSpace Day :: Type 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 #
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate type MetricSpace Day = Word8

type SDay = SBV Day Source #

Give a name to the symbolic variants of Day, for convenience

isWeekend :: SDay -> SBool Source #

Identify weekend days

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