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

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
 Source # Instance details Methods(==) :: Day -> Day -> Bool #(/=) :: Day -> Day -> Bool # Source # Instance details Methodsgfoldl :: (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 #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 # Source # Instance details Methodscompare :: Day -> Day -> Ordering #(<) :: Day -> Day -> Bool #(<=) :: Day -> Day -> Bool #(>) :: Day -> Day -> Bool #(>=) :: Day -> Day -> Bool #max :: Day -> Day -> Day #min :: Day -> Day -> Day # Source # Instance details Methods Source # Instance details MethodsshowsPrec :: Int -> Day -> ShowS #show :: Day -> String #showList :: [Day] -> ShowS # Source # Instance details Methods Source # Instance details MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV 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 # Source # Make Day a symbolic value. Instance details MethodsparseCVs :: [CV] -> Maybe (Day, [CV]) Source #cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) Source # Source # Instance details MethodssexprToVal :: SExpr -> Maybe Day Source # 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 Associated Types MethodsmsMinimize :: (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 type MetricSpace Day = Word8

type SDay = SBV Day Source #

Give a name to the symbolic variants of Day, for convenience

Identify weekend days

Using optimization, find the latest day that is not a weekend. We have:

>>> almostWeekend
Optimal model:
almostWeekend = Fri :: Day
last-day      =   4 :: Word8


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

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


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

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