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 | Safe-Inferred |
Language | Haskell2010 |
Documentation
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)
Instances
ITEOp SymBool Source # | |
ITEOp SymInteger Source # | |
Defined in Grisette.Internal.Core.Data.Class.ITEOp symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source # | |
(ITEOp a, Mergeable a) => ITEOp (UnionM a) Source # | |
(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n)) => ITEOp (SomeBV bv) Source # | |
(KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source # | |
(KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source # | |
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb) Source # | |
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb) Source # | |