-----------------------------------------------------------------------------
-- |
-- 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 FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ImplicitParams       #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.Overflow (

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

         -- * Cast overflows
       , sFromIntegralO, sFromIntegralChecked

    ) where

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

import GHC.TypeLits

import GHC.Stack

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

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

-- | Detecting underflow/overflow conditions. For each function,
-- the first result is the condition under which the computation
-- underflows, and the second is the condition under which it
-- overflows.
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 -> snd (bvAddO x (y::SWord16)) .<=> x + y .< x `smin` y
  -- Q.E.D.
  bvAddO :: a -> a -> (SBool, SBool)

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

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

  -- | Same as 'bvMulO', except instead of doing the computation internally, it simply sends it off to z3 as a primitive.
  -- Obviously, only use if you have the z3 backend! Note that z3 provides this operation only when no logic is set,
  -- so make sure to call @setLogic Logic_NONE@ in your program!
  bvMulOFast :: a -> a -> (SBool, 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 -> snd (x `bvDivO` (y::SInt8))
  -- Solution #1:
  --   s0 = -128 :: Int8
  --   s1 =   -1 :: Int8
  -- This is the only solution.

  bvDivO :: a -> a -> (SBool, SBool)

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

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

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

instance ArithOverflow SVal where
  bvAddO :: SVal -> SVal -> (SBool, SBool)
bvAddO     = (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
bvuaddo     Int -> SVal -> SVal -> (SVal, SVal)
bvsaddo
  bvSubO :: SVal -> SVal -> (SBool, SBool)
bvSubO     = (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
bvusubo     Int -> SVal -> SVal -> (SVal, SVal)
bvssubo
  bvMulO :: SVal -> SVal -> (SBool, SBool)
bvMulO     = (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
bvumulo     Int -> SVal -> SVal -> (SVal, SVal)
bvsmulo
  bvMulOFast :: SVal -> SVal -> (SBool, SBool)
bvMulOFast = (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
bvumuloFast Int -> SVal -> SVal -> (SVal, SVal)
bvsmuloFast
  bvDivO :: SVal -> SVal -> (SBool, SBool)
bvDivO     = (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
bvudivo     Int -> SVal -> SVal -> (SVal, SVal)
bvsdivo
  bvNegO :: SVal -> (SBool, SBool)
bvNegO     = (Int -> SVal -> (SVal, SVal))
-> (Int -> SVal -> (SVal, SVal)) -> SVal -> (SBool, SBool)
signPick1 Int -> SVal -> (SVal, SVal)
bvunego     Int -> SVal -> (SVal, SVal)
bvsnego

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

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

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

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

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

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

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

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

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

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


-- | Zero-extend to given bits
zx :: Int -> SVal -> SVal
zx :: Int -> SVal -> SVal
zx Int
n SVal
a
 | Int
n forall a. Ord a => a -> a -> Bool
< Int
sa = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Unexpected zero extension: from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Int
intSizeOf SVal
a) forall a. [a] -> [a] -> [a]
++ String
" to: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
 | Bool
True   = SVal
p SVal -> SVal -> SVal
`svJoin` SVal
a
 where sa :: Int
sa = forall a. HasKind a => a -> Int
intSizeOf SVal
a
       s :: Bool
s  = forall a. HasKind a => a -> Bool
hasSign SVal
a
       p :: SVal
p  = Kind -> Integer -> SVal
svInteger (Bool -> Int -> Kind
KBounded Bool
s (Int
n forall a. Num a => a -> a -> a
- Int
sa)) Integer
0

-- | Sign-extend to given bits. Note that we keep the signedness of the argument.
sx :: Int -> SVal -> SVal
sx :: Int -> SVal -> SVal
sx Int
n SVal
a
 | Int
n forall a. Ord a => a -> a -> Bool
< Int
sa = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Unexpected sign extension: from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Int
intSizeOf SVal
a) forall a. [a] -> [a] -> [a]
++ String
" to: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
 | Bool
True   = SVal
p SVal -> SVal -> SVal
`svJoin` SVal
a
 where sa :: Int
sa = forall a. HasKind a => a -> Int
intSizeOf SVal
a
       mk :: Integer -> SVal
mk = Kind -> Integer -> SVal
svInteger forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded (forall a. HasKind a => a -> Bool
hasSign SVal
a) (Int
n forall a. Num a => a -> a -> a
- Int
sa)
       p :: SVal
p  = SVal -> SVal -> SVal -> SVal
svIte (SVal -> SVal
pos SVal
a) (Integer -> SVal
mk Integer
0) (Integer -> SVal
mk (-Integer
1))

-- | Get the sign-bit
signBit :: SVal -> SVal
signBit :: SVal -> SVal
signBit SVal
x = SVal
x SVal -> Int -> SVal
`svTestBit` (forall a. HasKind a => a -> Int
intSizeOf SVal
x forall a. Num a => a -> a -> a
- Int
1)

-- | Is the sign-bit high?
neg :: SVal -> SVal
neg :: SVal -> SVal
neg SVal
x = SVal -> SVal
signBit SVal
x SVal -> SVal -> SVal
`svEqual` SVal
svTrue

-- | Is the sign-bit low?
pos :: SVal -> SVal
pos :: SVal -> SVal
pos SVal
x = SVal -> SVal
signBit SVal
x SVal -> SVal -> SVal
`svEqual` SVal
svFalse

-- | Do these have the same sign?
sameSign :: SVal -> SVal -> SVal
sameSign :: SVal -> SVal -> SVal
sameSign SVal
x SVal
y = (SVal -> SVal
pos SVal
x SVal -> SVal -> SVal
`svAnd` SVal -> SVal
pos SVal
y) SVal -> SVal -> SVal
`svOr` (SVal -> SVal
neg SVal
x SVal -> SVal -> SVal
`svAnd` SVal -> SVal
neg SVal
y)

-- | Do these have opposing signs?
diffSign :: SVal -> SVal -> SVal
diffSign :: SVal -> SVal -> SVal
diffSign SVal
x SVal
y = SVal -> SVal
svNot (SVal -> SVal -> SVal
sameSign SVal
x SVal
y)

-- | Check all true
svAll :: [SVal] -> SVal
svAll :: [SVal] -> SVal
svAll = 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 forall a. Ord a => a -> a -> Bool
>= Int
sz Bool -> Bool -> Bool
|| Int
n forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
m forall a. Ord a => a -> a -> Bool
< Int
n
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Tools.Overflow.allZero: Received unexpected parameters: " forall a. [a] -> [a] -> [a]
++ 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
mforall a. Num a => a -> a -> a
-Int
1 .. Int
n]]
  where sz :: Int
sz = 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 forall a. Ord a => a -> a -> Bool
>= Int
sz Bool -> Bool -> Bool
|| Int
n forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
m forall a. Ord a => a -> a -> Bool
< Int
n
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.Tools.Overflow.allOne: Received unexpected parameters: " forall a. [a] -> [a] -> [a]
++ 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
mforall a. Num a => a -> a -> a
-Int
1 .. Int
n]]
  where sz :: Int
