sbv-10.12: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Optimization.Enumerate

Description

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

Synopsis

Documentation

data Day Source #

A simple enumeration

Constructors

Mon 
Tue 
Wed 
Thu 
Fri 
Sat 
Sun 

Instances

Instances details
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 :: 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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Show Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

showsPrec :: Int -> Day -> ShowS #

show :: Day -> String #

showList :: [Day] -> ShowS #

Eq Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

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

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

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 #

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

HasKind Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

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 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

SatModel Day Source # 
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 #

type MetricSpace Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

type SDay = SBV Day Source #

Symbolic version of the type Day.

sMon :: SBV Day Source #

Symbolic version of the constructor Mon.

sTue :: SBV Day Source #

Symbolic version of the constructor Tue.

sWed :: SBV Day Source #

Symbolic version of the constructor Wed.

sThu :: SBV Day Source #

Symbolic version of the constructor Thu.

sFri :: SBV Day Source #

Symbolic version of the constructor Fri.

sSat :: SBV Day Source #

Symbolic version of the constructor Sat.

sSun :: SBV Day Source #

Symbolic version of the constructor Sun.

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:
  last-day             = Fri :: Day
  almostWeekend        = Fri :: Day
  DayAsWord8(last-day) =   4 :: Word8

weekendJustOver :: IO OptimizeResult Source #

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

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

firstWeekend :: IO OptimizeResult Source #

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

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