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	None
Language	Haskell2010

Grisette.Internal.Core.Data.Class.ITEOp

Description

Synopsis

class ITEOp v where
- symIte :: SymBool -> v -> v -> v

Documentation

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
>>> symIte a b c
(ite a b c)

Methods

symIte :: SymBool -> v -> v -> v Source #

Symbolic if-then-else.

Instances

Instances details

ITEOp SymAlgReal Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #
ITEOp SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymBool -> SymBool -> SymBool Source #
ITEOp SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #
ITEOp SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source #
SimpleMergeable a => ITEOp a Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable Methods symIte :: SymBool -> a -> a -> a Source #
ITEOp v => ITEOp (Identity v) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> Identity v -> Identity v -> Identity v Source #
ITEOp a => ITEOp (AsKey a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> AsKey a -> AsKey a -> AsKey a Source #
Mergeable a => ITEOp (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods symIte :: SymBool -> Union a -> Union a -> Union a Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => ITEOp (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
(KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
ITEOp (Proxy a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> Proxy a -> Proxy a -> Proxy a Source #
ITEOp (a --> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> (a --> b) -> (a --> b) -> a --> b Source #
ValidFP eb sb => ITEOp (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #
ITEOp (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb Source #
ITEOp (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb Source #