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 | Trustworthy |
Language | Haskell2010 |
Grisette.Core.Data.Class.Integer
Contents
Description
Synopsis
- data ArithException
- class SignedDivMod a where
- divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class UnsignedDivMod a where
- udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class SignedQuotRem a where
- quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a
Symbolic integer operations
data ArithException #
Arithmetic exceptions.
Constructors
Overflow | |
Underflow | |
LossOfPrecision | |
DivideByZero | |
Denormal | |
RatioZeroDenominator | Since: base-4.6.0.0 |
Instances
class SignedDivMod a where Source #
Safe signed div
and mod
with monadic error handling in multi-path
execution. These procedures show throw DivideByZero
exception when the
divisor is zero. The result should be able to handle errors with
MonadError
, and the error type should be compatible with ArithException
(see TransformError
for more details).
Methods
divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
Safe signed div
with monadic error handling in multi-path execution.
>>>
divs (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger
ExceptT {If (= b 0) (Left AssertionError) (Right (div a b))}
mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
Safe signed mod
with monadic error handling in multi-path execution.
>>>
mods (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymInteger
ExceptT {If (= b 0) (Left AssertionError) (Right (mod a b))}
Instances
SignedDivMod (Sym Integer) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim Methods divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source # mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source # |
class UnsignedDivMod a where Source #
Safe unsigned div
and mod
with monadic error handling in multi-path
execution. These procedures show throw DivideByZero
exception when the
divisor is zero. The result should be able to handle errors with
MonadError
, and the error type should be compatible with ArithException
(see TransformError
for more details).
Methods
udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
class SignedQuotRem a where Source #
Safe signed quot
and rem
with monadic error handling in multi-path
execution. These procedures show throw DivideByZero
exception when the
divisor is zero. The result should be able to handle errors with
MonadError
, and the error type should be compatible with ArithException
(see TransformError
for more details).
Methods
quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a Source #
Aggregation for the operations on symbolic integer types
Instances
SymIntegerOp (Sym Integer) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim |