Grisette.Core.Data.Class.SOrd

Symbolic total order relation

class SEq a => SOrd a where

Symbolic total order. Note that we can't use Haskell's Ord class since symbolic comparison won't necessarily return a concrete Bool or Ordering value.

>>> let a = 1 :: SymInteger
>>> let b = 2 :: SymInteger
>>> a <~ b
true
>>> a >~ b
false

>>> let a = "a" :: SymInteger
>>> let b = "b" :: SymInteger
>>> a <~ b
(< a b)
>>> a <=~ b
(<= a b)
>>> a >~ b
(< b a)
>>> a >=~ b
(<= b a)

For symCompare, Ordering is not a solvable type, and the result would be wrapped in a union-like monad. See UnionMBase and UnionLike for more information.

>>> a `symCompare` b :: UnionM Ordering -- UnionM is UnionMBase specialized with SymBool
{If (< a b) LT (If (= a b) EQ GT)}

Note: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ... deriving Generic deriving SOrd via (Default X)

Minimal complete definition

(<=~)

Methods

(<~) :: a -> a -> SymBool infix 4

(<=~) :: a -> a -> SymBool infix 4

(>~) :: a -> a -> SymBool infix 4

(>=~) :: a -> a -> SymBool infix 4

symCompare :: a -> a -> UnionM Ordering

Instances

SOrd Int16

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Int16 -> Int16 -> SymBool

(<=~) :: Int16 -> Int16 -> SymBool

(>~) :: Int16 -> Int16 -> SymBool

(>=~) :: Int16 -> Int16 -> SymBool

symCompare :: Int16 -> Int16 -> UnionM Ordering

SOrd Int32

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Int32 -> Int32 -> SymBool

(<=~) :: Int32 -> Int32 -> SymBool

(>~) :: Int32 -> Int32 -> SymBool

(>=~) :: Int32 -> Int32 -> SymBool

symCompare :: Int32 -> Int32 -> UnionM Ordering

SOrd Int64

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Int64 -> Int64 -> SymBool

(<=~) :: Int64 -> Int64 -> SymBool

(>~) :: Int64 -> Int64 -> SymBool

(>=~) :: Int64 -> Int64 -> SymBool

symCompare :: Int64 -> Int64 -> UnionM Ordering

SOrd Int8

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Int8 -> Int8 -> SymBool

(<=~) :: Int8 -> Int8 -> SymBool

(>~) :: Int8 -> Int8 -> SymBool

(>=~) :: Int8 -> Int8 -> SymBool

symCompare :: Int8 -> Int8 -> UnionM Ordering

SOrd Word16

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Word16 -> Word16 -> SymBool

(<=~) :: Word16 -> Word16 -> SymBool

(>~) :: Word16 -> Word16 -> SymBool

(>=~) :: Word16 -> Word16 -> SymBool

symCompare :: Word16 -> Word16 -> UnionM Ordering

SOrd Word32

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Word32 -> Word32 -> SymBool

(<=~) :: Word32 -> Word32 -> SymBool

(>~) :: Word32 -> Word32 -> SymBool

(>=~) :: Word32 -> Word32 -> SymBool

symCompare :: Word32 -> Word32 -> UnionM Ordering

SOrd Word64

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Word64 -> Word64 -> SymBool

(<=~) :: Word64 -> Word64 -> SymBool

(>~) :: Word64 -> Word64 -> SymBool

(>=~) :: Word64 -> Word64 -> SymBool

symCompare :: Word64 -> Word64 -> UnionM Ordering

SOrd Word8

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Word8 -> Word8 -> SymBool

(<=~) :: Word8 -> Word8 -> SymBool

(>~) :: Word8 -> Word8 -> SymBool

(>=~) :: Word8 -> Word8 -> SymBool

symCompare :: Word8 -> Word8 -> UnionM Ordering

SOrd ByteString

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: ByteString -> ByteString -> SymBool

(<=~) :: ByteString -> ByteString -> SymBool

(>~) :: ByteString -> ByteString -> SymBool

(>=~) :: ByteString -> ByteString -> SymBool

symCompare :: ByteString -> ByteString -> UnionM Ordering

SOrd AssertionError

