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

Grisette.Internal.Core.Data.Class.LogicalOp

Description

Synopsis

class LogicalOp b where
- true :: b
- false :: b
- (.||) :: b -> b -> b
- (.&&) :: b -> b -> b
- symNot :: b -> b
- symXor :: b -> b -> b
- symImplies :: b -> b -> b

Documentation

class LogicalOp b where Source #

Symbolic logical operators for symbolic booleans.

>>> let t = true :: SymBool
>>> let f = 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

(true | false), ((.||), symNot | (.&&), symNot)

Methods

true :: b Source #

Constant true

false :: b Source #

Constant false

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

Symbolic disjunction

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

Symbolic conjunction

symNot :: b -> b Source #

Symbolic negation

symXor :: b -> b -> b Source #

Symbolic exclusive disjunction

symImplies :: b -> b -> b Source #

Symbolic implication

Instances

Instances details

LogicalOp SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.LogicalOp Methods true :: SymBool Source # false :: SymBool Source # (.\|\|) :: SymBool -> SymBool -> SymBool Source # (.&&) :: SymBool -> SymBool -> SymBool Source # symNot :: SymBool -> SymBool Source # symXor :: SymBool -> SymBool -> SymBool Source # symImplies :: SymBool -> SymBool -> SymBool Source #
LogicalOp Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.LogicalOp Methods true :: Bool Source # false :: Bool Source # (.\|\|) :: Bool -> Bool -> Bool Source # (.&&) :: Bool -> Bool -> Bool Source # symNot :: Bool -> Bool Source # symXor :: Bool -> Bool -> Bool Source # symImplies :: Bool -> Bool -> Bool Source #
LogicalOp a => LogicalOp (Identity a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.LogicalOp Methods true :: Identity a Source # false :: Identity a Source # (.\|\|) :: Identity a -> Identity a -> Identity a Source # (.&&) :: Identity a -> Identity a -> Identity a Source # symNot :: Identity a -> Identity a Source # symXor :: Identity a -> Identity a -> Identity a Source # symImplies :: Identity a -> Identity a -> Identity a Source #
LogicalOp a => LogicalOp (AsKey a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.LogicalOp Methods true :: AsKey a Source # false :: AsKey a Source # (.\|\|) :: AsKey a -> AsKey a -> AsKey a Source # (.&&) :: AsKey a -> AsKey a -> AsKey a Source # symNot :: AsKey a -> AsKey a Source # symXor :: AsKey a -> AsKey a -> AsKey a Source # symImplies :: AsKey a -> AsKey a -> AsKey a Source #
(LogicalOp a, Mergeable a) => LogicalOp (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods true :: Union a Source # false :: Union a Source # (.\|\|) :: Union a -> Union a -> Union a Source # (.&&) :: Union a -> Union a -> Union a Source # symNot :: Union a -> Union a Source # symXor :: Union a -> Union a -> Union a Source # symImplies :: Union a -> Union a -> Union a Source #