sbv-8.3: 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
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

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

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

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 #

type MetricSpace Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

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