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

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

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