sz = forall a. HasKind a => a -> Int
intSizeOf SVal
x

-- | Unsigned addition. Can only overflow.
bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)
bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)
bvuaddo Int
n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse

        n' :: Int
n'       = Int
nforall a. Num a => a -> a -> a
+Int
1
        overflow :: SVal
overflow = SVal -> SVal
neg forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
zx Int
n' SVal
x SVal -> SVal -> SVal
`svPlus` Int -> SVal -> SVal
zx Int
n' SVal
y

-- | Signed addition.
bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsaddo Int
_n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = [SVal] -> SVal
svAll [SVal -> SVal
neg SVal
x, SVal -> SVal
neg SVal
y, SVal -> SVal
pos (SVal
x SVal -> SVal -> SVal
`svPlus` SVal
y)]
        overflow :: SVal
overflow  = [SVal] -> SVal
svAll [SVal -> SVal
pos SVal
x, SVal -> SVal
pos SVal
y, SVal -> SVal
neg (SVal
x SVal -> SVal -> SVal
`svPlus` SVal
y)]

-- | Unsigned subtraction. Can only underflow.
bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)
bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)
bvusubo Int
_n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
y SVal -> SVal -> SVal
`svGreaterThan` SVal
x
        overflow :: SVal
overflow  = SVal
svFalse

