sbv-11.4: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

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
sMon :: SBV Day
sTue :: SBV Day
sWed :: SBV Day
sThu :: SBV Day
sFri :: SBV Day
sSat :: SBV Day
sSun :: 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

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

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 #

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

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Day) Source #

literal :: Day -> SBV Day Source #

fromCV :: CV -> Day Source #

isConcretely :: SBV Day -> (Day -> Bool) -> Bool 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 #

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 #

isRational :: Day -> Bool Source #

isFP :: Day -> Bool Source #

isUnbounded :: Day -> Bool Source #

isUserSort :: 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 #

isArray :: Day -> Bool Source #

showType :: Day -> String 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
Instance details Defined in Documentation.SBV.Examples.Optimization.Enumerate type MetricSpace Day = Word8

Methods

toMetricSpace :: SBV Day -> SBV (MetricSpace Day) Source #

fromMetricSpace :: SBV (MetricSpace Day) -> SBV Day Source #

annotateForMS :: Proxy Day -> String -> String Source #

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m () Source #

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV Day -> m () Source #

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 MetricSpace Day = Word8

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

weekendJustOver :: IO OptimizeResult Source #

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

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

firstWeekend :: IO OptimizeResult Source #

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

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