Defined in Grisette.Core.Control.Exception

Methods

(<~) :: AssertionError -> AssertionError -> SymBool

(<=~) :: AssertionError -> AssertionError -> SymBool

(>~) :: AssertionError -> AssertionError -> SymBool

(>=~) :: AssertionError -> AssertionError -> SymBool

symCompare :: AssertionError -> AssertionError -> UnionM Ordering

SOrd VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

(<~) :: VerificationConditions -> VerificationConditions -> SymBool

(<=~) :: VerificationConditions -> VerificationConditions -> SymBool

(>~) :: VerificationConditions -> VerificationConditions -> SymBool

(>=~) :: VerificationConditions -> VerificationConditions -> SymBool

symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering

SOrd Integer

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Integer -> Integer -> SymBool

(<=~) :: Integer -> Integer -> SymBool

(>~) :: Integer -> Integer -> SymBool

(>=~) :: Integer -> Integer -> SymBool

symCompare :: Integer -> Integer -> UnionM Ordering

SOrd ()

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: () -> () -> SymBool

(<=~) :: () -> () -> SymBool

(>~) :: () -> () -> SymBool

(>=~) :: () -> () -> SymBool

symCompare :: () -> () -> UnionM Ordering

SOrd Bool

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Bool -> Bool -> SymBool

(<=~) :: Bool -> Bool -> SymBool

(>~) :: Bool -> Bool -> SymBool

(>=~) :: Bool -> Bool -> SymBool

symCompare :: Bool -> Bool -> UnionM Ordering

SOrd Char

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Char -> Char -> SymBool

(<=~) :: Char -> Char -> SymBool

(>~) :: Char -> Char -> SymBool

(>=~) :: Char -> Char -> SymBool

symCompare :: Char -> Char -> UnionM Ordering

SOrd Int

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Int -> Int -> SymBool

(<=~) :: Int -> Int -> SymBool

(>~) :: Int -> Int -> SymBool

(>=~) :: Int -> Int -> SymBool

symCompare :: Int -> Int -> UnionM Ordering

SOrd Word

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Word -> Word -> SymBool

(<=~) :: Word -> Word -> SymBool

(>~) :: Word -> Word -> SymBool

(>=~) :: Word -> Word -> SymBool

symCompare :: Word -> Word -> UnionM Ordering