-- | Signed subtraction.
bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)
bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)
bvssubo Int
_n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = [SVal] -> SVal
svAll [SVal -> SVal
neg SVal
x, SVal -> SVal
pos SVal
y, SVal -> SVal
pos (SVal
x SVal -> SVal -> SVal
`svMinus` SVal
y)]
        overflow :: SVal
overflow  = [SVal] -> SVal
svAll [SVal -> SVal
pos SVal
x, SVal -> SVal
neg SVal
y, SVal -> SVal
neg (SVal
x SVal -> SVal -> SVal
`svMinus` SVal
y)]

-- | Unsigned multiplication. Can only overflow.
bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)
bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)
bvumulo Int
0 SVal
_ SVal
_ = (SVal
svFalse,   SVal
svFalse)
bvumulo Int
n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse

        n1 :: Int
n1        = Int
nforall a. Num a => a -> a -> a
+Int
1
        overflow1 :: SVal
overflow1 = SVal -> SVal
signBit forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
zx Int
n1 SVal
x SVal -> SVal -> SVal
`svTimes` Int -> SVal -> SVal
zx Int
n1 SVal
y

        -- From Z3 sources:
        --
        -- expr_ref ovf(m()), v(m()), tmp(m());
        -- ovf = m().mk_false();
        -- v = m().mk_false();
        -- for (unsigned i = 1; i < sz; ++i) {
        --    mk_or(ovf, a_bits[sz-i], ovf);
        --    mk_and(ovf, b_bits[i], tmp);
        --    mk_or(tmp, v, v);
        -- }
        -- overflow2 = v;
        --
        overflow2 :: SVal
overflow2 = Int -> SVal -> SVal -> SVal
go Int
1 SVal
svFalse SVal
svFalse
          where go :: Int -> SVal -> SVal -> SVal
go Int
i SVal
ovf SVal
v
                 | Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = SVal
v
                 | Bool
True   = Int -> SVal -> SVal -> SVal
go (Int
iforall a. Num a => a -> a -> a
+Int
1) SVal
ovf' SVal
v'
                 where ovf' :: SVal
ovf' = SVal
ovf  SVal -> SVal -> SVal
`svOr`  (SVal
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
i))
                       tmp :: SVal
tmp  = SVal
ovf' SVal -> SVal -> SVal
`svAnd` (SVal
y SVal -> Int -> SVal
`svTestBit` Int
i)
                       v' :: SVal
v'   = SVal
tmp SVal -> SVal -> SVal
`svOr` SVal
v

        overflow :: SVal
overflow = SVal
overflow1 SVal -> SVal -> SVal
`svOr` SVal
overflow2

-- | Signed multiplication.
bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsmulo Int
0 SVal
_ SVal
_ = (SVal
svFalse,   SVal
svFalse)
bvsmulo Int
n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal -> SVal -> SVal
diffSign SVal
x SVal
y SVal -> SVal -> SVal
`svAnd` SVal
overflowPossible
        overflow :: SVal
overflow  = SVal -> SVal -> SVal
sameSign SVal
x SVal
y SVal -> SVal -> SVal
`svAnd` SVal
overflowPossible

        n1 :: Int
n1        = Int
nforall a. Num a => a -> a -> a
+Int
1
        overflow1 :: SVal
overflow1 = (SVal
xy1 SVal -> Int -> SVal
`svTestBit` Int
n) SVal -> SVal -> SVal
`svXOr` (SVal
xy1 SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1))
           where xy1 :: SVal
