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

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

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

Eq Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

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

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

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

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Day -> Bool

isFP :: 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

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 ()

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])

type MetricSpace Day

Defined in Documentation.SBV.Examples.Optimization.Enumerate

type MetricSpace Day = Word8

type SDay = SBV Day

Symbolic version of the type Day.

sSun :: SBV Day

Symbolic version of the constructor Sun.

sSat :: SBV Day

Symbolic version of the constructor Sat.

sFri :: SBV Day

Symbolic version of the constructor Fri.

sThu :: SBV Day

Symbolic version of the constructor Thu.

sWed :: SBV Day

Symbolic version of the constructor Wed.

sTue :: SBV Day

Symbolic version of the constructor Tue.

sMon :: SBV Day

Symbolic version of the constructor Mon.

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