SOrd a => SOrd (Identity a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Identity a -> Identity a -> SymBool

(<=~) :: Identity a -> Identity a -> SymBool

(>~) :: Identity a -> Identity a -> SymBool

(>=~) :: Identity a -> Identity a -> SymBool

symCompare :: Identity a -> Identity a -> UnionM Ordering

(SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Default a -> Default a -> SymBool

(<=~) :: Default a -> Default a -> SymBool

(>~) :: Default a -> Default a -> SymBool

(>=~) :: Default a -> Default a -> SymBool

symCompare :: Default a -> Default a -> UnionM Ordering

SOrd a => SOrd (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(<~) :: UnionM a -> UnionM a -> SymBool

(<=~) :: UnionM a -> UnionM a -> SymBool

(>~) :: UnionM a -> UnionM a -> SymBool

(>=~) :: UnionM a -> UnionM a -> SymBool

symCompare :: UnionM a -> UnionM a -> UnionM Ordering

SupportedPrim (IntN n) => SOrd (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering

SupportedPrim (WordN n) => SOrd (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering

SupportedPrim Integer => SOrd (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym Integer -> Sym Integer -> SymBool

(<=~) :: Sym Integer -> Sym Integer -> SymBool

(>~) :: Sym Integer -> Sym Integer -> SymBool

(>=~) :: Sym Integer -> Sym Integer -> SymBool

symCompare :: Sym Integer -> Sym Integer -> UnionM Ordering

SOrd (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym Bool -> Sym Bool -> SymBool

(<=~) :: Sym Bool -> Sym Bool -> SymBool

(>~) :: Sym Bool -> Sym Bool -> SymBool

(>=~) :: Sym Bool -> Sym Bool -> SymBool

symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering

SOrd a => SOrd (Maybe a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Maybe a -> Maybe a -> SymBool

(<=~) :: Maybe a -> Maybe a -> SymBool

(>~) :: Maybe a -> Maybe a -> SymBool

(>=~) :: Maybe a -> Maybe a -> SymBool

symCompare :: Maybe a -> Maybe a -> UnionM Ordering

SOrd a => SOrd [a]

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: [a] -> [a] -> SymBool

(<=~) :: [a] -> [a] -> SymBool

(>~) :: [a] -> [a] -> SymBool

(>=~) :: [a] -> [a] -> SymBool

symCompare :: [a] -> [a] -> UnionM Ordering

(SOrd a, SOrd b) => SOrd (Either a b)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Either a b -> Either a b -> SymBool

(<=~) :: Either a b -> Either a b -> SymBool

(>~) :: Either a b -> Either a b -> SymBool

(>=~) :: Either a b -> Either a b -> SymBool

symCompare :: Either a b -> Either a b -> UnionM Ordering

(SOrd a, SOrd b) => SOrd (CBMCEither a b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(<~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(<=~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(>~) :: CBMCEither a b -> CBMCEither a b -> SymBool

(>=~) :: CBMCEither a b -> CBMCEither a b -> SymBool

symCompare :: CBMCEither a b -> CBMCEither a b -> UnionM Ordering

SOrd (m (Maybe a)) => SOrd (MaybeT m a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: MaybeT m a -> MaybeT m a -> SymBool

(<=~) :: MaybeT m a -> MaybeT m a -> SymBool

(>~) :: MaybeT m a -> MaybeT m a -> SymBool

(>=~) :: MaybeT m a -> MaybeT m a -> SymBool

symCompare :: MaybeT m a -> MaybeT m a -> UnionM Ordering

(SOrd a, SOrd b) => SOrd (a, b)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b) -> (a, b) -> SymBool

(<=~) :: (a, b) -> (a, b) -> SymBool

(>~) :: (a, b) -> (a, b) -> SymBool

(>=~) :: (a, b) -> (a, b) -> SymBool

symCompare :: (a, b) -> (a, b) -> UnionM Ordering

SOrd (m (CBMCEither e a)) => SOrd (CBMCExceptT e m a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

(<~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(<=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(>~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

(>=~) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool

symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> UnionM Ordering

SOrd (m (Either e a)) => SOrd (ExceptT e m a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: ExceptT e m a -> ExceptT e m a -> SymBool

(<=~) :: ExceptT e m a -> ExceptT e m a -> SymBool

(>~) :: ExceptT e m a -> ExceptT e m a -> SymBool

(>=~) :: ExceptT e m a -> ExceptT e m a -> SymBool

symCompare :: ExceptT e m a -> ExceptT e m a -> UnionM Ordering

SOrd (m a) => SOrd (IdentityT m a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: IdentityT m a -> IdentityT m a -> SymBool

(<=~) :: IdentityT m a -> IdentityT m a -> SymBool

(>~) :: IdentityT m a -> IdentityT m a -> SymBool

(>=~) :: IdentityT m a -> IdentityT m a -> SymBool

symCompare :: IdentityT m a -> IdentityT m a -> UnionM Ordering

SOrd (m (a, s)) => SOrd (WriterT s m a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: WriterT s m a -> WriterT s m a -> SymBool

(<=~) :: WriterT s m a -> WriterT s m a -> SymBool

(>~) :: WriterT s m a -> WriterT s m a -> SymBool

(>=~) :: WriterT s m a -> WriterT s m a -> SymBool

symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering

SOrd (m (a, s)) => SOrd (WriterT s m a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: WriterT s m a -> WriterT s m a -> SymBool

(<=~) :: WriterT s m a -> WriterT s m a -> SymBool

(>~) :: WriterT s m a -> WriterT s m a -> SymBool

(>=~) :: WriterT s m a -> WriterT s m a -> SymBool

symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering

(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c) -> (a, b, c) -> SymBool

(<=~) :: (a, b, c) -> (a, b, c) -> SymBool

(>~) :: (a, b, c) -> (a, b, c) -> SymBool

(>=~) :: (a, b, c) -> (a, b, c) -> SymBool

symCompare :: (a, b, c) -> (a, b, c) -> UnionM Ordering

(SOrd (f a), SOrd (g a)) => SOrd (Sum f g a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: Sum f g a -> Sum f g a -> SymBool

(<=~) :: Sum f g a -> Sum f g a -> SymBool

(>~) :: Sum f g a -> Sum f g a -> SymBool

(>=~) :: Sum f g a -> Sum f g a -> SymBool

symCompare :: Sum f g a -> Sum f g a -> UnionM Ordering

(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

(<=~) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

(>~) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

(>=~) :: (a, b, c, d) -> (a, b, c, d) -> SymBool

symCompare :: (a, b, c, d) -> (a, b, c, d) -> UnionM Ordering

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

(<=~) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

(>~) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

(>=~) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SymBool

symCompare :: (a, b, c, d, e) -> (a, b, c, d, e) -> UnionM Ordering

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

(<=~) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

(>~) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

(>=~) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SymBool

symCompare :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> UnionM Ordering

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

(<=~) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

(>~) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

(>=~) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SymBool

symCompare :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> UnionM Ordering

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g, SOrd h) => SOrd (a, b, c, d, e, f, g, h)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

(<=~) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

(>~) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

(>=~) :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> SymBool

symCompare :: (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> UnionM Ordering

class SEq' f => SOrd' f where

Auxiliary class for SOrd instance derivation

Methods

(<~~) :: f a -> f a -> SymBool infix 4

Auxiliary function for '(<~~) derivation

(<=~~) :: f a -> f a -> SymBool infix 4

Auxiliary function for '(<=~~) derivation

(>~~) :: f a -> f a -> SymBool infix 4

Auxiliary function for '(>~~) derivation

(>=~~) :: f a -> f a -> SymBool infix 4

Auxiliary function for '(>=~~) derivation

symCompare' :: f a -> f a -> UnionM Ordering

Auxiliary function for symCompare derivation

Instances

SOrd' (U1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: U1 a -> U1 a -> SymBool

(<=~~) :: U1 a -> U1 a -> SymBool

(>~~) :: U1 a -> U1 a -> SymBool

(>=~~) :: U1 a -> U1 a -> SymBool

symCompare' :: U1 a -> U1 a -> UnionM Ordering

SOrd' (V1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: V1 a -> V1 a -> SymBool

(<=~~) :: V1 a -> V1 a -> SymBool

(>~~) :: V1 a -> V1 a -> SymBool

(>=~~) :: V1 a -> V1 a -> SymBool

symCompare' :: V1 a -> V1 a -> UnionM Ordering

(SOrd' a, SOrd' b) => SOrd' (a :*: b)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: (a :*: b) a0 -> (a :*: b) a0 -> SymBool

(<=~~) :: (a :*: b) a0 -> (a :*: b) a0 -> SymBool

(>~~) :: (a :*: b) a0 -> (a :*: b) a0 -> SymBool

(>=~~) :: (a :*: b) a0 -> (a :*: b) a0 -> SymBool

symCompare' :: (a :*: b) a0 -> (a :*: b) a0 -> UnionM Ordering

(SOrd' a, SOrd' b) => SOrd' (a :+: b)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool

(<=~~) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool

(>~~) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool

(>=~~) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool

symCompare' :: (a :+: b) a0 -> (a :+: b) a0 -> UnionM Ordering

SOrd c => SOrd' (K1 i c :: Type -> Type)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: K1 i c a -> K1 i c a -> SymBool

(<=~~) :: K1 i c a -> K1 i c a -> SymBool

(>~~) :: K1 i c a -> K1 i c a -> SymBool

(>=~~) :: K1 i c a -> K1 i c a -> SymBool

symCompare' :: K1 i c a -> K1 i c a -> UnionM Ordering

SOrd' a => SOrd' (M1 i c a)

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~~) :: M1 i c a a0 -> M1 i c a a0 -> SymBool

(<=~~) :: M1 i c a a0 -> M1 i c a a0 -> SymBool

(>~~) :: M1 i c a a0 -> M1 i c a a0 -> SymBool

(>=~~) :: M1 i c a a0 -> M1 i c a a0 -> SymBool

symCompare' :: M1 i c a a0 -> M1 i c a a0 -> UnionM Ordering