xy1 = Int -> SVal -> SVal
sx Int
n1 SVal
x SVal -> SVal -> SVal
`svTimes` Int -> SVal -> SVal
sx Int
n1 SVal
y

        -- From Z3 sources:
        -- expr_ref v(m()), tmp(m()), a(m()), b(m()), a_acc(m()), sign(m());
        -- a_acc = m().mk_false();
        -- v = m().mk_false();
        -- for (unsigned i = 1; i + 1 < sz; ++i) {
        --    mk_xor(b_bits[sz-1], b_bits[i], b);
        --    mk_xor(a_bits[sz-1], a_bits[sz-1-i], a);
        --    mk_or(a, a_acc, a_acc);
        --    mk_and(a_acc, b, tmp);
        --    mk_or(tmp, v, v);
        -- }
        -- overflow2 = v;
        overflow2 :: SVal
overflow2 = Int -> SVal -> SVal -> SVal
go Int
1 SVal
svFalse SVal
svFalse
           where sY :: SVal
sY = SVal -> SVal
signBit SVal
y
                 sX :: SVal
sX = SVal -> SVal
signBit SVal
x
                 go :: Int -> SVal -> SVal -> SVal
go Int
i SVal
v SVal
a_acc
                  | Int
i forall a. Num a => a -> a -> a
+ Int
1 forall a. Ord a => a -> a -> Bool
>= Int
n = SVal
v
                  | Bool
True       = Int -> SVal -> SVal -> SVal
go (Int
iforall a. Num a => a -> a -> a
+Int
1) SVal
v' SVal
a_acc'
                  where b :: SVal
b      = SVal
sY SVal -> SVal -> SVal
`svXOr` (SVal
y SVal -> Int -> SVal
`svTestBit` Int
i)
                        a :: SVal
a      = SVal
sX SVal -> SVal -> SVal
`svXOr` (SVal
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i))
                        a_acc' :: SVal
a_acc' = SVal
a SVal -> SVal -> SVal
`svOr` SVal
a_acc
                        tmp :: SVal
tmp    = SVal
a_acc' SVal -> SVal -> SVal
`svAnd` SVal
b
                        v' :: SVal
v'     = SVal
tmp SVal -> SVal -> SVal
`svOr` SVal
v

        overflowPossible :: SVal
overflowPossible = SVal
overflow1 SVal -> SVal -> SVal
`svOr` SVal
overflow2

-- | Is this a concrete value?
known :: SVal -> Bool
known :: SVal -> Bool
known (SVal Kind
_ (Left CV
_)) = Bool
True
known SVal
_                 = Bool
False

-- | Unsigned multiplication, fast version using z3 primitives.
bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
bvumuloFast Int
n SVal
x SVal
y
   | SVal -> Bool
known SVal
x Bool -> Bool -> Bool
&& SVal -> Bool
known SVal
y                         -- Not particularly fast, but avoids shipping of to the solver
   = Int -> SVal -> SVal -> (SVal, SVal)
bvumulo Int
n SVal
x SVal
y
   | Bool
True
   = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal -> (SVal, SVal)
bvumulo Int
n SVal
x SVal
y         -- No internal version for underflow exists (because it can't underflow)
        overflow :: SVal
overflow  = OvOp -> SVal -> SVal -> SVal
svMkOverflow OvOp
Overflow_UMul_OVFL SVal
x SVal
y

-- | Signed multiplication, fast version using z3 primitives.
bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
bvsmuloFast Int
n SVal
x SVal
y
  | SVal -> Bool
known SVal
x Bool -> Bool -> Bool
&& SVal -> Bool
known SVal
y                -- Not particularly fast, but avoids shipping of to the solver
  = Int -> SVal -> SVal -> (SVal, SVal)
bvsmulo Int
n SVal
x SVal
y
  | Bool
True
  = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = OvOp -> SVal -> SVal -> SVal
svMkOverflow OvOp
Overflow_SMul_UDFL SVal
x SVal
y
        overflow :: SVal
overflow  = OvOp -> SVal -> SVal -> SVal
svMkOverflow OvOp
Overflow_SMul_OVFL SVal
x SVal
y

-- | Unsigned division. Neither underflows, nor overflows.
bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)
bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)
bvudivo Int
_ SVal
_ SVal
_ = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse
        overflow :: SVal
