grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.SOrd

Description

 
Synopsis

Symbolic total order relation

class SEq a => SOrd a where Source #

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 Source #

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

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

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

symCompare :: a -> a -> UnionM Ordering Source #

Instances

Instances details
SOrd Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SOrd VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SOrd SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd () Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

(>~) :: () -> () -> SymBool Source #

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

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

SOrd Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd a => SOrd (Identity a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

(SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd a => SOrd (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

(KnownNat n, 1 <= n) => SOrd (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: IntN n -> IntN n -> SymBool Source #

(<=~) :: IntN n -> IntN n -> SymBool Source #

(>~) :: IntN n -> IntN n -> SymBool Source #

(>=~) :: IntN n -> IntN n -> SymBool Source #

symCompare :: IntN n -> IntN n -> UnionM Ordering Source #

(KnownNat n, 1 <= n) => SOrd (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

(KnownNat n, 1 <= n) => SOrd (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(KnownNat n, 1 <= n) => SOrd (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd a => SOrd (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd a => SOrd [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b) => SOrd (Either a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b) => SOrd (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

SOrd (m (Maybe a)) => SOrd (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b) => SOrd (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd (m (CBMCEither e a)) => SOrd (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

SOrd (m (Either e a)) => SOrd (ExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd (m a) => SOrd (IdentityT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SOrd (m (a, s)) => SOrd (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd (m (a, s)) => SOrd (WriterT s m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd (f a), SOrd (g a)) => SOrd (Sum f g a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(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) Source # 
Instance details

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 Source #

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

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

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

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

class SEq' f => SOrd' f where Source #

Auxiliary class for SOrd instance derivation

Methods

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

Auxiliary function for '(<~~) derivation

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

Auxiliary function for '(<=~~) derivation

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

Auxiliary function for '(>~~) derivation

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

Auxiliary function for '(>=~~) derivation

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

Auxiliary function for symCompare derivation

Instances

Instances details
SOrd' (U1 :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd' (V1 :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd' a, SOrd' b) => SOrd' (a :*: b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

(SOrd' a, SOrd' b) => SOrd' (a :+: b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd c => SOrd' (K1 i c :: Type -> Type) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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

SOrd' a => SOrd' (M1 i c a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

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

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

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

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

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