-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.Overflow
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Implementation of overflow detection functions.
-- Based on: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf>
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ImplicitParams       #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.Overflow (

         -- * Arithmetic overflows
         ArithOverflow(..), CheckedArithmetic(..)

         -- * Fast-checking of signed-multiplication overflow
         , signedMulOverflow

         -- * Cast overflows
       , sFromIntegralO, sFromIntegralChecked

    ) where

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Model
import Data.SBV.Core.Operations

import GHC.TypeLits

import GHC.Stack

import Data.Int
import Data.Word
import Data.Proxy

-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV

-- | Detecting overflow. Each function here will return 'sTrue' if the result will not fit in the target
-- type, i.e., if it overflows or underflows.
class ArithOverflow a where
  -- | Bit-vector addition. Unsigned addition can only overflow. Signed addition can underflow and overflow.
  --
  -- A tell tale sign of unsigned addition overflow is when the sum is less than minimum of the arguments.
  --
  -- >>> prove $ \x y -> bvAddO x (y::SWord16) .<=> x + y .< x `smin` y
  -- Q.E.D.
  bvAddO :: a -> a -> SBool

  -- | Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.
  bvSubO :: a -> a -> SBool

  -- | Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.
  bvMulO :: a -> a -> SBool

  -- | Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each
  -- signed bitvector type, there's precisely one pair that overflows, when @x@ is @minBound@ and @y@ is @-1@:
  --
  -- >>> allSat $ \x y -> x `bvDivO` (y::SInt8)
  -- Solution #1:
  --   s0 = -128 :: Int8
  --   s1 =   -1 :: Int8
  -- This is the only solution.
  bvDivO :: a -> a -> SBool

  -- | Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
  -- @minBound@:
  --
  -- >>> prove $ \x -> x .== minBound .<=> bvNegO (x::SInt16)
  -- Q.E.D.
  bvNegO :: a -> SBool

instance ArithOverflow SWord8  where {bvAddO :: SWord8 -> SWord8 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SWord8 -> SWord8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SWord8 -> SWord8 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SWord8 -> SWord8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SWord8 -> SWord8 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SWord8 -> SWord8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SWord8 -> SWord8 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SWord8 -> SWord8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SWord8 -> SBool
bvNegO = (SVal -> SBool) -> SWord8 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SWord16 where {bvAddO :: SWord16 -> SWord16 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SWord16 -> SWord16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SWord16 -> SWord16 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SWord16 -> SWord16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SWord16 -> SWord16 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SWord16 -> SWord16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SWord16 -> SWord16 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SWord16 -> SWord16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SWord16 -> SBool
bvNegO = (SVal -> SBool) -> SWord16 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SWord32 where {bvAddO :: SWord32 -> SWord32 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SWord32 -> SWord32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SWord32 -> SWord32 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SWord32 -> SWord32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SWord32 -> SWord32 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SWord32 -> SWord32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SWord32 -> SWord32 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SWord32 -> SWord32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SWord32 -> SBool
bvNegO = (SVal -> SBool) -> SWord32 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SWord64 where {bvAddO :: SWord64 -> SWord64 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SWord64 -> SWord64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SWord64 -> SWord64 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SWord64 -> SWord64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SWord64 -> SWord64 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SWord64 -> SWord64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SWord64 -> SWord64 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SWord64 -> SWord64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SWord64 -> SBool
bvNegO = (SVal -> SBool) -> SWord64 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SInt8   where {bvAddO :: SInt8 -> SInt8 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SInt8 -> SInt8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SInt8 -> SInt8 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SInt8 -> SInt8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SInt8 -> SInt8 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SInt8 -> SInt8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SInt8 -> SInt8 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SInt8 -> SInt8 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SInt8 -> SBool
bvNegO = (SVal -> SBool) -> SInt8 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SInt16  where {bvAddO :: SInt16 -> SInt16 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SInt16 -> SInt16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SInt16 -> SInt16 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SInt16 -> SInt16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SInt16 -> SInt16 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SInt16 -> SInt16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SInt16 -> SInt16 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SInt16 -> SInt16 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SInt16 -> SBool
bvNegO = (SVal -> SBool) -> SInt16 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SInt32  where {bvAddO :: SInt32 -> SInt32 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SInt32 -> SInt32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SInt32 -> SInt32 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SInt32 -> SInt32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SInt32 -> SInt32 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SInt32 -> SInt32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SInt32 -> SInt32 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SInt32 -> SInt32 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SInt32 -> SBool
bvNegO = (SVal -> SBool) -> SInt32 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance ArithOverflow SInt64  where {bvAddO :: SInt64 -> SInt64 -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SInt64 -> SInt64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SInt64 -> SInt64 -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SInt64 -> SInt64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SInt64 -> SInt64 -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SInt64 -> SInt64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SInt64 -> SInt64 -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SInt64 -> SInt64 -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SInt64 -> SBool
bvNegO = (SVal -> SBool) -> SInt64 -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}

instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) where {bvAddO :: SWord n -> SWord n -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SWord n -> SWord n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SWord n -> SWord n -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SWord n -> SWord n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SWord n -> SWord n -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SWord n -> SWord n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SWord n -> SWord n -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SWord n -> SWord n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SWord n -> SBool
bvNegO = (SVal -> SBool) -> SWord n -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}
instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt  n) where {bvAddO :: SInt n -> SInt n -> SBool
bvAddO = (SVal -> SVal -> SBool) -> SInt n -> SInt n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO; bvSubO :: SInt n -> SInt n -> SBool
bvSubO = (SVal -> SVal -> SBool) -> SInt n -> SInt n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO; bvMulO :: SInt n -> SInt n -> SBool
bvMulO = (SVal -> SVal -> SBool) -> SInt n -> SInt n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO; bvDivO :: SInt n -> SInt n -> SBool
bvDivO = (SVal -> SVal -> SBool) -> SInt n -> SInt n -> SBool
forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO; bvNegO :: SInt n -> SBool
bvNegO = (SVal -> SBool) -> SInt n -> SBool
forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO}

instance ArithOverflow SVal where
  bvAddO :: SVal -> SVal -> SBool
bvAddO     = (SVal -> SVal -> SVal)
-> (SVal -> SVal -> SVal) -> SVal -> SVal -> SBool
signPick2 (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
PlusOv Bool
False)) (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
PlusOv Bool
True))
  bvSubO :: SVal -> SVal -> SBool
bvSubO     = (SVal -> SVal -> SVal)
-> (SVal -> SVal -> SVal) -> SVal -> SVal -> SBool
signPick2 (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
SubOv  Bool
False)) (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
SubOv  Bool
True))
  bvMulO :: SVal -> SVal -> SBool
bvMulO     = (SVal -> SVal -> SVal)
-> (SVal -> SVal -> SVal) -> SVal -> SVal -> SBool
signPick2 (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
MulOv  Bool
False)) (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 (Bool -> OvOp
MulOv  Bool
True))
  bvDivO :: SVal -> SVal -> SBool