overflow  = SVal
svFalse

-- | Signed division. Can only overflow.
bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)
bvsdivo Int
n SVal
x SVal
y = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse

        ones :: SVal
ones      = Kind -> Integer -> SVal
svInteger (Bool -> Int -> Kind
KBounded Bool
True Int
n) (-Integer
1)
        topSet :: SVal
topSet    = Kind -> Integer -> SVal
svInteger (Bool -> Int -> Kind
KBounded Bool
True Int
n) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
nforall a. Num a => a -> a -> a
-Int
1))

        overflow :: SVal
overflow = [SVal] -> SVal
svAll [SVal
x SVal -> SVal -> SVal
`svEqual` SVal
topSet, SVal
y SVal -> SVal -> SVal
`svEqual` SVal
ones]

-- | Unsigned negation. Neither underflows, nor overflows.
bvunego :: Int -> SVal -> (SVal, SVal)
bvunego :: Int -> SVal -> (SVal, SVal)
bvunego Int
_ SVal
_ = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse
        overflow :: SVal
overflow  = SVal
svFalse

-- | Signed negation. Can only overflow.
bvsnego :: Int -> SVal -> (SVal, SVal)
bvsnego :: Int -> SVal -> (SVal, SVal)
bvsnego Int
n SVal
x = (SVal
underflow, SVal
overflow)
  where underflow :: SVal
underflow = SVal
svFalse

        topSet :: SVal
topSet    = Kind -> Integer -> SVal
svInteger (Bool -> Int -> Kind
KBounded Bool
True Int
n) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
nforall a. Num a => a -> a -> a
-Int
1))
        overflow :: SVal
overflow  = SVal
x SVal -> SVal -> SVal
`svEqual` SVal
topSet

-- | 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 (forall a. HasKind a => a -> Kind
kindOf SBV a
x, forall a. HasKind a => a -> Kind
kindOf (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)              -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"sFromIntegralO: Expected bounded-BV types, received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
kFrom, Kind
kTo)

  where res :: SBV b
        res :: SBV b
res = 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 forall a. OrdSymbolic a => a -> a -> SBool
.< forall a. SymVal a => a -> SBV a
literal Integer
lb, SInteger
ix forall a. OrdSymbolic a => a -> a -> SBool
.> forall a. SymVal a => a -> SBV a
literal Integer
ub)
          where ix :: SInteger
                ix :: SInteger
ix = 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
sz

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

                lb :: Integer
                lb :: Integer
lb | Bool
signed = -Integer
ubforall 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 forall a. Ord a => a -> a -> Bool
<= Int
m = SBool
sFalse
                  | Bool
