Maybe package:sbv

Symbolic option type, symbolic version of Haskell's Maybe type.

Case analysis for symbolic Maybes. If the value isNothing, return the default value; if it isJust, apply the function.

>>> sat $ \x -> x .== maybe 0 (`sMod` 2) (sJust (3 :: SInteger))
Satisfiable. Model:
s0 = 1 :: Integer

>>> sat $ \x -> x .== maybe 0 (`sMod` 2) (sNothing :: SMaybe Integer)
Satisfiable. Model:
s0 = 0 :: Integer

>>> let f = uninterpret "f" :: SInteger -> SBool

>>> prove $ \x d -> maybe d f (sJust x) .== f x
Q.E.D.

>>> prove $ \d -> maybe d f sNothing .== d
Q.E.D.

Symbolic version of the type Maybe.

Declare a symbolic maybe.

Declare a symbolic maybe, unnamed.

Declare a list of symbolic maybes.

Return the value of an optional value. The default is returned if Nothing. Compare to fromJust.

>>> fromMaybe 2 (sNothing :: SMaybe Integer)
2 :: SInteger

>>> sat $ \x -> fromMaybe 2 (sJust 5 :: SMaybe Integer) .== x
Satisfiable. Model:
s0 = 5 :: Integer

>>> prove $ \x -> fromMaybe x (sNothing :: SMaybe Integer) .== x
Q.E.D.

>>> prove $ \x -> fromMaybe (x+1) (sJust x :: SMaybe Integer) .== x
Q.E.D.

Construct an SMaybe a from a Maybe (SBV a).

>>> liftMaybe (Just (3 :: SInteger))
Just 3 :: Maybe Integer

>>> liftMaybe (Nothing :: Maybe SInteger)
Nothing :: Maybe Integer