SmallShifts.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  TestSuite.Basics.SmallShift
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Testing small-shift amounts using the dynamic interface. See
-- https://github.com/LeventErkok/sbv/issues/323 for the genesis.
-----------------------------------------------------------------------------

module TestSuite.Basics.SmallShifts(tests) where

import Utils.SBVTestFramework hiding (proveWith)

import Control.Monad.Reader (ask)
import Control.Monad.Trans  (liftIO)
import Data.SBV.Dynamic

k1, k32, k33 :: Kind
k1   = KBounded False  1
k32  = KBounded False 32
k33  = KBounded False 33
type SW32 = SVal
type SW33 = SVal
type SW1  = SVal

b0 :: SW1
b0 = svInteger k1 0

b1 :: SW1
b1 = svInteger k1 1

average33 :: SW32 -> SW32 -> SW32
average33 x y = svExtract 31 0 (z' `svDivide` svInteger k33 2)
    where z' :: SW33
          z' = (b0 `svJoin` x) `svPlus` (b0 `svJoin` y)

average4 :: SW32 -> SW32 -> SW32
average4 x y =   ((x `svShiftRight` b1) `svPlus` (y `svShiftRight` b1))
                `svPlus` (x `svAnd` (y `svAnd` svInteger k32 1))

prop :: Symbolic SVal
prop = do x <- ask >>= liftIO . svMkSymVar Nothing k32 (Just "x")
          y <- ask >>= liftIO . svMkSymVar Nothing k32 (Just "y")
          return $ average33 x y `svEqual` average4 x y

checkThm :: ThmResult -> Assertion
checkThm r = assert isThm
  where isThm = case r of
                  ThmResult Unsatisfiable{} -> return True :: IO Bool
                  ThmResult Satisfiable{}   -> return False
                  _                         -> error "checkThm: Unexpected result!"

-- Test suite
tests :: TestTree
tests = testGroup "Basics.SmallShifts"
   [ testCase "smallShift" $ checkThm =<< proveWith z3 prop
   ]