True   = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nforall 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 forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nforall a. Num a => a -> a -> a
-Int
1) (Int
mforall 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 = (forall {a}. SBV a
underflow, SBool
overflow)
          where underflow :: SBV a
underflow = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ (forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svTrue

                overflow :: SBool
overflow
                  | Int
m forall a. Ord a => a -> a -> Bool
>= Int
n forall a. Num a => a -> a -> a
- Int
1 = SBool
sFalse
                  | Bool
True       = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svFalse, SVal -> SVal
svNot forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nforall 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 forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svTrue,  SVal -> SVal
svNot forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> SBV a -> SVal
allOne  (Int
nforall a. Num a => a -> a -> a
-Int
1) (Int
mforall a. Num a => a -> a -> a
-Int
1) SBV a
x]

                overflow :: SBool
overflow
                  | Int
m forall a. Ord a => a -> a -> Bool
> Int
n = SBool
sFalse
                  | Bool
True  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal
svAll [(forall a. SBV a -> SVal
unSBV SBV a
x SVal -> Int -> SVal
`svTestBit` (Int
nforall a. Num a => a -> a -> a
-Int
1)) SVal -> SVal -> SVal
`svEqual` SVal
svFalse, SVal -> SVal
svNot forall a b. (a -> b) -> a -> b
$ forall a. Int -> Int -> SBV a -> SVal
allZero (Int
nforall a. Num a => a -> a -> a
-Int
1) (Int
mforall 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 = forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (forall a. a -> Maybe a
Just ?loc::CallStack
?loc) (String -> String
msg String
"underflows") (SBool -> SBool
sNot SBool
u)
                       forall a b. (a -> b) -> a -> b
$ forall a.
HasKind a =>
Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert (forall a. a -> Maybe a
Just ?loc::CallStack
?loc) (String -> String
msg String
"overflows")  (SBool -> SBool
sNot SBool
o)
                         SBV b
r
  where kFrom :: String
kFrom = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> Kind
kindOf SBV a
x
        kTo :: String
kTo   = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)
        msg :: String -> String
msg String
c = String
"Casting from " forall a. [a] -> [a] -> [a]
++ String
kFrom forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ String
kTo forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
c

        (SBV b
r, (SBool
u, SBool
o)) = 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


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

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

signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal)) -> (Int -> SVal -> SVal -> (SVal, SVal)) -> (SVal -> SVal -> (SBool, SBool))
signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal))
-> (Int -> SVal -> SVal -> (SVal, SVal))
-> SVal
-> SVal
-> (SBool, SBool)
signPick2 Int -> SVal -> SVal -> (SVal, SVal)
fu Int -> SVal -> SVal -> (SVal, SVal)
fs SVal
a SVal
b
 | forall a. HasKind a => a -> Bool
hasSign SVal
a = let (SVal
u, SVal
o) = Int -> SVal -> SVal -> (SVal, SVal)
fs Int
n SVal
a SVal
b in (forall a. SVal -> SBV a
SBV SVal
u, forall a. SVal -> SBV a
SBV SVal
o)
 | Bool
True      = let (SVal
u, SVal
o) = Int -> SVal -> SVal -> (SVal, SVal)
fu Int
n SVal
a SVal
b in (forall a. SVal -> SBV a
SBV SVal
u, forall a. SVal -> SBV a
SBV SVal
o)
 where n :: Int
n = forall a. HasKind a => a -> Int
intSizeOf SVal
a

signPick1 :: (Int -> SVal -> (SVal, SVal)) -> (Int -> SVal -> (SVal, SVal)) -> (SVal -> (SBool, SBool))
signPick1 :: (Int -> SVal -> (SVal, SVal))
-> (Int -> SVal -> (SVal, SVal)) -> SVal -> (SBool, SBool)
signPick1 Int -> SVal -> (SVal, SVal)
fu Int -> SVal -> (SVal, SVal)
fs SVal
a
 | forall a. HasKind a => a -> Bool
hasSign SVal
a = let (SVal
u, SVal
o) = Int -> SVal -> (SVal, SVal)
fs Int
n SVal
a in (forall a. SVal -> SBV a
SBV SVal
u, forall a. SVal -> SBV a
SBV SVal
o)
 | Bool
True      = let (SVal
u, SVal
o) = Int -> SVal -> (SVal, SVal)
fu Int
n SVal
a in (forall a. SVal -> SBV a
SBV SVal
u, forall a. SVal -> SBV a
SBV SVal
o)
 where n :: Int
n = forall a. HasKind a => a -> Int
intSizeOf SVal
a

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

        (SBool
u, SBool
o) = a -> (SBool, SBool)
cop a
a

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

        (SBool
u, SBool
o) = a
a a -> b -> (SBool, SBool)
`cop` b
b