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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
|
-----------------------------------------------------------------------------
-- |
-- Module : SBVTest
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Main entry point to the test suite
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Main(main) where
import Test.Tasty
import qualified TestSuite.Arrays.InitVals
import qualified TestSuite.Arrays.Memory
import qualified TestSuite.Arrays.Query
import qualified TestSuite.Arrays.Caching
import qualified TestSuite.Basics.AllSat
import qualified TestSuite.Basics.ArbFloats
import qualified TestSuite.Basics.ArithNoSolver
import qualified TestSuite.Basics.ArithSolver
import qualified TestSuite.Basics.Assert
import qualified TestSuite.Basics.BasicTests
import qualified TestSuite.Basics.BarrelRotate
import qualified TestSuite.Basics.BoundedList
import qualified TestSuite.Basics.DynSign
import qualified TestSuite.Basics.Exceptions
import qualified TestSuite.Basics.EqSym
import qualified TestSuite.Basics.GenBenchmark
import qualified TestSuite.Basics.Higher
import qualified TestSuite.Basics.Index
import qualified TestSuite.Basics.IteTest
import qualified TestSuite.Basics.Lambda
import qualified TestSuite.Basics.List
import qualified TestSuite.Basics.ModelValidate
import qualified TestSuite.Basics.Nonlinear
import qualified TestSuite.Basics.ProofTests
import qualified TestSuite.Basics.PseudoBoolean
import qualified TestSuite.Basics.QRem
import qualified TestSuite.Basics.Quantifiers
import qualified TestSuite.Basics.Recursive
import qualified TestSuite.Basics.Set
import qualified TestSuite.Basics.SmallShifts
import qualified TestSuite.Basics.SquashReals
import qualified TestSuite.Basics.String
import qualified TestSuite.Basics.Sum
import qualified TestSuite.Basics.TOut
import qualified TestSuite.Basics.Tuple
import qualified TestSuite.Basics.UISat
import qualified TestSuite.BitPrecise.BitTricks
import qualified TestSuite.BitPrecise.Legato
import qualified TestSuite.BitPrecise.MergeSort
import qualified TestSuite.BitPrecise.PrefixSum
import qualified TestSuite.CantTypeCheck.Misc
import qualified TestSuite.Char.Char
import qualified TestSuite.CodeGeneration.AddSub
import qualified TestSuite.CodeGeneration.CgTests
import qualified TestSuite.CodeGeneration.CRC_USB5
import qualified TestSuite.CodeGeneration.Fibonacci
import qualified TestSuite.CodeGeneration.Floats
import qualified TestSuite.CodeGeneration.GCD
import qualified TestSuite.CodeGeneration.PopulationCount
import qualified TestSuite.CodeGeneration.Uninterpreted
import qualified TestSuite.CRC.CCITT
import qualified TestSuite.CRC.CCITT_Unidir
import qualified TestSuite.CRC.GenPoly
import qualified TestSuite.CRC.Parity
import qualified TestSuite.CRC.USB5
import qualified TestSuite.Crypto.AES
import qualified TestSuite.Crypto.RC4
import qualified TestSuite.Crypto.SHA
import qualified TestSuite.Existentials.CRCPolynomial
import qualified TestSuite.GenTest.GenTests
import qualified TestSuite.Optimization.AssertWithPenalty
import qualified TestSuite.Optimization.Basics
import qualified TestSuite.Optimization.Combined
import qualified TestSuite.Optimization.ExtensionField
import qualified TestSuite.Optimization.Floats
import qualified TestSuite.Optimization.NoOpt
import qualified TestSuite.Optimization.Quantified
import qualified TestSuite.Optimization.Reals
import qualified TestSuite.Optimization.Tuples
import qualified TestSuite.Overflows.Arithmetic
import qualified TestSuite.Overflows.Casts
import qualified TestSuite.Polynomials.Polynomials
import qualified TestSuite.Puzzles.Coins
import qualified TestSuite.Puzzles.Counts
import qualified TestSuite.Puzzles.DogCatMouse
import qualified TestSuite.Puzzles.Euler185
import qualified TestSuite.Puzzles.MagicSquare
import qualified TestSuite.Puzzles.NQueens
import qualified TestSuite.Puzzles.PowerSet
import qualified TestSuite.Puzzles.Sudoku
import qualified TestSuite.Puzzles.Temperature
import qualified TestSuite.Puzzles.U2Bridge
import qualified TestSuite.Queries.BasicQuery
import qualified TestSuite.Queries.BadOption
import qualified TestSuite.Queries.DSat
import qualified TestSuite.Queries.Enums
import qualified TestSuite.Queries.FreshVars
import qualified TestSuite.Queries.Int_ABC
import qualified TestSuite.Queries.Int_Boolector
import qualified TestSuite.Queries.Int_CVC4
import qualified TestSuite.Queries.Int_Mathsat
import qualified TestSuite.Queries.Int_Yices
import qualified TestSuite.Queries.Int_Z3
import qualified TestSuite.Queries.Interpolants
import qualified TestSuite.Queries.Lists
import qualified TestSuite.Queries.Strings
import qualified TestSuite.Queries.Sums
import qualified TestSuite.Queries.Tables
import qualified TestSuite.Queries.Tuples
import qualified TestSuite.Queries.UISat
import qualified TestSuite.Queries.UISatEx
import qualified TestSuite.Queries.Uninterpreted
import qualified TestSuite.QuickCheck.QC
import qualified TestSuite.Transformers.SymbolicEval
import qualified TestSuite.Uninterpreted.AUF
import qualified TestSuite.Uninterpreted.Axioms
import qualified TestSuite.Uninterpreted.Function
import qualified TestSuite.Uninterpreted.Sort
import qualified TestSuite.Uninterpreted.Uninterpreted
main :: IO ()
main = defaultMain $ testGroup "SBV" [
TestSuite.Arrays.InitVals.tests
, TestSuite.Arrays.Memory.tests
, TestSuite.Arrays.Query.tests
, TestSuite.Arrays.Caching.tests
, TestSuite.Basics.AllSat.tests
, TestSuite.Basics.ArbFloats.tests
, TestSuite.Basics.ArithNoSolver.tests
, TestSuite.Basics.ArithSolver.tests
, TestSuite.Basics.Assert.tests
, TestSuite.Basics.BarrelRotate.tests
, TestSuite.Basics.BasicTests.tests
, TestSuite.Basics.BoundedList.tests
, TestSuite.Basics.DynSign.tests
, TestSuite.Basics.EqSym.tests
, TestSuite.Basics.Exceptions.testsLocal
, TestSuite.Basics.Exceptions.testsRemote
, TestSuite.Basics.GenBenchmark.tests
, TestSuite.Basics.Higher.tests
, TestSuite.Basics.Index.tests
, TestSuite.Basics.IteTest.tests
, TestSuite.Basics.Lambda.tests
, TestSuite.Basics.List.tests
, TestSuite.Basics.ModelValidate.tests
, TestSuite.Basics.ModelValidate.testsABC
, TestSuite.Basics.Nonlinear.tests
, TestSuite.Basics.ProofTests.tests
, TestSuite.Basics.PseudoBoolean.tests
, TestSuite.Basics.QRem.tests
, TestSuite.Basics.Quantifiers.tests
, TestSuite.Basics.Recursive.tests
, TestSuite.Basics.Set.tests
, TestSuite.Basics.SmallShifts.tests
, TestSuite.Basics.SquashReals.tests
, TestSuite.Basics.String.tests
, TestSuite.Basics.Sum.tests
, TestSuite.Basics.TOut.tests
, TestSuite.Basics.Tuple.tests
, TestSuite.Basics.UISat.tests
, TestSuite.BitPrecise.BitTricks.tests
, TestSuite.BitPrecise.Legato.tests
, TestSuite.BitPrecise.MergeSort.tests
, TestSuite.BitPrecise.PrefixSum.tests
, TestSuite.CantTypeCheck.Misc.tests
, TestSuite.Char.Char.tests
, TestSuite.CodeGeneration.AddSub.tests
, TestSuite.CodeGeneration.CgTests.tests
, TestSuite.CodeGeneration.CRC_USB5.tests
, TestSuite.CodeGeneration.Fibonacci.tests
, TestSuite.CodeGeneration.Floats.tests
, TestSuite.CodeGeneration.GCD.tests
, TestSuite.CodeGeneration.PopulationCount.tests
, TestSuite.CodeGeneration.Uninterpreted.tests
, TestSuite.CRC.CCITT.tests
, TestSuite.CRC.CCITT_Unidir.tests
, TestSuite.CRC.GenPoly.tests
, TestSuite.CRC.Parity.tests
, TestSuite.CRC.USB5.tests
, TestSuite.Crypto.AES.tests
, TestSuite.Crypto.RC4.tests
, TestSuite.Crypto.SHA.tests
, TestSuite.Existentials.CRCPolynomial.tests
, TestSuite.GenTest.GenTests.tests
, TestSuite.Optimization.AssertWithPenalty.tests
, TestSuite.Optimization.Basics.tests
, TestSuite.Optimization.Combined.tests
, TestSuite.Optimization.ExtensionField.tests
, TestSuite.Optimization.Floats.tests
, TestSuite.Optimization.NoOpt.tests
, TestSuite.Optimization.Tuples.tests
, TestSuite.Optimization.Quantified.tests
, TestSuite.Optimization.Reals.tests
, TestSuite.Overflows.Arithmetic.tests
, TestSuite.Overflows.Casts.tests
, TestSuite.Polynomials.Polynomials.tests
, TestSuite.Puzzles.Coins.tests
, TestSuite.Puzzles.Counts.tests
, TestSuite.Puzzles.DogCatMouse.tests
, TestSuite.Puzzles.Euler185.tests
, TestSuite.Puzzles.MagicSquare.tests
, TestSuite.Puzzles.NQueens.tests
, TestSuite.Puzzles.PowerSet.tests
, TestSuite.Puzzles.Sudoku.tests
, TestSuite.Puzzles.Temperature.tests
, TestSuite.Puzzles.U2Bridge.tests
, TestSuite.Queries.BadOption.tests
, TestSuite.Queries.BasicQuery.tests
, TestSuite.Queries.DSat.tests
, TestSuite.Queries.Interpolants.tests
, TestSuite.Queries.Enums.tests
, TestSuite.Queries.FreshVars.tests
, TestSuite.Queries.Int_Z3.tests
, TestSuite.Queries.Int_ABC.tests
, TestSuite.Queries.Int_Boolector.tests
, TestSuite.Queries.Int_CVC4.tests
, TestSuite.Queries.Int_Mathsat.tests
, TestSuite.Queries.Int_Yices.tests
, TestSuite.Queries.Lists.tests
, TestSuite.Queries.Strings.tests
, TestSuite.Queries.Sums.tests
, TestSuite.Queries.Tables.tests
, TestSuite.Queries.Tuples.tests
, TestSuite.Queries.UISat.tests
, TestSuite.Queries.UISatEx.tests
, TestSuite.Queries.Uninterpreted.tests
, TestSuite.QuickCheck.QC.tests
, TestSuite.Transformers.SymbolicEval.tests
, TestSuite.Uninterpreted.AUF.tests
, TestSuite.Uninterpreted.Axioms.tests
, TestSuite.Uninterpreted.Function.tests
, TestSuite.Uninterpreted.Sort.tests
, TestSuite.Uninterpreted.Uninterpreted.tests
]
|