bvDivO     = (SVal -> SVal -> SVal)
-> (SVal -> SVal -> SVal) -> SVal -> SVal -> SBool
signPick2 ((SVal -> SVal) -> SVal -> SVal -> SVal
forall a b. a -> b -> a
const (SVal -> SVal -> SVal
forall a b. a -> b -> a
const SVal
svFalse))        (OvOp -> SVal -> SVal -> SVal
svMkOverflow2 OvOp
DivOv)           -- unsigned division doesn't overflow
  bvNegO :: SVal -> SBool
bvNegO     = (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SBool
signPick1 (SVal -> SVal -> SVal
forall a b. a -> b -> a
const SVal
svFalse)                (OvOp -> SVal -> SVal
svMkOverflow1 OvOp
NegOv)           -- unsigned unary negation doesn't overflow

-- | A class of checked-arithmetic operations. These follow the usual arithmetic,
-- except make calls to 'Data.SBV.sAssert' to ensure no overflow/underflow can occur.
-- Use them in conjunction with 'Data.SBV.safe' to ensure no overflow can happen.
class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where
  (+!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  (-!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  (*!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  (/!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  negateChecked :: (?loc :: CallStack) => SBV a          -> SBV a

  infixl 6 +!, -!
  infixl 7 *!, /!

instance CheckedArithmetic Word8 where
  +! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
(+!)          = CallStack
-> String
-> (SWord8 -> SWord8 -> SWord8)
-> (SWord8 -> SWord8 -> SBool)
-> SWord8
-> SWord8
-> SWord8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
(+)    SWord8 -> SWord8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
(-!)          = CallStack
-> String
-> (SWord8 -> SWord8 -> SWord8)
-> (SWord8 -> SWord8 -> SBool)
-> SWord8
-> SWord8
-> SWord8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SWord8 -> SWord8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
(*!)          = CallStack
-> String
-> (SWord8 -> SWord8 -> SWord8)
-> (SWord8 -> SWord8 -> SBool)
-> SWord8
-> SWord8
-> SWord8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
(*)    SWord8 -> SWord8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
(/!)          = CallStack
-> String
-> (SWord8 -> SWord8 -> SWord8)
-> (SWord8 -> SWord8 -> SBool)
-> SWord8
-> SWord8
-> SWord8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SWord8 -> SWord8 -> SWord8
forall a. SDivisible a => a -> a -> a
sDiv   SWord8 -> SWord8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SWord8 -> SWord8
negateChecked = CallStack
-> String
-> (SWord8 -> SWord8)
-> (SWord8 -> SBool)
-> SWord8
-> SWord8
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SWord8 -> SWord8
forall a. Num a => a -> a
negate SWord8 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Word16 where
  +! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
(+!)          = CallStack
-> String
-> (SWord16 -> SWord16 -> SWord16)
-> (SWord16 -> SWord16 -> SBool)
-> SWord16
-> SWord16
-> SWord16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SWord16 -> SWord16 -> SWord16
forall a. Num a => a -> a -> a
(+)    SWord16 -> SWord16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
(-!)          = CallStack
-> String
-> (SWord16 -> SWord16 -> SWord16)
-> (SWord16 -> SWord16 -> SBool)
-> SWord16
-> SWord16
-> SWord16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SWord16 -> SWord16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
(*!)          = CallStack
-> String
-> (SWord16 -> SWord16 -> SWord16)
-> (SWord16 -> SWord16 -> SBool)
-> SWord16
-> SWord16
-> SWord16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SWord16 -> SWord16 -> SWord16
forall a. Num a => a -> a -> a
(*)    SWord16 -> SWord16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
(/!)          = CallStack
-> String
-> (SWord16 -> SWord16 -> SWord16)
-> (SWord16 -> SWord16 -> SBool)
-> SWord16
-> SWord16
-> SWord16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SWord16 -> SWord16 -> SWord16
forall a. SDivisible a => a -> a -> a
sDiv   SWord16 -> SWord16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SWord16 -> SWord16
negateChecked = CallStack
-> String
-> (SWord16 -> SWord16)
-> (SWord16 -> SBool)
-> SWord16
-> SWord16
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SWord16 -> SWord16
forall a. Num a => a -> a
negate SWord16 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Word32 where
  +! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
(+!)          = CallStack
-> String
-> (SWord32 -> SWord32 -> SWord32)
-> (SWord32 -> SWord32 -> SBool)
-> SWord32
-> SWord32
-> SWord32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
(+)    SWord32 -> SWord32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
(-!)          = CallStack
-> String
-> (SWord32 -> SWord32 -> SWord32)
-> (SWord32 -> SWord32 -> SBool)
-> SWord32
-> SWord32
-> SWord32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SWord32 -> SWord32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
(*!)          = CallStack
-> String
-> (SWord32 -> SWord32 -> SWord32)
-> (SWord32 -> SWord32 -> SBool)
-> SWord32
-> SWord32
-> SWord32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
(*)    SWord32 -> SWord32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
(/!)          = CallStack
-> String
-> (SWord32 -> SWord32 -> SWord32)
-> (SWord32 -> SWord32 -> SBool)
-> SWord32
-> SWord32
-> SWord32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SWord32 -> SWord32 -> SWord32
forall a. SDivisible a => a -> a -> a
sDiv   SWord32 -> SWord32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SWord32 -> SWord32
negateChecked = CallStack
-> String
-> (SWord32 -> SWord32)
-> (SWord32 -> SBool)
-> SWord32
-> SWord32
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SWord32 -> SWord32
forall a. Num a => a -> a
negate SWord32 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Word64 where
  +! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
(+!)          = CallStack
-> String
-> (SWord64 -> SWord64 -> SWord64)
-> (SWord64 -> SWord64 -> SBool)
-> SWord64
-> SWord64
-> SWord64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SWord64 -> SWord64 -> SWord64
forall a. Num a => a -> a -> a
(+)    SWord64 -> SWord64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
(-!)          = CallStack
-> String
-> (SWord64 -> SWord64 -> SWord64)
-> (SWord64 -> SWord64 -> SBool)
-> SWord64
-> SWord64
-> SWord64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SWord64 -> SWord64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
(*!)          = CallStack
-> String
-> (SWord64 -> SWord64 -> SWord64)
-> (SWord64 -> SWord64 -> SBool)
-> SWord64
-> SWord64
-> SWord64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SWord64 -> SWord64 -> SWord64
forall a. Num a => a -> a -> a
(*)    SWord64 -> SWord64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
(/!)          = CallStack
-> String
-> (SWord64 -> SWord64 -> SWord64)
-> (SWord64 -> SWord64 -> SBool)
-> SWord64
-> SWord64
-> SWord64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SWord64 -> SWord64 -> SWord64
forall a. SDivisible a => a -> a -> a
sDiv   SWord64 -> SWord64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SWord64 -> SWord64
negateChecked = CallStack
-> String
-> (SWord64 -> SWord64)
-> (SWord64 -> SBool)
-> SWord64
-> SWord64
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SWord64 -> SWord64
forall a. Num a => a -> a
negate SWord64 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Int8 where
  +! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
(+!)          = CallStack
-> String
-> (SInt8 -> SInt8 -> SInt8)
-> (SInt8 -> SInt8 -> SBool)
-> SInt8
-> SInt8
-> SInt8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SInt8 -> SInt8 -> SInt8
forall a. Num a => a -> a -> a
(+)    SInt8 -> SInt8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
(-!)          = CallStack
-> String
-> (SInt8 -> SInt8 -> SInt8)
-> (SInt8 -> SInt8 -> SBool)
-> SInt8
-> SInt8
-> SInt8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SInt8 -> SInt8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
(*!)          = CallStack
-> String
-> (SInt8 -> SInt8 -> SInt8)
-> (SInt8 -> SInt8 -> SBool)
-> SInt8
-> SInt8
-> SInt8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SInt8 -> SInt8 -> SInt8
forall a. Num a => a -> a -> a
(*)    SInt8 -> SInt8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
(/!)          = CallStack
-> String
-> (SInt8 -> SInt8 -> SInt8)
-> (SInt8 -> SInt8 -> SBool)
-> SInt8
-> SInt8
-> SInt8
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SInt8 -> SInt8 -> SInt8
forall a. SDivisible a => a -> a -> a
sDiv   SInt8 -> SInt8 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SInt8 -> SInt8
negateChecked = CallStack
-> String -> (SInt8 -> SInt8) -> (SInt8 -> SBool) -> SInt8 -> SInt8
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SInt8 -> SInt8
forall a. Num a => a -> a
negate SInt8 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Int16 where
  +! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
(+!)          = CallStack
-> String
-> (SInt16 -> SInt16 -> SInt16)
-> (SInt16 -> SInt16 -> SBool)
-> SInt16
-> SInt16
-> SInt16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SInt16 -> SInt16 -> SInt16
forall a. Num a => a -> a -> a
(+)    SInt16 -> SInt16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
(-!)          = CallStack
-> String
-> (SInt16 -> SInt16 -> SInt16)
-> (SInt16 -> SInt16 -> SBool)
-> SInt16
-> SInt16
-> SInt16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SInt16 -> SInt16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
(*!)          = CallStack
-> String
-> (SInt16 -> SInt16 -> SInt16)
-> (SInt16 -> SInt16 -> SBool)
-> SInt16
-> SInt16
-> SInt16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SInt16 -> SInt16 -> SInt16
forall a. Num a => a -> a -> a
(*)    SInt16 -> SInt16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
(/!)          = CallStack
-> String
-> (SInt16 -> SInt16 -> SInt16)
-> (SInt16 -> SInt16 -> SBool)
-> SInt16
-> SInt16
-> SInt16
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SInt16 -> SInt16 -> SInt16
forall a. SDivisible a => a -> a -> a
sDiv   SInt16 -> SInt16 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SInt16 -> SInt16
negateChecked = CallStack
-> String
-> (SInt16 -> SInt16)
-> (SInt16 -> SBool)
-> SInt16
-> SInt16
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SInt16 -> SInt16
forall a. Num a => a -> a
negate SInt16 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Int32 where
  +! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
(+!)          = CallStack
-> String
-> (SInt32 -> SInt32 -> SInt32)
-> (SInt32 -> SInt32 -> SBool)
-> SInt32
-> SInt32
-> SInt32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SInt32 -> SInt32 -> SInt32
forall a. Num a => a -> a -> a
(+)    SInt32 -> SInt32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
(-!)          = CallStack
-> String
-> (SInt32 -> SInt32 -> SInt32)
-> (SInt32 -> SInt32 -> SBool)
-> SInt32
-> SInt32
-> SInt32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SInt32 -> SInt32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
(*!)          = CallStack
-> String
-> (SInt32 -> SInt32 -> SInt32)
-> (SInt32 -> SInt32 -> SBool)
-> SInt32
-> SInt32
-> SInt32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SInt32 -> SInt32 -> SInt32
forall a. Num a => a -> a -> a
(*)    SInt32 -> SInt32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
(/!)          = CallStack
-> String
-> (SInt32 -> SInt32 -> SInt32)
-> (SInt32 -> SInt32 -> SBool)
-> SInt32
-> SInt32
-> SInt32
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SInt32 -> SInt32 -> SInt32
forall a. SDivisible a => a -> a -> a
sDiv   SInt32 -> SInt32 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SInt32 -> SInt32
negateChecked = CallStack
-> String
-> (SInt32 -> SInt32)
-> (SInt32 -> SBool)
-> SInt32
-> SInt32
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SInt32 -> SInt32
forall a. Num a => a -> a
negate SInt32 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance CheckedArithmetic Int64 where
  +! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
(+!)          = CallStack
-> String
-> (SInt64 -> SInt64 -> SInt64)
-> (SInt64 -> SInt64 -> SBool)
-> SInt64
-> SInt64
-> SInt64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SInt64 -> SInt64 -> SInt64
forall a. Num a => a -> a -> a
(+)    SInt64 -> SInt64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
(-!)          = CallStack
-> String
-> (SInt64 -> SInt64 -> SInt64)
-> (SInt64 -> SInt64 -> SBool)
-> SInt64
-> SInt64
-> SInt64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SInt64 -> SInt64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
(*!)          = CallStack
-> String
-> (SInt64 -> SInt64 -> SInt64)
-> (SInt64 -> SInt64 -> SBool)
-> SInt64
-> SInt64
-> SInt64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SInt64 -> SInt64 -> SInt64
forall a. Num a => a -> a -> a
(*)    SInt64 -> SInt64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
(/!)          = CallStack
-> String
-> (SInt64 -> SInt64 -> SInt64)
-> (SInt64 -> SInt64 -> SBool)
-> SInt64
-> SInt64
-> SInt64
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SInt64 -> SInt64 -> SInt64
forall a. SDivisible a => a -> a -> a
sDiv   SInt64 -> SInt64 -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SInt64 -> SInt64
negateChecked = CallStack
-> String
-> (SInt64 -> SInt64)
-> (SInt64 -> SBool)
-> SInt64
-> SInt64
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SInt64 -> SInt64
forall a. Num a => a -> a
negate SInt64 -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) where
  +! :: (?loc::CallStack) =>
SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
(+!)          = CallStack
-> String
-> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
-> (SBV (WordN n) -> SBV (WordN n) -> SBool)
-> SBV (WordN n)
-> SBV (WordN n)
-> SBV (WordN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a. Num a => a -> a -> a
(+)    SBV (WordN n) -> SBV (WordN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) =>
SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
(-!)          = CallStack
-> String
-> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
-> (SBV (WordN n) -> SBV (WordN n) -> SBool)
-> SBV (WordN n)
-> SBV (WordN n)
-> SBV (WordN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SBV (WordN n) -> SBV (WordN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) =>
SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
(*!)          = CallStack
-> String
-> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
-> (SBV (WordN n) -> SBV (WordN n) -> SBool)
-> SBV (WordN n)
-> SBV (WordN n)
-> SBV (WordN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a. Num a => a -> a -> a
(*)    SBV (WordN n) -> SBV (WordN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) =>
SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
(/!)          = CallStack
-> String
-> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
-> (SBV (WordN n) -> SBV (WordN n) -> SBool)
-> SBV (WordN n)
-> SBV (WordN n)
-> SBV (WordN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a. SDivisible a => a -> a -> a
sDiv   SBV (WordN n) -> SBV (WordN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SBV (WordN n) -> SBV (WordN n)
negateChecked = CallStack
-> String
-> (SBV (WordN n) -> SBV (WordN n))
-> (SBV (WordN n) -> SBool)
-> SBV (WordN n)
-> SBV (WordN n)
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SBV (WordN n) -> SBV (WordN n)
forall a. Num a => a -> a
negate SBV (WordN n) -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) where
  +! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
(+!)          = CallStack
-> String
-> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
-> (SBV (IntN n) -> SBV (IntN n) -> SBool)
-> SBV (IntN n)
-> SBV (IntN n)
-> SBV (IntN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"addition"       SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
forall a. Num a => a -> a -> a
(+)    SBV (IntN n) -> SBV (IntN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvAddO
  -! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
(-!)          = CallStack
-> String
-> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
-> (SBV (IntN n) -> SBV (IntN n) -> SBool)
-> SBV (IntN n)
-> SBV (IntN n)
-> SBV (IntN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"subtraction"    (-)    SBV (IntN n) -> SBV (IntN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvSubO
  *! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
(*!)          = CallStack
-> String
-> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
-> (SBV (IntN n) -> SBV (IntN n) -> SBool)
-> SBV (IntN n)
-> SBV (IntN n)
-> SBV (IntN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"multiplication" SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
forall a. Num a => a -> a -> a
(*)    SBV (IntN n) -> SBV (IntN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvMulO
  /! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
(/!)          = CallStack
-> String
-> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
-> (SBV (IntN n) -> SBV (IntN n) -> SBool)
-> SBV (IntN n)
-> SBV (IntN n)
-> SBV (IntN n)
forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 ?loc::CallStack
CallStack
?loc String
"division"       SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
forall a. SDivisible a => a -> a -> a
sDiv   SBV (IntN n) -> SBV (IntN n) -> SBool
forall a. ArithOverflow a => a -> a -> SBool
bvDivO
  negateChecked :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n)
negateChecked = CallStack
-> String
-> (SBV (IntN n) -> SBV (IntN n))
-> (SBV (IntN n) -> SBool)
-> SBV (IntN n)
-> SBV (IntN n)
forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 ?loc::CallStack
CallStack
?loc String
"unary negation" SBV (IntN n) -> SBV (IntN n)
forall a. Num a => a -> a
negate SBV (IntN n) -> SBool
forall a. ArithOverflow a => a -> SBool
bvNegO

-- | Check all true
svAll :: [SVal] -> SVal
svAll :: [SVal] -> SVal
svAll = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SVal -> SVal -> SVal
svAnd SVal
svTrue

-- | Are all the bits between a b (inclusive) zero?
allZero :: Int -> Int -> SBV a -> SVal
allZero :: forall a. Int -> Int -> SBV a -> SVal
allZero Int
m Int
n (SBV SVal
x)
  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
sz Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
  = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Tools.Overflow.allZero: Received unexpected parameters: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int, Int) -> String
forall a. Show a => a -> String
show (Int
m, Int
n, Int
sz)
  | Bool
True
  = [SVal] -> SVal
svAll [SVal -> Int -> SVal
svTestBit SVal
x Int
i SVal -> SVal -> SVal
`svEqual` SVal
svFalse | Int
i <- [Int
m, Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1 .. Int
n]]
  where sz :: Int
sz = SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
x

-- | Are all the bits between a b (inclusive) one?
allOne :: Int -> Int -> SBV a -> SVal
allOne :: forall a. Int -> Int -> SBV a -> SVal
allOne Int
m Int
n (SBV SVal
x)
  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
sz Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
  = String -> SVal
forall a. HasCallStack => String -> a
error (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Tools.Overflow.allOne: Received unexpected parameters: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int, Int) -> String
forall a. Show a => a -> String
show (Int
m, Int
n, Int
sz)
  | Bool
True
  = [SVal] -> SVal
svAll [SVal -> Int -> SVal
svTestBit SVal
x Int
i SVal -> SVal -> SVal
`svEqual` SVal
svTrue | Int
i <- [Int
m, Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1 .. Int
n]]
  where sz :: Int
sz = SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
x

-- | Detecting underflow/overflow conditions for casting between bit-vectors. The first output is the result,
-- the second component itself is a pair with the first boolean indicating underflow and the second indicating overflow.
--
-- >>> sFromIntegralO (256 :: SInt16) :: (SWord8, (SBool, SBool))
-- (0 :: SWord8,(False,True))
-- >>> sFromIntegralO (-2 :: SInt16) :: (SWord8, (SBool, SBool))
-- (254 :: SWord8,(True,False))
-- >>> sFromIntegralO (2 :: SInt16) :: (SWord8, (SBool, SBool))
-- (2 :: SWord8,(False,False))
-- >>> prove $ \x -> sFromIntegralO (x::SInt32) .== (sFromIntegral x :: SInteger, (sFalse, sFalse))
-- Q.E.D.
--
-- As the last example shows, converting to `sInteger` never underflows or overflows for any value.
sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))
sFromIntegralO :: forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> (SBV b, (SBool, SBool))
sFromIntegralO SBV a
x = case (SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x, Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)) of
                     (KBounded Bool
False Int
n, KBounded Bool
False Int
m) -> (SBV b
res, Int -> Int -> (SBool, SBool)
u2u Int
n Int
m)
                     (KBounded Bool
False Int
n, KBounded Bool
True  Int
m) -> (SBV b
res, Int -> Int -> (SBool, SBool)
u2s Int
n Int
m)
                     (KBounded Bool
True Int
n,  KBounded Bool
False Int
m) -> (SBV b
res, Int -> Int -> (SBool, SBool)
s2u Int
n Int
m)
                     (KBounded Bool
True Int
n,  KBounded Bool
True  Int
m) -> (SBV b
res, Int -> Int -> (SBool, SBool)
s2s Int
n Int
m)
                     (Kind
KUnbounded,       KBounded Bool
s Int
m)     -> (SBV b
res, Bool -> Int -> (SBool, SBool)
checkBounds Bool
s Int
m)
                     (KBounded{},       Kind
KUnbounded)       -> (SBV b
res, (SBool
sFalse, SBool
sFalse))
                     (Kind
KUnbounded,       Kind
KUnbounded)       -> (SBV b
res, (SBool
sFalse, SBool
sFalse))
                     (Kind
kFrom,            Kind
kTo)              -> String -> (SBV b, (SBool, SBool))
forall a. HasCallStack => String -> a
error (String -> (SBV b, (SBool, SBool)))
-> String -> (SBV b, (SBool, SBool))
forall a b. (a -> b) -> a -> b
$ String
"sFromIntegralO: Expected bounded-BV types, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
kFrom, Kind
kTo)

  where res :: SBV b
        res :: SBV b
res = SBV a -> SBV b
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
x

        checkBounds :: Bool -> Int -> (SBool, SBool)
        checkBounds :: Bool -> Int -> (SBool, SBool)
checkBounds Bool
signed Int
sz = (SInteger
ix SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
lb, SInteger
ix SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
ub)
          where ix :: SInteger
                ix :: SInteger
ix = SBV a -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV a
x

                s :: Integer
                s :: Integer
s = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
sz

                ub :: Integer
                ub :: Integer
ub | Bool
signed = Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
                   | Bool
True   = Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
s       Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

                lb :: Integer
                lb :: Integer
lb | Bool
signed = -Integer
ubInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1
                   | Bool
True   = Integer
0

        u2u :: Int -> Int -> (SBool, SBool)
        u2u :: Int -> Int -> (SBool, SBool)
u2u Int
n Int
m = (SBool
underflow, SBool
overflow)
          where underflow :: SBool
underflow  = SBool
sFalse
                overflow :: SBool
overflow
                  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
m = SBool
sFalse
                  | Bool
True   = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SBV a -> SVal
forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
m SBV a
x

        u2s :: Int -> Int -> (SBool, SBool)
        u2s :: Int -> Int -> (SBool, SBool)
u2s Int
n Int
m = (SBool
underflow, SBool
overflow)
          where underflow :: SBool
underflow = SBool
sFalse
                overflow :: SBool
overflow
                  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SBV a -> SVal
forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SBV a
x

        s2u :: Int -> Int -> (SBool, SBool)
        s2u :: Int -> Int -> (SBool, SBool)
s2u Int
n Int
m = (SBool
forall {a}. SBV a
underflow, SBool
overflow)
          where underflow :: SBV a
underflow = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ (SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svTrue

                overflow :: SBool
overflow
                  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 = SBool
sFalse
                  | Bool
True       = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svFalse, SVal -> SVal
svNot (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SBV a -> SVal
forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
m SBV a
x]

        s2s :: Int -> Int -> (SBool, SBool)
        s2s :: Int -> Int -> (SBool, SBool)
s2s Int
n Int
m = (SBool
underflow, SBool
overflow)
          where underflow :: SBool
underflow
                  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svTrue,  SVal -> SVal
svNot (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SBV a -> SVal
forall a. Int -> Int -> SBV a -> SVal
allOne  (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SBV a
x]

                overflow :: SBool
overflow
                  | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svFalse, SVal -> SVal
svNot (SVal -> SVal) -> SVal -> SVal
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SBV a -> SVal
forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SBV a
x]

-- | Version of 'sFromIntegral' that has calls to 'Data.SBV.sAssert' for checking no overflow/underflow can happen. Use it with a 'Data.SBV.safe' call.
sFromIntegralChecked :: forall a b. (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
sFromIntegralChecked :: forall a b.
(?loc::CallStack, Integral a, HasKind a, HasKind b, Num a,
 SymVal a, HasKind b, Num b, SymVal b) =>
SBV a -> SBV b
sFromIntegralChecked SBV a
x = Maybe CallStack -> String -> SBool -> SBV b -> SBV b
forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (CallStack -> Maybe CallStack
forall a. a -> Maybe a
Just ?loc::CallStack
CallStack
?loc) (String -> String
msg String
"underflows") (SBool -> SBool
sNot SBool
u)
                       (SBV b -> SBV b) -> SBV b -> SBV b
forall a b. (a -> b) -> a -> b
$ Maybe CallStack -> String -> SBool -> SBV b -> SBV b
forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (CallStack -> Maybe CallStack
forall a. a -> Maybe a
Just ?loc::CallStack
CallStack
?loc) (String -> String
msg String
"overflows")  (SBool -> SBool
sNot SBool
o)
                         SBV b
r
  where kFrom :: String
kFrom = Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> Kind -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x
        kTo :: String
kTo   = Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> Kind -> String
forall a b. (a -> b) -> a -> b
$ Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
        msg :: String -> String
msg String
c = String
"Casting from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
kFrom String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
kTo String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c

        (SBV b
r, (SBool
u, SBool
o)) = SBV a -> (SBV b, (SBool, SBool))
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> (SBV b, (SBool, SBool))
sFromIntegralO SBV a
x

-- | signedMulOverflow: Checking if a signed bitvector multiplication can overflow. In general you should simply use 'bvMulO' for checking
-- signed multiplication overflow for bit-vectors. This is a function supported by SMTLib. Unfortunately, individual implementations have
-- different performance characteristics. For instance, bitwuzla has a fairly performant implementation of this, but z3 does not. (At least
-- not as of August 2024.) In cases where you can't use bitwuzla, you can use this implementation which has better performance.
signedMulOverflow :: forall n. ( KnownNat n,          BVIsNonZero n
                               , KnownNat (n+1),      BVIsNonZero (n+1)
                               , KnownNat (2+Log2 n), BVIsNonZero (2+Log2 n))
                               => SInt n -> SInt n -> SBool
signedMulOverflow :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n, KnownNat (n + 1), BVIsNonZero (n + 1),
 KnownNat (2 + Log2 n), BVIsNonZero (2 + Log2 n)) =>
SInt n -> SInt n -> SBool
signedMulOverflow SInt n
x SInt n
y = SBool -> SBool
sNot SBool
zeroOut SBool -> SBool -> SBool
.&& SBool
overflow
  where zeroOut :: SBool
zeroOut = SInt n
x SInt n -> SInt n -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInt n
0 SBool -> SBool -> SBool
.|| SInt n
y SInt n -> SInt n -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInt n
0

        prod :: SInt (n+1)
        prod :: SBV (IntN (n + 1))
prod = SInt n -> SBV (IntN (n + 1))
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInt n
x SBV (IntN (n + 1)) -> SBV (IntN (n + 1)) -> SBV (IntN (n + 1))
forall a. Num a => a -> a -> a
* SInt n -> SBV (IntN (n + 1))
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInt n
y

        nv :: Int
        nv :: Int
nv = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)

        prodN, prodNm1 :: SBool
        prodN :: SBool
prodN   = SBV (IntN (n + 1))
prod SBV (IntN (n + 1)) -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
`sTestBit` Int
nv
        prodNm1 :: SBool
prodNm1 = SBV (IntN (n + 1))
prod SBV (IntN (n + 1)) -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
`sTestBit` (Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

        overflow :: SBool
overflow =   (KnownNat n, BVIsNonZero n, KnownNat (2 + Log2 n),
 BVIsNonZero (2 + Log2 n)) =>
SInt n -> SBV (WordN (2 + Log2 n))
SInt n -> SBV (WordN (2 + Log2 n))
nonSignBitPos SInt n
x SBV (WordN (2 + Log2 n))
-> SBV (WordN (2 + Log2 n)) -> SBV (WordN (2 + Log2 n))
forall a. Num a => a -> a -> a
+ (KnownNat n, BVIsNonZero n, KnownNat (2 + Log2 n),
 BVIsNonZero (2 + Log2 n)) =>
SInt n -> SBV (WordN (2 + Log2 n))
SInt n -> SBV (WordN (2 + Log2 n))
nonSignBitPos SInt n
y SBV (WordN (2 + Log2 n)) -> SBV (WordN (2 + Log2 n)) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> WordN (2 + Log2 n) -> SBV (WordN (2 + Log2 n))
forall a. SymVal a => a -> SBV a
literal (Int -> WordN (2 + Log2 n)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2))
                 SBool -> SBool -> SBool
.|| SBool
prodN SBool -> SBool -> SBool
.<+> SBool
prodNm1

        -- Find the position of the first non-sign bit. i.e., the first bit that differs from the msb.
        -- Position is 0 indexed. Note that if there's no differing bit, then you also get back 0.
        -- This is essentially an approximation of the logarithm of the magnitude of the number.
        --
        -- The result is at most N-2 for an N-bit word. Later we add two of these, so the maximum
        -- value we need to represent is 2N-4. This will require 1 + lg(2N-4) = 2 + log(N-1) bits.
        -- To suppor the case N=0, we return a (2 + log N) bit word.
        --
        -- Example for 3 bits:
        --
        --    000 -> 0  (no differing bit from 0; so we get 0)
        --    001 -> 0
        --    010 -> 1
        --    011 -> 1
        --    100 -> 1
        --    101 -> 1
        --    110 -> 0
        --    111 -> 0  (no differing bit from 1; so we get 0)
        nonSignBitPos :: ( KnownNat n,          BVIsNonZero n
                         , KnownNat (2+Log2 n), BVIsNonZero (2+Log2 n))
                         => SInt n -> SWord (2+Log2 n)
        nonSignBitPos :: (KnownNat n, BVIsNonZero n, KnownNat (2 + Log2 n),
 BVIsNonZero (2 + Log2 n)) =>
SInt n -> SBV (WordN (2 + Log2 n))
nonSignBitPos SInt n
w = SBV (WordN (2 + Log2 n))
-> [(SBV (WordN (2 + Log2 n)), SBool)] -> SBV (WordN (2 + Log2 n))
forall {t}. Mergeable t => t -> [(t, SBool)] -> t
walk SBV (WordN (2 + Log2 n))
0 [(SBV (WordN (2 + Log2 n)), SBool)]
rest
          where (SBool
sign, [(SBV (WordN (2 + Log2 n)), SBool)]
rest) = case SInt n -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SInt n
w of
                                 []     -> String -> (SBool, [(SBV (WordN (2 + Log2 n)), SBool)])
forall a. HasCallStack => String -> a
error (String -> (SBool, [(SBV (WordN (2 + Log2 n)), SBool)]))
-> String -> (SBool, [(SBV (WordN (2 + Log2 n)), SBool)])
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened, blastBE returned no bits for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SInt n -> String
forall a. Show a => a -> String
show SInt n
w
                                 (SBool
b:[SBool]
bs) -> (SBool
b, [SBV (WordN (2 + Log2 n))]
-> [SBool] -> [(SBV (WordN (2 + Log2 n)), SBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SBV (WordN (2 + Log2 n))
0..] ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
bs))

                walk :: t -> [(t, SBool)] -> t
walk t
sofar []          = t
sofar
                walk t
sofar ((t
i, SBool
b):[(t, SBool)]
bs) = t -> [(t, SBool)] -> t
walk (SBool -> t -> t -> t
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBool
b SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBool
sign) t
i t
sofar) [(t, SBool)]
bs

-- Helpers
l2 :: (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 :: forall a. (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
l2 SVal -> SVal -> SBool
f (SBV SVal
a) (SBV SVal
b) = SVal -> SVal -> SBool
f SVal
a SVal
b

l1 :: (SVal -> SBool) -> SBV a -> SBool
l1 :: forall a. (SVal -> SBool) -> SBV a -> SBool
l1 SVal -> SBool
f (SBV SVal
a) = SVal -> SBool
f SVal
a

signPick2 :: (SVal -> SVal -> SVal) -> (SVal -> SVal -> SVal) -> (SVal -> SVal -> SBool)
signPick2 :: (SVal -> SVal -> SVal)
-> (SVal -> SVal -> SVal) -> SVal -> SVal -> SBool
signPick2 SVal -> SVal -> SVal
fu SVal -> SVal -> SVal
fs SVal
a SVal
b
 | SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
a = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
fs SVal
a SVal
b)
 | Bool
True      = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
fu SVal
a SVal
b)

signPick1 :: (SVal -> SVal) -> (SVal -> SVal) -> (SVal -> SBool)
signPick1 :: (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SBool
signPick1 SVal -> SVal
fu SVal -> SVal
fs SVal
a
 | SVal -> Bool
forall a. HasKind a => a -> Bool
hasSign SVal
a = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal
fs SVal
a)
 | Bool
True      = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal
fu SVal
a)

checkOp1 :: (HasKind a, HasKind b) => CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 :: forall a b.
(HasKind a, HasKind b) =>
CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b
checkOp1 CallStack
loc String
w a -> SBV b
op a -> SBool
cop a
a = Maybe CallStack -> String -> SBool -> SBV b -> SBV b
forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (CallStack -> Maybe CallStack
forall a. a -> Maybe a
Just CallStack
loc) (String -> String
msg String
"overflows") (SBool -> SBool
sNot (a -> SBool
cop a
a)) (SBV b -> SBV b) -> SBV b -> SBV b
forall a b. (a -> b) -> a -> b
$ a -> SBV b
op a
a
  where k :: String
k = Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> Kind -> String
forall a b. (a -> b) -> a -> b
$ a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
a
        msg :: String -> String
msg String
c = String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c

checkOp2 :: (HasKind a, HasKind c) => CallStack -> String -> (a -> b -> SBV c) -> (a -> b -> SBool) -> a -> b -> SBV c
checkOp2 :: forall a c b.
(HasKind a, HasKind c) =>
CallStack
-> String
-> (a -> b -> SBV c)
-> (a -> b -> SBool)
-> a
-> b
-> SBV c
checkOp2 CallStack
loc String
w a -> b -> SBV c
op a -> b -> SBool
cop a
a b
b = Maybe CallStack -> String -> SBool -> SBV c -> SBV c
forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (CallStack -> Maybe CallStack
forall a. a -> Maybe a
Just CallStack
loc) (String -> String
msg String
"overflows")  (SBool -> SBool
sNot (a
a a -> b -> SBool
`cop` b
b)) (SBV c -> SBV c) -> SBV c -> SBV c
forall a b. (a -> b) -> a -> b
$ a
a a -> b -> SBV c
`op` b
b
  where k :: String
k = Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> Kind -> String
forall a b. (a -> b) -> a -> b
$ a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
a
        msg :: String -> String
msg String
c = String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c