sbv-13.1: 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
Arbitrary Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

arbitrary :: Gen Day #

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

mkSymValInit :: State -> SBV Day -> IO () Source #

literal :: Day -> SBV Day Source #

fromCV :: CV -> Day Source #

isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source #

minMaxBound :: Maybe (Day, 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 #

unlitCV :: SBV Day -> Maybe (Kind, CVal) 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 #

isADT :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

isSet :: Day -> Bool Source #

isTuple :: Day -> Bool Source #

isArray :: Day -> Bool Source #

isRoundingMode :: Day -> Bool Source #

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

EnumSymbolic Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

succ :: SBV Day -> SBV Day Source #

pred :: SBV Day -> SBV Day Source #

toEnum :: SInteger -> SBV Day Source #

fromEnum :: SBV Day -> SInteger Source #

enumFrom :: SBV Day -> SList Day Source #

enumFromThen :: SBV Day -> SBV Day -> SList Day Source #

enumFromTo :: SBV Day -> SBV Day -> SList Day Source #

enumFromThenTo :: SBV Day -> SBV Day -> SBV Day -> SList Day 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 #

OrdSymbolic (SBV Day) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

(.<) :: SBV Day -> SBV Day -> SBool Source #

(.<=) :: SBV Day -> SBV Day -> SBool Source #

(.>) :: SBV Day -> SBV Day -> SBool Source #

(.>=) :: SBV Day -> SBV Day -> SBool Source #

smin :: SBV Day -> SBV Day -> SBV Day Source #

smax :: SBV Day -> SBV Day -> SBV Day Source #

inRange :: SBV Day -> (SBV Day, SBV Day) -> SBool Source #

HasInductionSchema (Forall ta Day -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Day -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type MetricSpace Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

type MetricSpace Day = Word8

cv2Day :: String -> [CV] -> Day Source #

Conversion from SMT values to Day values.

_undefiner_Day :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

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.

isMon :: SBV Day -> SBool Source #

Field recognizer predicate.

isTue :: SBV Day -> SBool Source #

Field recognizer predicate.

isWed :: SBV Day -> SBool Source #

Field recognizer predicate.

isThu :: SBV Day -> SBool Source #

Field recognizer predicate.

isFri :: SBV Day -> SBool Source #

Field recognizer predicate.

isSat :: SBV Day -> SBool Source #

Field recognizer predicate.

isSun :: SBV Day -> SBool Source #

Field recognizer predicate.

sCaseDay :: Mergeable result => SBV Day -> result -> result -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Day.

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