Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SEq

Contents

Symbolic equality

Description

Synopsis

class SEq a where
- (.==) :: a -> a -> SymBool
- (./=) :: a -> a -> SymBool
class SEq' f where
- (..==) :: f a -> f a -> SymBool

Symbolic equality

class SEq a where Source #

Symbolic equality. Note that we can't use Haskell's Eq class since symbolic comparison won't necessarily return a concrete Bool value.

>>> let a = 1 :: SymInteger
>>> let b = 2 :: SymInteger
>>> a .== b
false
>>> a ./= b
true

>>> let a = "a" :: SymInteger
>>> let b = "b" :: SymInteger
>>> a ./= b
(! (= a b))
>>> a ./= b
(! (= a b))

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

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

Minimal complete definition

(.==) | (./=)

Methods

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

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

Instances

Instances details

SEq Int16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Int16 -> Int16 -> SymBool Source # (./=) :: Int16 -> Int16 -> SymBool Source #
SEq Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Int32 -> Int32 -> SymBool Source # (./=) :: Int32 -> Int32 -> SymBool Source #
SEq Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Int64 -> Int64 -> SymBool Source # (./=) :: Int64 -> Int64 -> SymBool Source #
SEq Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Int8 -> Int8 -> SymBool Source # (./=) :: Int8 -> Int8 -> SymBool Source #
SEq Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Word16 -> Word16 -> SymBool Source # (./=) :: Word16 -> Word16 -> SymBool Source #
SEq Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Word32 -> Word32 -> SymBool Source # (./=) :: Word32 -> Word32 -> SymBool Source #
SEq Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Word64 -> Word64 -> SymBool Source # (./=) :: Word64 -> Word64 -> SymBool Source #
SEq Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Word8 -> Word8 -> SymBool Source # (./=) :: Word8 -> Word8 -> SymBool Source #
SEq ByteString Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: ByteString -> ByteString -> SymBool Source # (./=) :: ByteString -> ByteString -> SymBool Source #
SEq AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: AssertionError -> AssertionError -> SymBool Source # (./=) :: AssertionError -> AssertionError -> SymBool Source #
SEq VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: VerificationConditions -> VerificationConditions -> SymBool Source # (./=) :: VerificationConditions -> VerificationConditions -> SymBool Source #
SEq SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymBool -> SymBool -> SymBool Source # (./=) :: SymBool -> SymBool -> SymBool Source #
SEq SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymInteger -> SymInteger -> SymBool Source # (./=) :: SymInteger -> SymInteger -> SymBool Source #
SEq Text Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Text -> Text -> SymBool Source # (./=) :: Text -> Text -> SymBool Source #
SEq Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Integer -> Integer -> SymBool Source # (./=) :: Integer -> Integer -> SymBool Source #
SEq () Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: () -> () -> SymBool Source # (./=) :: () -> () -> SymBool Source #
SEq Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Bool -> Bool -> SymBool Source # (./=) :: Bool -> Bool -> SymBool Source #
SEq Char Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Char -> Char -> SymBool Source # (./=) :: Char -> Char -> SymBool Source #
SEq Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Int -> Int -> SymBool Source # (./=) :: Int -> Int -> SymBool Source #
SEq Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Word -> Word -> SymBool Source # (./=) :: Word -> Word -> SymBool Source #
SEq a => SEq (Identity a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Identity a -> Identity a -> SymBool Source # (./=) :: Identity a -> Identity a -> SymBool Source #
(Generic a, SEq' (Rep a)) => SEq (Default a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Default a -> Default a -> SymBool Source # (./=) :: Default a -> Default a -> SymBool Source #
(Mergeable a, SEq a) => SEq (UnionM a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods (.==) :: UnionM a -> UnionM a -> SymBool Source # (./=) :: UnionM a -> UnionM a -> SymBool Source #
(KnownNat n, 1 <= n) => SEq (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: IntN n -> IntN n -> SymBool Source # (./=) :: IntN n -> IntN n -> SymBool Source #
(KnownNat n, 1 <= n) => SEq (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: WordN n -> WordN n -> SymBool Source # (./=) :: WordN n -> WordN n -> SymBool Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.==) :: SomeBV bv -> SomeBV bv -> SymBool Source # (./=) :: SomeBV bv -> SomeBV bv -> SymBool Source #
(KnownNat n, 1 <= n) => SEq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymIntN n -> SymIntN n -> SymBool Source # (./=) :: SymIntN n -> SymIntN n -> SymBool Source #
(KnownNat n, 1 <= n) => SEq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymWordN n -> SymWordN n -> SymBool Source # (./=) :: SymWordN n -> SymWordN n -> SymBool Source #
SEq a => SEq (Maybe a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Maybe a -> Maybe a -> SymBool Source # (./=) :: Maybe a -> Maybe a -> SymBool Source #
SEq a => SEq [a] Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: [a] -> [a] -> SymBool Source # (./=) :: [a] -> [a] -> SymBool Source #
(SEq e, SEq a) => SEq (Either e a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Either e a -> Either e a -> SymBool Source # (./=) :: Either e a -> Either e a -> SymBool Source #
(SEq e, SEq a) => SEq (CBMCEither e a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods (.==) :: CBMCEither e a -> CBMCEither e a -> SymBool Source # (./=) :: CBMCEither e a -> CBMCEither e a -> SymBool Source #
SEq (m (Maybe a)) => SEq (MaybeT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: MaybeT m a -> MaybeT m a -> SymBool Source # (./=) :: MaybeT m a -> MaybeT m a -> SymBool Source #
(SEq a, SEq b) => SEq (a, b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: (a, b) -> (a, b) -> SymBool Source # (./=) :: (a, b) -> (a, b) -> SymBool Source #
SEq (m (CBMCEither e a)) => SEq (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods (.==) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (./=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source #
SEq (m (Either e a)) => SEq (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: ExceptT e m a -> ExceptT e m a -> SymBool Source # (./=) :: ExceptT e m a -> ExceptT e m a -> SymBool Source #
SEq (m a) => SEq (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: IdentityT m a -> IdentityT m a -> SymBool Source # (./=) :: IdentityT m a -> IdentityT m a -> SymBool Source #
SEq (m (a, s)) => SEq (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: WriterT s m a -> WriterT s m a -> SymBool Source # (./=) :: WriterT s m a -> WriterT s m a -> SymBool Source #
SEq (m (a, s)) => SEq (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: WriterT s m a -> WriterT s m a -> SymBool Source # (./=) :: WriterT s m a -> WriterT s m a -> SymBool Source #
(SEq a, SEq b, SEq c) => SEq (a, b, c) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: (a, b, c) -> (a, b, c) -> SymBool Source # (./=) :: (a, b, c) -> (a, b, c) -> SymBool Source #
(SEq (f a), SEq (g a)) => SEq (Sum f g a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: Sum f g a -> Sum f g a -> SymBool Source # (./=) :: Sum f g a -> Sum f g a -> SymBool Source #
(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source # (./=) :: (a, b, c, d) -> (a, b, c, d) -> SymBool Source #
(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq 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 #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq 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 #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq 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 #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g, SEq h) => SEq (a, b, c, d, e, f, g, h) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq 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 #

class SEq' f where Source #

Auxiliary class for SEq instance derivation

Methods

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

Auxiliary function for '(..==) derivation

Instances

Instances details

SEq' (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: U1 a -> U1 a -> SymBool Source #
SEq' (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: V1 a -> V1 a -> SymBool Source #
(SEq' a, SEq' b) => SEq' (a :*: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source #
(SEq' a, SEq' b) => SEq' (a :+: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source #
SEq c => SEq' (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: K1 i c a -> K1 i c a -> SymBool Source #
SEq' a => SEq' (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (..==) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source #