Symbolic version of the constructor Left.

Symbolic version of the constructor Right.

Construct an SEither a b from an Either (SBV a) (SBV b)

>>> liftEither (Left 3 :: Either SInteger SBool)
Left 3 :: Either Integer Bool
>>> liftEither (Right sTrue :: Either SInteger SBool)
Right True :: Either Integer Bool

Symbolic version of the type Either.

Declare a symbolic maybe.

Declare a symbolic maybe, unnamed.

Declare a list of symbolic maybes.

Case analysis for symbolic Eithers. If the value isLeft, apply the first function; if it isRight, apply the second function.

>>> either (*2) (*3) (sLeft (3 :: SInteger))
6 :: SInteger
>>> either (*2) (*3) (sRight (3 :: SInteger))
9 :: SInteger
>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> let g = uninterpret "g" :: SInteger -> SInteger
>>> prove $ \x -> either f g (sLeft x) .== f x
Q.E.D.
>>> prove $ \x -> either f g (sRight x) .== g x
Q.E.D.

Map over both sides of a symbolic Either at the same time

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> let g = uninterpret "g" :: SInteger -> SInteger
>>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x
Q.E.D.
>>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x
Q.E.D.

Map over the left side of an Either

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> prove $ \x -> first f (sLeft x :: SEither Integer Integer) .== sLeft (f x)
Q.E.D.
>>> prove $ \x -> first f (sRight x :: SEither Integer Integer) .== sRight x
Q.E.D.

Map over the right side of an Either

>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> prove $ \x -> second f (sRight x :: SEither Integer Integer) .== sRight (f x)
Q.E.D.
>>> prove $ \x -> second f (sLeft x :: SEither Integer Integer) .== sLeft x
Q.E.D.

Field recognizer predicate.

Field recognizer predicate.

Return the value from the left component. The behavior is undefined if passed a right value, i.e., it can return any value.

>>> fromLeft (sLeft (literal 'a') :: SEither Char Integer)
'a' :: SChar
>>> prove $ \x -> fromLeft (sLeft x :: SEither Char Integer) .== (x :: SChar)
Q.E.D.
>>> sat $ \x -> x .== (fromLeft (sRight 4 :: SEither Char Integer))
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.

Return the value from the right component. The behavior is undefined if passed a left value, i.e., it can return any value.

>>> fromRight (sRight (literal 'a') :: SEither Integer Char)
'a' :: SChar
>>> prove $ \x -> fromRight (sRight x :: SEither Char Integer) .== (x :: SInteger)
Q.E.D.
>>> sat $ \x -> x .== (fromRight (sLeft (literal 2) :: SEither Integer Char))
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.