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.Core.Data.Class.Bool

Contents

Symbolic equality
Symbolic Boolean operations

Description

Synopsis

class SEq a where
- (==~) :: a -> a -> SymBool
- (/=~) :: a -> a -> SymBool
class SEq' f where
- (==~~) :: f a -> f a -> SymBool
class LogicalOp b where
- (||~) :: b -> b -> b
- (&&~) :: b -> b -> b
- nots :: b -> b
- xors :: b -> b -> b
- implies :: b -> b -> b
class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b
class ITEOp v where
- ites :: SymBool -> v -> v -> v

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.Core.Data.Class.Bool Methods (==~) :: Int16 -> Int16 -> SymBool Source # (/=~) :: Int16 -> Int16 -> SymBool Source #
SEq Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Int32 -> Int32 -> SymBool Source # (/=~) :: Int32 -> Int32 -> SymBool Source #
SEq Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Int64 -> Int64 -> SymBool Source # (/=~) :: Int64 -> Int64 -> SymBool Source #
SEq Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Int8 -> Int8 -> SymBool Source # (/=~) :: Int8 -> Int8 -> SymBool Source #
SEq Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Word16 -> Word16 -> SymBool Source # (/=~) :: Word16 -> Word16 -> SymBool Source #
SEq Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Word32 -> Word32 -> SymBool Source # (/=~) :: Word32 -> Word32 -> SymBool Source #
SEq Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Word64 -> Word64 -> SymBool Source # (/=~) :: Word64 -> Word64 -> SymBool Source #
SEq Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Word8 -> Word8 -> SymBool Source # (/=~) :: Word8 -> Word8 -> SymBool Source #
SEq ByteString Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: ByteString -> ByteString -> SymBool Source # (/=~) :: ByteString -> ByteString -> SymBool Source #
SEq AssertionError Source #
Instance details Defined in Grisette.Core.Control.Exception Methods (==~) :: AssertionError -> AssertionError -> SymBool Source # (/=~) :: AssertionError -> AssertionError -> SymBool Source #
SEq VerificationConditions Source #
Instance details Defined in Grisette.Core.Control.Exception Methods (==~) :: VerificationConditions -> VerificationConditions -> SymBool Source # (/=~) :: VerificationConditions -> VerificationConditions -> SymBool Source #
SEq SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: SomeIntN -> SomeIntN -> SymBool Source # (/=~) :: SomeIntN -> SomeIntN -> SymBool Source #
SEq SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: SomeWordN -> SomeWordN -> SymBool Source # (/=~) :: SomeWordN -> SomeWordN -> SymBool Source #
SEq SomeSymIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (==~) :: SomeSymIntN -> SomeSymIntN -> SymBool Source # (/=~) :: SomeSymIntN -> SomeSymIntN -> SymBool Source #
SEq SomeSymWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (==~) :: SomeSymWordN -> SomeSymWordN -> SymBool Source # (/=~) :: SomeSymWordN -> SomeSymWordN -> SymBool Source #
SEq SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (==~) :: SymBool -> SymBool -> SymBool Source # (/=~) :: SymBool -> SymBool -> SymBool Source #
SEq SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (==~) :: SymInteger -> SymInteger -> SymBool Source # (/=~) :: SymInteger -> SymInteger -> SymBool Source #
SEq Integer Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Integer -> Integer -> SymBool Source # (/=~) :: Integer -> Integer -> SymBool Source #
SEq () Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: () -> () -> SymBool Source # (/=~) :: () -> () -> SymBool Source #
SEq Bool Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Bool -> Bool -> SymBool Source # (/=~) :: Bool -> Bool -> SymBool Source #
SEq Char Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Char -> Char -> SymBool Source # (/=~) :: Char -> Char -> SymBool Source #
SEq Int Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Int -> Int -> SymBool Source # (/=~) :: Int -> Int -> SymBool Source #
SEq Word Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Word -> Word -> SymBool Source # (/=~) :: Word -> Word -> SymBool Source #
SEq a => SEq (Identity a) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool 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.Core.Data.Class.Bool Methods (==~) :: Default a -> Default a -> SymBool Source # (/=~) :: Default a -> Default a -> SymBool Source #
SEq a => SEq (UnionM a) Source #
Instance details Defined in Grisette.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.Core.Data.Class.Bool 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.Core.Data.Class.Bool Methods (==~) :: WordN n -> WordN n -> SymBool Source # (/=~) :: WordN n -> WordN n -> SymBool Source #
(KnownNat n, 1 <= n) => SEq (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim 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.IR.SymPrim.Data.SymPrim Methods (==~) :: SymWordN n -> SymWordN n -> SymBool Source # (/=~) :: SymWordN n -> SymWordN n -> SymBool Source #
SEq a => SEq (Maybe a) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: Maybe a -> Maybe a -> SymBool Source # (/=~) :: Maybe a -> Maybe a -> SymBool Source #
SEq a => SEq [a] Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: [a] -> [a] -> SymBool Source # (/=~) :: [a] -> [a] -> SymBool Source #
(SEq e, SEq a) => SEq (Either e a) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool 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.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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool 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.Core.Data.Class.Bool Methods (==~~) :: U1 a -> U1 a -> SymBool Source #
SEq' (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~~) :: V1 a -> V1 a -> SymBool Source #
(SEq' a, SEq' b) => SEq' (a :*: b) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~~) :: (a :: b) a0 -> (a :: b) a0 -> SymBool Source #
(SEq' a, SEq' b) => SEq' (a :+: b) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~~) :: (a :+: b) a0 -> (a :+: b) a0 -> SymBool Source #
SEq c => SEq' (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~~) :: K1 i c a -> K1 i c a -> SymBool Source #
SEq' a => SEq' (M1 i c a) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~~) :: M1 i c a a0 -> M1 i c a a0 -> SymBool Source #

Symbolic Boolean operations

class LogicalOp b where Source #

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

Symbolic disjunction

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

Symbolic conjunction

nots :: b -> b Source #

Symbolic negation

xors :: b -> b -> b Source #

Symbolic exclusive disjunction

implies :: b -> b -> b Source #

Symbolic implication

Instances

Instances details

LogicalOp SymBool Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (\|\|~) :: SymBool -> SymBool -> SymBool Source # (&&~) :: SymBool -> SymBool -> SymBool Source # nots :: SymBool -> SymBool Source # xors :: SymBool -> SymBool -> SymBool Source # implies :: SymBool -> SymBool -> SymBool Source #
LogicalOp Bool Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (\|\|~) :: Bool -> Bool -> Bool Source # (&&~) :: Bool -> Bool -> Bool Source # nots :: Bool -> Bool Source # xors :: Bool -> Bool -> Bool Source # implies :: Bool -> Bool -> Bool Source #
(LogicalOp a, Mergeable a) => LogicalOp (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods (\|\|~) :: UnionM a -> UnionM a -> UnionM a Source # (&&~) :: UnionM a -> UnionM a -> UnionM a Source # nots :: UnionM a -> UnionM a Source # xors :: UnionM a -> UnionM a -> UnionM a Source # implies :: UnionM a -> UnionM a -> UnionM a Source #

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

Aggregation for the operations on symbolic boolean types

class ITEOp v where Source #

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

Instances

Instances details

ITEOp SomeSymIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN Source #
ITEOp SomeSymWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN Source #
ITEOp SymBool Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SymBool -> SymBool -> SymBool Source #
ITEOp SymInteger Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SymInteger -> SymInteger -> SymInteger Source #
(ITEOp a, Mergeable a) => ITEOp (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods ites :: SymBool -> UnionM a -> UnionM a -> UnionM a Source #
(KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb Source #