grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.SafeArith

Description

 
Synopsis

Symbolic integer operations

data ArithException #

Arithmetic exceptions.

Instances

Instances details
Exception ArithException

Since: base-4.0.0.0

Instance details

Defined in GHC.Exception.Type

Show ArithException

Since: base-4.0.0.0

Instance details

Defined in GHC.Exception.Type

Eq ArithException

Since: base-3.0

Instance details

Defined in GHC.Exception.Type

Ord ArithException

Since: base-3.0

Instance details

Defined in GHC.Exception.Type

Mergeable ArithException Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

TransformError ArithException AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SafeDivision ArithException Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

SafeDivision ArithException Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #

SafeDivision ArithException Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SafeLinearArith ArithException Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int -> uf Int Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> uf Int Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

SafeLinearArith ArithException Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> uf (SymIntN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> uf (SymIntN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where Source #

Safe division with monadic error handling in multi-path execution. These procedures throw an exception when the divisor is zero. The result should be able to handle errors with MonadError.

Minimal complete definition

(safeDivMod | safeDiv, safeMod), (safeDivMod' | safeDiv', safeMod')

Methods

safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed div with monadic error handling in multi-path execution.

>>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}

safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed mod with monadic error handling in multi-path execution.

>>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}

safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #

Safe signed divMod with monadic error handling in multi-path execution.

>>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)
ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}

safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed quot with monadic error handling in multi-path execution.

safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe signed rem with monadic error handling in multi-path execution.

safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #

Safe signed quotRem with monadic error handling in multi-path execution.

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed div with monadic error handling in multi-path execution. The error is transformed.

>>> safeDiv' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger
ExceptT {If (= b 0) (Left ()) (Right (div a b))}

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed mod with monadic error handling in multi-path execution. The error is transformed.

>>> safeMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger
ExceptT {If (= b 0) (Left ()) (Right (mod a b))}

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #

Safe signed divMod with monadic error handling in multi-path execution. The error is transformed.

>>> safeDivMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM (SymInteger, SymInteger)
ExceptT {If (= b 0) (Left ()) (Right ((div a b),(mod a b)))}

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed quot with monadic error handling in multi-path execution. The error is transformed.

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe signed rem with monadic error handling in multi-path execution. The error is transformed.

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #

Safe signed quotRem with monadic error handling in multi-path execution. The error is transformed.

Instances

Instances details
SafeDivision ArithException Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf SymInteger Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymInteger -> SymInteger -> uf (SymInteger, SymInteger) Source #

SafeDivision ArithException Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeDivision ArithException Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf (Int, Int) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf (Int, Int) Source #

SafeDivision ArithException Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n, SymIntN n) Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymWordN n -> SymWordN n -> uf (SymWordN n, SymWordN n) Source #

SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where Source #

Safe division with monadic error handling in multi-path execution. These procedures throw an exception when overflow or underflow happens. The result should be able to handle errors with MonadError.

Methods

safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe + with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {Right (+ a b)}
>>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)
ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}

safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a Source #

Safe negate with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeNeg (ssym "a") :: ExceptT ArithException UnionM SymInteger
ExceptT {Right (- a)}
>>> safeNeg (ssym "a") :: ExceptT ArithException UnionM (SymIntN 4)
ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}

safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #

Safe - with monadic error handling in multi-path execution. Overflows or underflows are treated as errors.

>>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {Right (+ a (- b))}
>>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)
ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe + with monadic error handling in multi-path execution. Overflows or underflows are treated as errors. The error is transformed.

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a Source #

Safe negate with monadic error handling in multi-path execution. Overflows or underflows are treated as errors. The error is transformed.

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #

Safe - with monadic error handling in multi-path execution. Overflows or underflows are treated as errors. The error is transformed.

Instances

Instances details
SafeLinearArith ArithException Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SafeLinearArith ArithException Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith ArithException Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => Int -> uf Int Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => Int -> Int -> uf Int Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> uf Int Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> Int -> Int -> uf Int Source #

SafeLinearArith ArithException Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> uf (SymIntN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> uf (SymIntN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a Source #

Aggregation for the operations on symbolic integer types

Instances

Instances details
SymIntegerOp SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim