Grisette.Core.Data.Class.Bool

Symbolic equality

class SEq a where

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

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

Instances

SEq Int16

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Int32

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Int64

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Int8

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Word16

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Word32

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Word64

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Word8

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq ByteString

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq AssertionError

Defined in Grisette.Core.Control.Exception

Methods

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

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

SEq VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

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

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

SEq Integer

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq ()

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Bool

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Char

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Int

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq Word

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq a => SEq (Identity a)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq a => SEq (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

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

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

SupportedPrim (IntN n) => SEq (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

SupportedPrim (WordN n) => SEq (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

SupportedPrim Integer => SEq (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SupportedPrim Bool => SEq (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SEq a => SEq (Maybe a)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq a => SEq [a]

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

(SEq e, SEq a) => SEq (Either e a)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

(/=~) :: Either e a -> Either e a -> SymBool

(SEq e, SEq a) => SEq (CBMCEither e a)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

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

(/=~) :: CBMCEither e a -> CBMCEither e a -> SymBool

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

(SEq a, SEq b) => SEq (a, b)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq (m (CBMCEither e a)) => SEq (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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

SEq (m a) => SEq (IdentityT m a)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

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

Defined in Grisette.Core.Data.Class.Bool

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

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

Defined in Grisette.Core.Data.Class.Bool

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

(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)

Defined in Grisette.Core.Data.Class.Bool

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

class SEq' f where

Auxiliary class for SEq instance derivation

Methods

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

Auxiliary function for '(==~~) derivation

Instances

SEq' (U1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

SEq' (V1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

Defined in Grisette.Core.Data.Class.Bool

Methods

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

Symbolic Boolean operations

class LogicalOp b where

Symbolic logical operators for symbolic booleans.

>>> let t = con True :: SymBool
>>> let f = con False :: SymBool
>>> let a = "a" :: SymBool
>>> let b = "b" :: SymBool
>>> t ||~ f
true
>>> a ||~ t
true
>>> a ||~ f
a
>>> a ||~ b
(|| a b)
>>> t &&~ f
false
>>> a &&~ t
a
>>> a &&~ f
false
>>> a &&~ b
(&& a b)
>>> nots t
false
>>> nots f
true
>>> nots a
(! a)
>>> t `xors` f
true
>>> t `xors` t
false
>>> a `xors` t
(! a)
>>> a `xors` f
a
>>> a `xors` b
(|| (&& (! a) b) (&& a (! b)))

Minimal complete definition

(||~), nots | (&&~), nots

Methods

(||~) :: b -> b -> b infixr 2

Symbolic disjunction

(&&~) :: b -> b -> b infixr 3

Symbolic conjunction

nots :: b -> b

Symbolic negation

xors :: b -> b -> b

Symbolic exclusive disjunction

implies :: b -> b -> b

Symbolic implication

Instances

LogicalOp Bool

Defined in Grisette.Core.Data.Class.Bool

Methods

(||~) :: Bool -> Bool -> Bool

(&&~) :: Bool -> Bool -> Bool

nots :: Bool -> Bool

xors :: Bool -> Bool -> Bool

implies :: Bool -> Bool -> Bool

(LogicalOp a, Mergeable a) => LogicalOp (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

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

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

nots :: UnionM a -> UnionM a

xors :: UnionM a -> UnionM a -> UnionM a

implies :: UnionM a -> UnionM a -> UnionM a

LogicalOp (Sym Bool)

Defined in Grisette.Core.Data.Class.Bool

Methods

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

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

nots :: Sym Bool -> Sym Bool

xors :: Sym Bool -> Sym Bool -> Sym Bool

implies :: Sym Bool -> Sym Bool -> Sym Bool

class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b

Aggregation for the operations on symbolic boolean types

Instances

SymBoolOp (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

class ITEOp v where

ITE operator for solvable (see Grisette.Core)s, including symbolic boolean, integer, etc.

>>> let a = "a" :: SymBool
>>> let b = "b" :: SymBool
>>> let c = "c" :: SymBool
>>> ites a b c
(ite a b c)

Methods

ites :: SymBool -> v -> v -> v

Instances

(ITEOp a, Mergeable a) => ITEOp (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

ites :: SymBool -> UnionM a -> UnionM a -> UnionM a

SupportedPrim a => ITEOp (Sym a)

Defined in Grisette.Core.Data.Class.Bool

Methods

ites :: SymBool -> Sym a -> Sym a -> Sym a