Symbolic version of the constructor Just.

Symbolic version of the constructor Nothing.

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

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

Symbolic version of the type Maybe.

Declare a symbolic maybe.

Declare a symbolic maybe, unnamed.

Declare a list of symbolic maybes.

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.

Map over the Just side of a Maybe.

>>> prove $ \x -> fromJust (map (+1) (sJust x)) .== x+(1::SInteger)
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

Map over two maybe values.

Field recognizer predicate.

Field recognizer predicate.

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.

Return the value of an optional value. The behavior is undefined if passed Nothing, i.e., it can return any value. Compare to fromMaybe.

>>> sat $ \x -> fromJust (sJust (literal 'a')) .== x
Satisfiable. Model:
  s0 = 'a' :: Char
>>> prove $ \x -> fromJust (sJust x) .== (x :: SChar)
Q.E.D.
>>> sat $ \x -> x .== (fromJust sNothing :: SChar)
Satisfiable. Model:
  s0 = 'A' :: 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.