Data.SBV.Maybe

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

Constructing optional values

sJust :: forall a. SymVal a => SBV a -> SMaybe a

Construct an SMaybe a from an SBV a

>>> sJust 3
Just 3 :: SMaybe Integer

sNothing :: forall a. SymVal a => SMaybe a

The symbolic Nothing

>>> sNothing :: SMaybe Integer
Nothing :: SMaybe Integer

liftMaybe :: SymVal a => Maybe (SBV a) -> SMaybe a

Construct an SMaybe a from a Maybe (SBV a)

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

Destructing optionals

maybe :: forall a b. (SymVal a, SymVal b) => SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b

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

>>> maybe 0 (`sMod` 2) (sJust (3 :: SInteger))
1 :: SInteger
>>> maybe 0 (`sMod` 2) (sNothing :: SMaybe Integer)
0 :: SInteger
>>> 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.

Mapping functions

map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SMaybe a -> SMaybe b

Map over the Just side of a Maybe

>>> prove $ \x -> fromJust (map (+1) (sJust x)) .== x+1
Q.E.D.
>>> let f = uninterpret "f" :: SInteger -> SBool
>>> prove $ \x -> map f (sJust x) .== sJust (f x)
Q.E.D.
>>> map f sNothing .== sNothing
True

Scrutinizing the branches of an option

isNothing :: SymVal a => SMaybe a -> SBool

Check if the symbolic value is nothing.

>>> isNothing (sNothing :: SMaybe Integer)
True
>>> isNothing (sJust (literal "nope"))
False

isJust :: SymVal a => SMaybe a -> SBool

Check if the symbolic value is not nothing.

>>> isJust (sNothing :: SMaybe Integer)
False
>>> isJust (sJust (literal "yep"))
True
>>> prove $ \x -> isJust (sJust (x :: SInteger))
Q.E.D.

fromMaybe :: SymVal a => SBV a -> SMaybe a -> SBV a

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

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

fromJust :: forall a. SymVal a => SMaybe a -> SBV a

Return the value of an optional value. The behavior is undefined if passed Nothing. Compare to fromMaybe.

>>> fromJust (sJust (literal 'a'))
'a' :: SChar
>>> prove $ \x -> fromJust (sJust x) .== (x :: SChar)
Q.E.D.
>>> sat $ \x -> x .== (fromJust sNothing :: SChar)
Satisfiable. Model:
  s0 = '\NUL' :: Char

Note how we get a satisfying assignment in the last case: The behavior is unspecified, thus the SMT solver picks whatever satisfies the constraints, if there is one.