sbv-14.1: SBVTestSuite/TestSuite/Arrays/InitVals.hs
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Arrays.InitVals
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing arrays with initializers
-----------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Arrays.InitVals(tests) where
import Data.SBV
import Utils.SBVTestFramework
readDef :: Predicate
readDef = do c :: SInteger <- free "c"
i :: SInteger <- free "i"
j <- free "j"
let a = constArray c
let a' = writeArray a j 32
return $ ite (i ./= j) (readArray a' i .== c)
(readArray a' i .== 32)
readNoDef :: Predicate
readNoDef = do i :: SInteger <- free "i"
j :: SInteger <- free "j"
a <- sArray_
return $ readArray a i .== j
constArr :: Predicate
constArr = do i :: SInteger <- sInteger "i"
j :: SInteger <- sInteger "j"
constrain $ i .< j
constrain $ i `sElem` [1, 2, 3, 75]
pure $ readArray myArray i .== readArray myArray j
where myArray = listArray [(1, 12), (2, 5) , (3, 6), (75, 5)] (7 :: Integer)
constArr2 :: Predicate
constArr2 = do i :: SInteger <- sInteger "i"
j :: SInteger <- sInteger "j"
constrain $ i .< j
constrain $ i `sElem` [1, 2, 3, 75]
pure $ readArray myArray i .== readArray myArray j
where myArray = listArray [(1, 12), (2, 5) , (3, 6), (75, 5)] (2 :: Integer)
tests :: TestTree
tests = testGroup "Arrays" [
testGroup "Arrays.InitVals"
[ testCase "readDef_SArray" $ assertIsThm readDef
, testCase "readDef2_SArray2" $ assertIsSat readNoDef
, goldenCapturedIO "constArr_SArray" $ t satWith constArr
, goldenCapturedIO "constArr2_SArray" $ t satWith constArr2
]
, testGroup "Arrays.Misc"
[ goldenCapturedIO "array_misc_1" $ t proveWith $ \i -> readArray (listArray [(True,1),(False,0)] 3) i .<= (1::SInteger)
, goldenCapturedIO "array_misc_2" $ t satWith $ \(x :: SArray Integer Integer) i1 i2 i3 ->
readArray x i1 .== 4 .&& readArray x i2 .== 5 .&& readArray x i3 .== 12
, goldenCapturedIO "array_misc_3" $ t proveWith $ write (empty False) [(True, True), (False, False)]
.== write (empty True) [(True, True), (False, False)]
, testCase "array_misc_4" $ (write (empty False) [(True, True), (False, False)]
.== write (empty True) [(True, True), (False, False)]) `showsAs` "True"
-- Interestingly, z3 says UNKNOWN if the logic below isn't set to ALL.
, goldenCapturedIO "array_misc_5" $ t proveWith $ do setLogic Logic_ALL
pure ( write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) :: Symbolic SBool
, testCase "array_misc_6" $ (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "<symbolic> :: SBool"
, goldenCapturedIO "array_misc_7" $ t proveWith $ write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
, testCase "array_misc_8" $ (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "True"
, goldenCapturedIO "array_misc_9" $ t proveWith $ write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
, testCase "array_misc_10" $ (write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 0) [(i, i ) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "False"
, goldenCapturedIO "array_misc_11" $ t satWith $ \(a :: SArray (Integer, Integer) Integer) -> readArray a (literal (1, 2)) .== 3
, goldenCapturedIO "array_misc_12" $ t satWith $ \(a :: SArray Integer (Integer, Integer)) -> readArray a 3 .== literal (1, 2)
, goldenCapturedIO "array_misc_13" $ t satWith $ \(a :: SArray (Integer, Integer) (Integer, Integer)) -> readArray a (literal (1, 2)) .== literal (1, 2)
, goldenCapturedIO "array_misc_14" $ t satWith $ \(a :: SArray Integer Float) -> fpIsNaN (readArray a 2)
, goldenCapturedIO "array_misc_15" $ t satWith $ \(a :: SArray Float Integer) -> readArray a (0/0) .== 3
, goldenCapturedIO "array_misc_16" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Float Integer) 0)
, goldenCapturedIO "array_misc_17" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Double Integer) 0)
, goldenCapturedIO "array_misc_18" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (0 :: SFloatingPoint 10 4))
, goldenCapturedIO "array_misc_19" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Float Integer) (-0))
, goldenCapturedIO "array_misc_20" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Double Integer) (-0))
, goldenCapturedIO "array_misc_21" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-(0 :: SFloatingPoint 10 4)))
, goldenCapturedIO "array_misc_22" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray Float Integer) (0/0))
, goldenCapturedIO "array_misc_23" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray Double Integer) (0/0))
, goldenCapturedIO "array_misc_24" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (0/0))
, goldenCapturedIO "array_misc_25" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float Integer) (1/0))
, goldenCapturedIO "array_misc_26" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double Integer) (1/0))
, goldenCapturedIO "array_misc_27" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (1/0))
, goldenCapturedIO "array_misc_28" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float Integer) (-(1/0)))
, goldenCapturedIO "array_misc_29" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double Integer) (-(1/0)))
, goldenCapturedIO "array_misc_30" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-(1/0)))
, goldenCapturedIO "array_misc_31" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Integer))
]
]
where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
empty :: (SymVal a, SymVal b) => b -> SArray a b
empty = listArray []
write :: (SymVal a, SymVal b) => SArray a b -> [(a, b)] -> SArray a b
write = foldr (\(k, v) a -> writeArray a (literal k) (literal v))
{- HLint ignore module "Reduce duplication" -}