Grisette.Internal.Core.Data.Class.ITEOp

Documentation

class ITEOp v where

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

Symbolic if-then-else.

Instances

ITEOp SymAlgReal

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal

ITEOp SymBool

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymBool -> SymBool -> SymBool

ITEOp SymFPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode

ITEOp SymInteger

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

ITEOp v => ITEOp (Identity v)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> Identity v -> Identity v -> Identity v

(ITEOp a, Mergeable a) => ITEOp (Union a)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

symIte :: SymBool -> Union a -> Union a -> Union a

(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => ITEOp (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv

(KnownNat n, 1 <= n) => ITEOp (SymIntN n)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => ITEOp (SymWordN n)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

ValidFP eb sb => ITEOp (SymFP eb sb)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb)

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb