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.Bool

Description

 
Synopsis

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

SEq Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SEq VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SEq SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SEq SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SEq SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SEq SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SEq SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SEq Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

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

SEq Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

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

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

Defined in Grisette.Core.Data.Class.Bool

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

Defined in Grisette.Core.Data.Class.Bool

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

ITEOp SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

ITEOp SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

ITEOp SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

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