1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Arrays.Query
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for query mode arrays
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Arrays.Query(tests) where
import Data.SBV.Control
import Utils.SBVTestFramework
-- Test suite
tests :: TestTree
tests =
testGroup "Arrays.Query"
[ goldenCapturedIO "queryArrays1" $ t q1
, goldenCapturedIO "queryArrays2" $ t q2
, goldenCapturedIO "queryArrays3" $ t q3
, goldenCapturedIO "queryArrays4" $ t q4
, goldenCapturedIO "queryArrays5" $ t q5
, goldenCapturedIO "queryArrays6" $ t q6
, goldenCapturedIO "queryArrays7" $ t q7
, goldenCapturedIO "queryArrays8" $ t q8
]
where t tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc
appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n")
q1 :: Symbolic (Word8, Word8, Int8)
q1 = do m :: SArray Word8 Int8 <- newArray "a" Nothing
a1 <- sWord8 "a1"
a2 <- sWord8 "a2"
constrain $ a1 ./= a2
v1 <- sInt8 "v1"
query $ do constrain $ v1 .== readArray (writeArray m a1 v1) a1
_ <- checkSat
va1 <- getValue a1
va2 <- getValue a2
vv1 <- getValue v1
return (va1, va2, vv1)
q2 :: Symbolic Word8
q2 = do i <- sWord8 "i"
setLogic QF_UFBV
query $ do constrain $ i .== select [0 .. 255] 0 i
_ <- checkSat
getValue i
q3 :: Symbolic Word8
q3 = do i <- sWord8 "i"
setLogic QF_UFBV
query $ do constrain $ i .== select (replicate 256 i) 0 i
_ <- checkSat
getValue i
q4 :: Symbolic (Word8, Word8)
q4 = do i <- sWord8 "i"
j <- sWord8 "j"
setLogic QF_UFBV
query $ do constrain $ i .== select [0 .. 255] 0 i
_ <- checkSat
iv <- getValue i
constrain $ j .== select [0 .. 255] 0 j
constrain $ i .== literal iv
constrain $ j .== i+1
_ <- checkSat
jv <- getValue j
return (iv, jv)
q5 :: Symbolic (Maybe (Word8, Int8))
q5 = do m :: SArray Word8 Int8 <- newArray "a" Nothing
a <- sWord8 "a"
v <- sInt8 "v"
query $ do let m2 = writeArray (writeArray m a v) (a+1) (v+1)
vRead = readArray m2 (a+1)
constrain $ v + 1 ./= vRead
cs <- checkSat
case cs of
Unsat -> return Nothing
Unk -> error "solver returned Unknown!"
DSat{} -> error "solver returned Delta-satisfiable!"
Sat -> do av <- getValue a
vv <- getValue v
return $ Just (av, vv)
q6 :: Symbolic [Integer]
q6 = do (a :: SArray Integer Integer) <- newArray "a" Nothing
query $ loop (writeArray a 1 1) []
where loop a sofar = do push 1
constrain $ readArray a 1 .== 5
cs <- checkSat
case cs of
Unk -> error "Unknown"
Unsat -> do pop 1
d <- freshVar $ "d" ++ show (length sofar)
constrain $ d .>= 1 .&& d .< 3
loop (writeArray a 1 (readArray a 1 + d)) (sofar ++ [d])
DSat{} -> error "solver returned Delta-satisfiable!"
Sat -> mapM getValue sofar
q7 :: Symbolic (CheckSatResult, CheckSatResult)
q7 = do x :: SArray Integer Integer <- newArray "x" Nothing
let y = writeArray x 0 1
query $ do constrain $ readArray y 0 .== 2
r1 <- checkSat
resetAssertions
constrain $ readArray y 0 .== 2
r2 <- checkSat
pure (r1, r2)
q8 :: Symbolic (CheckSatResult, CheckSatResult)
q8 = query $ do x :: SArray Integer Integer <- freshArray "x" Nothing
let y = writeArray x 0 1
constrain $ readArray y 0 .== 2
r1 <- checkSat
resetAssertions
constrain $ readArray y 0 .== 2
r2 <- checkSat
pure (r1, r2)
{- HLint ignore module "Reduce duplication" -}
|
