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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Basics.Set
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test sets.
-----------------------------------------------------------------------------
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Basics.Set (tests) where
import Data.SBV hiding (complement)
import Data.SBV.Set
import Data.SBV.Control
import Data.SBV.Tuple
import Utils.SBVTestFramework hiding (complement)
data E = A | B | C
mkSymbolicEnumeration ''E
__unused :: SE
__unused = error "stop GHC from complaining unused names" sA sB sC
type SC = SSet Integer
type RC = RCSet Integer
cSetAL :: SC
cSetAL = fromList [1,2,3,3,4]
cIntA :: SInteger
cIntA = literal 2
cSetA :: SC
cSetA = singleton $ literal 0
-- Test suite
tests :: TestTree
tests = testGroup "Basics.Set" [
goldenCapturedIO "set_uninterp1" $ ta setE1
, goldenCapturedIO "set_uninterp2" $ tq setE2
, goldenCapturedIO "set_compl1" $ tq $ templateU cSetAL complement
, goldenCapturedIO "set_union1" $ tq $ templateB cSetA cSetA union
, goldenCapturedIO "set_intersect1" $ tq $ templateB cSetA cSetA intersection
, goldenCapturedIO "set_diff1" $ tq $ templateB cSetA cSetA difference
, goldenCapturedIO "set_empty1" $ tq $ templateUB cSetAL isEmpty
, goldenCapturedIO "set_full1" $ tq $ templateUB cSetAL isFull
, goldenCapturedIO "set_subset1" $ tq $ templateBB cSetA cSetA isSubsetOf
, goldenCapturedIO "set_psubset1" $ tq $ templateBB cSetA cSetA isProperSubsetOf
, goldenCapturedIO "set_disj1" $ tq $ templateBB cSetA cSetA disjoint
, goldenCapturedIO "set_insert1" $ tq $ templateBE cIntA cSetAL insert
, goldenCapturedIO "set_delete1" $ tq $ templateBE cIntA cSetAL delete
, goldenCapturedIO "set_member1" $ tq $ templateBEB cIntA cSetAL member
, goldenCapturedIO "set_notMember1" $ tq $ templateBEB cIntA cSetAL notMember
, goldenCapturedIO "set_tupleSet" $ ta setOfTuples
]
where ta tc goldFile = record goldFile =<< tc defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile}
tq tc goldFile = record goldFile =<< runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc
record goldFile r = appendFile goldFile ("\nFINAL:\n" ++ show r ++ "\nDONE!\n")
setE1 :: SMTConfig -> IO AllSatResult
setE1 cfg = allSatWith cfg $ \(_ :: SSet E) -> sTrue
setE2 :: Symbolic (RCSet E, RCSet E)
setE2 = do a :: SSet E <- sSet "a"
b :: SSet E <- sSet "b"
constrain $ distinct [a, b]
query $ do ensureSat
(,) <$> getValue a <*> getValue b
templateU :: SC -> (SC -> SC) -> Symbolic (RC, RC, RC, RC, RC)
templateU is f = do a <- sSet "a"
constrain $ a .== is
let o1 = f a
o2 = f o1
o3 = o1 `intersection` a
o4 = o1 `union` a
query $ do ensureSat
(,,,,) <$> getValue a <*> getValue o1 <*> getValue o2 <*> getValue o3 <*> getValue o4
templateB :: SC -> SC -> (SC -> SC -> SC) -> Symbolic (RC, RC, RC, RC, RC, RC)
templateB is1 is2 f = do a <- sSet "a"
b <- sSet "b"
constrain $ a .== is1
constrain $ b .== is2
let o1 = a `f` b
o2 = a `f` complement b
o3 = complement a `f` b
o4 = complement a `f` complement b
query $ do ensureSat
(,,,,,) <$> getValue a <*> getValue b <*> getValue o1 <*> getValue o2 <*> getValue o3 <*> getValue o4
templateUB :: SC -> (SC -> SBool) -> Symbolic (RC, Bool, Bool)
templateUB is f = do a <- sSet "a"
constrain $ a .== is
let o1 = f a
o2 = f (complement a)
query $ do ensureSat
(,,) <$> getValue a <*> getValue o1 <*> getValue o2
templateBB :: SC -> SC -> (SC -> SC -> SBool) -> Symbolic (RC, RC, Bool, Bool, Bool, Bool)
templateBB is1 is2 f = do a <- sSet "a"
b <- sSet "b"
constrain $ a .== is1
constrain $ b .== is2
let o1 = a `f` b
o2 = a `f` complement b
o3 = complement a `f` b
o4 = complement a `f` complement b
query $ do ensureSat
(,,,,,) <$> getValue a <*> getValue b <*> getValue o1 <*> getValue o2 <*> getValue o3 <*> getValue o4
templateBE :: SInteger -> SC -> (SInteger -> SC -> SC) -> Symbolic (Integer, RC, RC, RC)
templateBE ic is f = do a <- sInteger "a"
b <- sSet "b"
constrain $ a .== ic
constrain $ b .== is
let o1 = a `f` b
o2 = a `f` complement b
query $ do ensureSat
(,,,) <$> getValue a <*> getValue b <*> getValue o1 <*> getValue o2
templateBEB :: SInteger -> SC -> (SInteger -> SC -> SBool) -> Symbolic (Integer, RC, Bool, Bool)
templateBEB ic is f = do a <- sInteger "a"
b <- sSet "b"
constrain $ a .== ic
constrain $ b .== is
let o1 = a `f` b
o2 = a `f` complement b
query $ do ensureSat
(,,,) <$> getValue a <*> getValue b <*> getValue o1 <*> getValue o2
setOfTuples :: SMTConfig -> IO SatResult
setOfTuples cfg = satWith cfg $ do
let x = tuple (empty :: SSet Bool, empty :: SSet Bool)
y <- free_
return $ x ./= y
{- HLint ignore module "Reduce duplication" -}
|
