Grisette.Core.Data.Class.LogicalOp

Documentation

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)
>>> symNot t
false
>>> symNot f
true
>>> symNot a
(! a)
>>> t `symXor` f
true
>>> t `symXor` t
false
>>> a `symXor` t
(! a)
>>> a `symXor` f
a
>>> a `symXor` b
(|| (&& (! a) b) (&& a (! b)))

Minimal complete definition

(.||), symNot | (.&&), symNot

Methods

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

Symbolic disjunction

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

Symbolic conjunction

symNot :: b -> b

Symbolic negation

symXor :: b -> b -> b

Symbolic exclusive disjunction

symImplies :: b -> b -> b

Symbolic implication

Instances

LogicalOp SymBool

Defined in Grisette.Core.Data.Class.LogicalOp

Methods

(.||) :: SymBool -> SymBool -> SymBool

(.&&) :: SymBool -> SymBool -> SymBool

symNot :: SymBool -> SymBool

symXor :: SymBool -> SymBool -> SymBool

symImplies :: SymBool -> SymBool -> SymBool

LogicalOp Bool

Defined in Grisette.Core.Data.Class.LogicalOp

Methods

(.||) :: Bool -> Bool -> Bool

(.&&) :: Bool -> Bool -> Bool

symNot :: Bool -> Bool

symXor :: Bool -> Bool -> Bool

symImplies :: 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

symNot :: UnionM a -> UnionM a

symXor :: UnionM a -> UnionM a -> UnionM a

symImplies :: UnionM a -> UnionM a -> UnionM a