1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Morgan Deters, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Unit testing for cvc5::LogicInfo class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "base/configuration.h" |
17 |
|
#include "expr/kind.h" |
18 |
|
#include "test.h" |
19 |
|
#include "theory/logic_info.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
|
23 |
|
using namespace theory; |
24 |
|
|
25 |
|
namespace test { |
26 |
|
|
27 |
12 |
class TestTheoryWhiteLogicInfo : public TestInternal |
28 |
|
{ |
29 |
|
// This test is of questionable compatiblity with contrib/new-theory. Is the |
30 |
|
// new theory id handled correctly by the Logic info. |
31 |
|
protected: |
32 |
48 |
void eq(const LogicInfo& logic1, const LogicInfo& logic2) const |
33 |
|
{ |
34 |
48 |
std::cout << "asserting that " << logic1 << " == " << logic2 << std::endl; |
35 |
|
|
36 |
48 |
ASSERT_TRUE(logic1 == logic2); |
37 |
48 |
ASSERT_FALSE((logic1 != logic2)); |
38 |
48 |
ASSERT_FALSE((logic1 < logic2)); |
39 |
48 |
ASSERT_FALSE((logic1 > logic2)); |
40 |
48 |
ASSERT_TRUE(logic1 <= logic2); |
41 |
48 |
ASSERT_TRUE(logic1 >= logic2); |
42 |
48 |
ASSERT_TRUE(logic1.isComparableTo(logic2)); |
43 |
|
|
44 |
48 |
ASSERT_TRUE(logic2 == logic1); |
45 |
48 |
ASSERT_FALSE((logic2 != logic1)); |
46 |
48 |
ASSERT_FALSE((logic2 < logic1)); |
47 |
48 |
ASSERT_FALSE((logic2 > logic1)); |
48 |
48 |
ASSERT_TRUE(logic2 <= logic1); |
49 |
48 |
ASSERT_TRUE(logic2 >= logic1); |
50 |
48 |
ASSERT_TRUE(logic2.isComparableTo(logic1)); |
51 |
|
} |
52 |
|
|
53 |
688 |
void nc(const LogicInfo& logic1, const LogicInfo& logic2) const |
54 |
|
{ |
55 |
688 |
std::cout << "asserting that " << logic1 << " is-not-comparable-to " |
56 |
688 |
<< logic2 << std::endl; |
57 |
688 |
ASSERT_FALSE((logic1 == logic2)); |
58 |
688 |
ASSERT_TRUE(logic1 != logic2); |
59 |
688 |
ASSERT_FALSE((logic1 < logic2)); |
60 |
688 |
ASSERT_FALSE((logic1 > logic2)); |
61 |
688 |
ASSERT_FALSE((logic1 <= logic2)); |
62 |
688 |
ASSERT_FALSE((logic1 >= logic2)); |
63 |
688 |
ASSERT_FALSE(logic1.isComparableTo(logic2)); |
64 |
|
|
65 |
688 |
ASSERT_FALSE((logic2 == logic1)); |
66 |
688 |
ASSERT_TRUE(logic2 != logic1); |
67 |
688 |
ASSERT_FALSE((logic2 < logic1)); |
68 |
688 |
ASSERT_FALSE((logic2 > logic1)); |
69 |
688 |
ASSERT_FALSE((logic2 <= logic1)); |
70 |
688 |
ASSERT_FALSE((logic2 >= logic1)); |
71 |
688 |
ASSERT_FALSE(logic2.isComparableTo(logic1)); |
72 |
|
} |
73 |
|
|
74 |
222 |
void lt(const LogicInfo& logic1, const LogicInfo& logic2) const |
75 |
|
{ |
76 |
222 |
std::cout << "asserting that " << logic1 << " < " << logic2 << std::endl; |
77 |
|
|
78 |
222 |
ASSERT_FALSE((logic1 == logic2)); |
79 |
222 |
ASSERT_TRUE(logic1 != logic2); |
80 |
222 |
ASSERT_TRUE(logic1 < logic2); |
81 |
222 |
ASSERT_FALSE((logic1 > logic2)); |
82 |
222 |
ASSERT_TRUE(logic1 <= logic2); |
83 |
222 |
ASSERT_FALSE((logic1 >= logic2)); |
84 |
222 |
ASSERT_TRUE(logic1.isComparableTo(logic2)); |
85 |
|
|
86 |
222 |
ASSERT_FALSE((logic2 == logic1)); |
87 |
222 |
ASSERT_TRUE(logic2 != logic1); |
88 |
222 |
ASSERT_FALSE((logic2 < logic1)); |
89 |
222 |
ASSERT_TRUE(logic2 > logic1); |
90 |
222 |
ASSERT_FALSE((logic2 <= logic1)); |
91 |
222 |
ASSERT_TRUE(logic2 >= logic1); |
92 |
222 |
ASSERT_TRUE(logic2.isComparableTo(logic1)); |
93 |
|
} |
94 |
|
|
95 |
216 |
void gt(const LogicInfo& logic1, const LogicInfo& logic2) const |
96 |
|
{ |
97 |
216 |
std::cout << "asserting that " << logic1 << " > " << logic2 << std::endl; |
98 |
|
|
99 |
216 |
ASSERT_FALSE((logic1 == logic2)); |
100 |
216 |
ASSERT_TRUE(logic1 != logic2); |
101 |
216 |
ASSERT_FALSE((logic1 < logic2)); |
102 |
216 |
ASSERT_TRUE(logic1 > logic2); |
103 |
216 |
ASSERT_FALSE((logic1 <= logic2)); |
104 |
216 |
ASSERT_TRUE(logic1 >= logic2); |
105 |
216 |
ASSERT_TRUE(logic1.isComparableTo(logic2)); |
106 |
|
|
107 |
216 |
ASSERT_FALSE((logic2 == logic1)); |
108 |
216 |
ASSERT_TRUE(logic2 != logic1); |
109 |
216 |
ASSERT_TRUE(logic2 < logic1); |
110 |
216 |
ASSERT_FALSE((logic2 > logic1)); |
111 |
216 |
ASSERT_TRUE(logic2 <= logic1); |
112 |
216 |
ASSERT_FALSE((logic2 >= logic1)); |
113 |
216 |
ASSERT_TRUE(logic2.isComparableTo(logic1)); |
114 |
|
} |
115 |
|
}; |
116 |
|
|
117 |
12 |
TEST_F(TestTheoryWhiteLogicInfo, smtlib_logics) |
118 |
|
{ |
119 |
4 |
LogicInfo info("QF_SAT"); |
120 |
2 |
ASSERT_TRUE(info.isLocked()); |
121 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
122 |
2 |
ASSERT_TRUE(info.isPure(THEORY_BOOL)); |
123 |
2 |
ASSERT_FALSE(info.isQuantified()); |
124 |
2 |
ASSERT_FALSE(info.hasEverything()); |
125 |
2 |
ASSERT_TRUE(info.hasNothing()); |
126 |
|
|
127 |
2 |
info = LogicInfo("AUFLIA"); |
128 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
129 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
130 |
2 |
ASSERT_TRUE(info.isQuantified()); |
131 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
132 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
133 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
134 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
135 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
136 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
137 |
2 |
ASSERT_TRUE(info.isLinear()); |
138 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
139 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
140 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
141 |
2 |
ASSERT_FALSE(info.hasEverything()); |
142 |
2 |
ASSERT_FALSE(info.hasNothing()); |
143 |
|
|
144 |
2 |
info = LogicInfo("AUFLIRA"); |
145 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
146 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
147 |
2 |
ASSERT_TRUE(info.isQuantified()); |
148 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
149 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
150 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
151 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
152 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
153 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
154 |
2 |
ASSERT_TRUE(info.isLinear()); |
155 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
156 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
157 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
158 |
2 |
ASSERT_FALSE(info.hasEverything()); |
159 |
2 |
ASSERT_FALSE(info.hasNothing()); |
160 |
|
|
161 |
2 |
info = LogicInfo("AUFNIRA"); |
162 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
163 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
164 |
2 |
ASSERT_TRUE(info.isQuantified()); |
165 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
166 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
167 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
168 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
169 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
170 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
171 |
2 |
ASSERT_FALSE(info.isLinear()); |
172 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
173 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
174 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
175 |
2 |
ASSERT_FALSE(info.hasEverything()); |
176 |
2 |
ASSERT_FALSE(info.hasNothing()); |
177 |
|
|
178 |
2 |
info = LogicInfo("LRA"); |
179 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
180 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
181 |
2 |
ASSERT_TRUE(info.isQuantified()); |
182 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
183 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
184 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
185 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
186 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
187 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
188 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
189 |
2 |
ASSERT_TRUE(info.isLinear()); |
190 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
191 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
192 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
193 |
2 |
ASSERT_FALSE(info.hasEverything()); |
194 |
2 |
ASSERT_FALSE(info.hasNothing()); |
195 |
|
|
196 |
2 |
info = LogicInfo("QF_ABV"); |
197 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
198 |
2 |
ASSERT_FALSE(info.isQuantified()); |
199 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
200 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
201 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
202 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
203 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); |
204 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
205 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
206 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
207 |
2 |
ASSERT_FALSE(info.hasEverything()); |
208 |
2 |
ASSERT_FALSE(info.hasNothing()); |
209 |
|
|
210 |
2 |
info = LogicInfo("QF_AUFBV"); |
211 |
2 |
ASSERT_FALSE(info.isQuantified()); |
212 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
213 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
214 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
215 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
216 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); |
217 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
218 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
219 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
220 |
2 |
ASSERT_FALSE(info.hasEverything()); |
221 |
2 |
ASSERT_FALSE(info.hasNothing()); |
222 |
|
|
223 |
2 |
info = LogicInfo("QF_AUFLIA"); |
224 |
2 |
ASSERT_FALSE(info.isQuantified()); |
225 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
226 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
227 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
228 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
229 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); |
230 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
231 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
232 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
233 |
2 |
ASSERT_TRUE(info.isLinear()); |
234 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
235 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
236 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
237 |
2 |
ASSERT_FALSE(info.hasEverything()); |
238 |
2 |
ASSERT_FALSE(info.hasNothing()); |
239 |
|
|
240 |
2 |
info = LogicInfo("QF_AX"); |
241 |
2 |
ASSERT_FALSE(info.isQuantified()); |
242 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
243 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
244 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
245 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
246 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARRAYS)); |
247 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
248 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
249 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
250 |
2 |
ASSERT_FALSE(info.hasEverything()); |
251 |
2 |
ASSERT_FALSE(info.hasNothing()); |
252 |
|
|
253 |
2 |
info = LogicInfo("QF_BV"); |
254 |
2 |
ASSERT_FALSE(info.isQuantified()); |
255 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
256 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
257 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
258 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
259 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); |
260 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
261 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
262 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
263 |
2 |
ASSERT_FALSE(info.hasEverything()); |
264 |
2 |
ASSERT_FALSE(info.hasNothing()); |
265 |
|
|
266 |
2 |
info = LogicInfo("QF_IDL"); |
267 |
2 |
ASSERT_FALSE(info.isQuantified()); |
268 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
269 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
270 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
271 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
272 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
273 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
274 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
275 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
276 |
2 |
ASSERT_TRUE(info.isLinear()); |
277 |
2 |
ASSERT_TRUE(info.isDifferenceLogic()); |
278 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
279 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
280 |
2 |
ASSERT_FALSE(info.hasEverything()); |
281 |
2 |
ASSERT_FALSE(info.hasNothing()); |
282 |
|
|
283 |
2 |
info = LogicInfo("QF_LIA"); |
284 |
2 |
ASSERT_FALSE(info.isQuantified()); |
285 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
286 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
287 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
288 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
289 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
290 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
291 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
292 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
293 |
2 |
ASSERT_TRUE(info.isLinear()); |
294 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
295 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
296 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
297 |
2 |
ASSERT_FALSE(info.hasEverything()); |
298 |
2 |
ASSERT_FALSE(info.hasNothing()); |
299 |
|
|
300 |
2 |
info = LogicInfo("QF_LRA"); |
301 |
2 |
ASSERT_FALSE(info.isQuantified()); |
302 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
303 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
304 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
305 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
306 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
307 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
308 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
309 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
310 |
2 |
ASSERT_TRUE(info.isLinear()); |
311 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
312 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
313 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
314 |
2 |
ASSERT_FALSE(info.hasEverything()); |
315 |
2 |
ASSERT_FALSE(info.hasNothing()); |
316 |
|
|
317 |
2 |
info = LogicInfo("QF_NIA"); |
318 |
2 |
ASSERT_FALSE(info.isQuantified()); |
319 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
320 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
321 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
322 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
323 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
324 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
325 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
326 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
327 |
2 |
ASSERT_FALSE(info.isLinear()); |
328 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
329 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
330 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
331 |
2 |
ASSERT_FALSE(info.hasEverything()); |
332 |
2 |
ASSERT_FALSE(info.hasNothing()); |
333 |
|
|
334 |
2 |
info = LogicInfo("QF_NRA"); |
335 |
2 |
ASSERT_FALSE(info.isQuantified()); |
336 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
337 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
338 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
339 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
340 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
341 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
342 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
343 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
344 |
2 |
ASSERT_FALSE(info.isLinear()); |
345 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
346 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
347 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
348 |
2 |
ASSERT_FALSE(info.hasEverything()); |
349 |
2 |
ASSERT_FALSE(info.hasNothing()); |
350 |
|
|
351 |
2 |
info = LogicInfo("QF_RDL"); |
352 |
2 |
ASSERT_FALSE(info.isQuantified()); |
353 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
354 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
355 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
356 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
357 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARITH)); |
358 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
359 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
360 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
361 |
2 |
ASSERT_TRUE(info.isLinear()); |
362 |
2 |
ASSERT_TRUE(info.isDifferenceLogic()); |
363 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
364 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
365 |
2 |
ASSERT_FALSE(info.hasEverything()); |
366 |
2 |
ASSERT_FALSE(info.hasNothing()); |
367 |
|
|
368 |
2 |
info = LogicInfo("QF_UF"); |
369 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
370 |
2 |
ASSERT_FALSE(info.isQuantified()); |
371 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
372 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
373 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
374 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
375 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
376 |
2 |
ASSERT_TRUE(info.isPure(THEORY_UF)); |
377 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
378 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
379 |
2 |
ASSERT_FALSE(info.hasEverything()); |
380 |
2 |
ASSERT_FALSE(info.hasNothing()); |
381 |
|
|
382 |
2 |
info = LogicInfo("QF_UFBV"); |
383 |
2 |
ASSERT_FALSE(info.isQuantified()); |
384 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
385 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
386 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
387 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
388 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
389 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BV)); |
390 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
391 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
392 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
393 |
2 |
ASSERT_FALSE(info.hasEverything()); |
394 |
2 |
ASSERT_FALSE(info.hasNothing()); |
395 |
|
|
396 |
2 |
info = LogicInfo("QF_UFIDL"); |
397 |
2 |
ASSERT_FALSE(info.isQuantified()); |
398 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
399 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
400 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
401 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
402 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
403 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
404 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
405 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
406 |
2 |
ASSERT_TRUE(info.isLinear()); |
407 |
2 |
ASSERT_TRUE(info.isDifferenceLogic()); |
408 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
409 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
410 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
411 |
2 |
ASSERT_FALSE(info.hasEverything()); |
412 |
2 |
ASSERT_FALSE(info.hasNothing()); |
413 |
|
|
414 |
2 |
info = LogicInfo("QF_UFLIA"); |
415 |
2 |
ASSERT_FALSE(info.isQuantified()); |
416 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
417 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
418 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
419 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
420 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
421 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
422 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
423 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
424 |
2 |
ASSERT_TRUE(info.isLinear()); |
425 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
426 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
427 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
428 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
429 |
2 |
ASSERT_FALSE(info.hasEverything()); |
430 |
2 |
ASSERT_FALSE(info.hasNothing()); |
431 |
|
|
432 |
2 |
info = LogicInfo("QF_UFLRA"); |
433 |
2 |
ASSERT_FALSE(info.isQuantified()); |
434 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
435 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
436 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
437 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
438 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
439 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
440 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
441 |
2 |
ASSERT_TRUE(info.isLinear()); |
442 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
443 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
444 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
445 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
446 |
2 |
ASSERT_FALSE(info.hasEverything()); |
447 |
2 |
ASSERT_FALSE(info.hasNothing()); |
448 |
|
|
449 |
2 |
info = LogicInfo("QF_UFNRA"); |
450 |
2 |
ASSERT_FALSE(info.isQuantified()); |
451 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
452 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
453 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
454 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
455 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
456 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
457 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
458 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
459 |
2 |
ASSERT_FALSE(info.isLinear()); |
460 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
461 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
462 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
463 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
464 |
2 |
ASSERT_FALSE(info.hasEverything()); |
465 |
2 |
ASSERT_FALSE(info.hasNothing()); |
466 |
|
|
467 |
2 |
info = LogicInfo("UFLRA"); |
468 |
2 |
ASSERT_TRUE(info.isQuantified()); |
469 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
470 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
471 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
472 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
473 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
474 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
475 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
476 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
477 |
2 |
ASSERT_TRUE(info.isLinear()); |
478 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
479 |
2 |
ASSERT_FALSE(info.areIntegersUsed()); |
480 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
481 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
482 |
2 |
ASSERT_FALSE(info.hasEverything()); |
483 |
2 |
ASSERT_FALSE(info.hasNothing()); |
484 |
|
|
485 |
2 |
info = LogicInfo("UFNIA"); |
486 |
2 |
ASSERT_TRUE(info.isQuantified()); |
487 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
488 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
489 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
490 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
491 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
492 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
493 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
494 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
495 |
2 |
ASSERT_FALSE(info.isLinear()); |
496 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
497 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
498 |
2 |
ASSERT_FALSE(info.areRealsUsed()); |
499 |
2 |
ASSERT_FALSE(info.areTranscendentalsUsed()); |
500 |
2 |
ASSERT_FALSE(info.hasEverything()); |
501 |
2 |
ASSERT_FALSE(info.hasNothing()); |
502 |
|
|
503 |
2 |
info = LogicInfo("QF_ALL"); |
504 |
2 |
ASSERT_TRUE(info.isLocked()); |
505 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
506 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
507 |
2 |
ASSERT_FALSE(info.isQuantified()); |
508 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
509 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
510 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
511 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
512 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); |
513 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
514 |
2 |
ASSERT_FALSE(info.isLinear()); |
515 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
516 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
517 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
518 |
2 |
ASSERT_TRUE(info.areTranscendentalsUsed()); |
519 |
2 |
ASSERT_FALSE(info.hasEverything()); |
520 |
2 |
ASSERT_FALSE(info.hasNothing()); |
521 |
|
|
522 |
2 |
info = LogicInfo("ALL"); |
523 |
2 |
ASSERT_TRUE(info.isLocked()); |
524 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
525 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
526 |
2 |
ASSERT_TRUE(info.isQuantified()); |
527 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
528 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
529 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
530 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
531 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); |
532 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
533 |
2 |
ASSERT_FALSE(info.isLinear()); |
534 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
535 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
536 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
537 |
2 |
ASSERT_TRUE(info.hasEverything()); |
538 |
2 |
ASSERT_FALSE(info.hasNothing()); |
539 |
|
} |
540 |
|
|
541 |
12 |
TEST_F(TestTheoryWhiteLogicInfo, default_logic) |
542 |
|
{ |
543 |
4 |
LogicInfo info; |
544 |
2 |
ASSERT_FALSE(info.isLocked()); |
545 |
|
|
546 |
4 |
ASSERT_THROW(info.getLogicString(), cvc5::IllegalArgumentException); |
547 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_BUILTIN), |
548 |
2 |
cvc5::IllegalArgumentException); |
549 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_BOOL), |
550 |
2 |
cvc5::IllegalArgumentException); |
551 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), cvc5::IllegalArgumentException); |
552 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_ARITH), |
553 |
2 |
cvc5::IllegalArgumentException); |
554 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_ARRAYS), |
555 |
2 |
cvc5::IllegalArgumentException); |
556 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), cvc5::IllegalArgumentException); |
557 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_DATATYPES), |
558 |
2 |
cvc5::IllegalArgumentException); |
559 |
4 |
ASSERT_THROW(info.isTheoryEnabled(THEORY_QUANTIFIERS), |
560 |
2 |
cvc5::IllegalArgumentException); |
561 |
4 |
ASSERT_THROW(info.isPure(THEORY_BUILTIN), cvc5::IllegalArgumentException); |
562 |
4 |
ASSERT_THROW(info.isPure(THEORY_BOOL), cvc5::IllegalArgumentException); |
563 |
4 |
ASSERT_THROW(info.isPure(THEORY_UF), cvc5::IllegalArgumentException); |
564 |
4 |
ASSERT_THROW(info.isPure(THEORY_ARITH), cvc5::IllegalArgumentException); |
565 |
4 |
ASSERT_THROW(info.isPure(THEORY_ARRAYS), cvc5::IllegalArgumentException); |
566 |
4 |
ASSERT_THROW(info.isPure(THEORY_BV), cvc5::IllegalArgumentException); |
567 |
4 |
ASSERT_THROW(info.isPure(THEORY_DATATYPES), cvc5::IllegalArgumentException); |
568 |
4 |
ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), cvc5::IllegalArgumentException); |
569 |
4 |
ASSERT_THROW(info.isQuantified(), cvc5::IllegalArgumentException); |
570 |
4 |
ASSERT_THROW(info.areIntegersUsed(), cvc5::IllegalArgumentException); |
571 |
4 |
ASSERT_THROW(info.areRealsUsed(), cvc5::IllegalArgumentException); |
572 |
4 |
ASSERT_THROW(info.isLinear(), cvc5::IllegalArgumentException); |
573 |
|
|
574 |
2 |
info.lock(); |
575 |
2 |
ASSERT_TRUE(info.isLocked()); |
576 |
2 |
ASSERT_EQ(info.getLogicString(), "ALL"); |
577 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
578 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BUILTIN)); |
579 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
580 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
581 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
582 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
583 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
584 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); |
585 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_QUANTIFIERS)); |
586 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BUILTIN)); |
587 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
588 |
2 |
ASSERT_FALSE(info.isPure(THEORY_UF)); |
589 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARITH)); |
590 |
2 |
ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); |
591 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BV)); |
592 |
2 |
ASSERT_FALSE(info.isPure(THEORY_DATATYPES)); |
593 |
2 |
ASSERT_FALSE(info.isPure(THEORY_QUANTIFIERS)); |
594 |
2 |
ASSERT_TRUE(info.isQuantified()); |
595 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
596 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
597 |
2 |
ASSERT_TRUE(info.areTranscendentalsUsed()); |
598 |
2 |
ASSERT_FALSE(info.isLinear()); |
599 |
|
|
600 |
4 |
ASSERT_THROW(info.arithOnlyLinear(), cvc5::IllegalArgumentException); |
601 |
4 |
ASSERT_THROW(info.disableIntegers(), cvc5::IllegalArgumentException); |
602 |
4 |
ASSERT_THROW(info.disableQuantifiers(), cvc5::IllegalArgumentException); |
603 |
4 |
ASSERT_THROW(info.disableTheory(THEORY_BV), cvc5::IllegalArgumentException); |
604 |
4 |
ASSERT_THROW(info.disableTheory(THEORY_DATATYPES), |
605 |
2 |
cvc5::IllegalArgumentException); |
606 |
4 |
ASSERT_THROW(info.enableIntegers(), cvc5::IllegalArgumentException); |
607 |
4 |
ASSERT_THROW(info.disableReals(), cvc5::IllegalArgumentException); |
608 |
4 |
ASSERT_THROW(info.disableTheory(THEORY_ARITH), |
609 |
2 |
cvc5::IllegalArgumentException); |
610 |
4 |
ASSERT_THROW(info.disableTheory(THEORY_UF), cvc5::IllegalArgumentException); |
611 |
2 |
info = info.getUnlockedCopy(); |
612 |
2 |
ASSERT_FALSE(info.isLocked()); |
613 |
2 |
info.disableTheory(THEORY_STRINGS); |
614 |
2 |
info.disableTheory(THEORY_SETS); |
615 |
2 |
info.disableTheory(THEORY_BAGS); |
616 |
2 |
info.arithOnlyLinear(); |
617 |
2 |
info.disableIntegers(); |
618 |
2 |
info.lock(); |
619 |
2 |
ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); |
620 |
|
|
621 |
2 |
info = info.getUnlockedCopy(); |
622 |
2 |
ASSERT_FALSE(info.isLocked()); |
623 |
2 |
info.disableQuantifiers(); |
624 |
2 |
info.disableTheory(THEORY_BAGS); |
625 |
2 |
info.lock(); |
626 |
2 |
ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); |
627 |
|
|
628 |
2 |
info = info.getUnlockedCopy(); |
629 |
2 |
ASSERT_FALSE(info.isLocked()); |
630 |
2 |
info.disableTheory(THEORY_BV); |
631 |
2 |
info.disableTheory(THEORY_DATATYPES); |
632 |
2 |
info.disableTheory(THEORY_BAGS); |
633 |
2 |
info.enableIntegers(); |
634 |
2 |
info.disableReals(); |
635 |
2 |
info.lock(); |
636 |
2 |
ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); |
637 |
|
|
638 |
2 |
info = info.getUnlockedCopy(); |
639 |
2 |
ASSERT_FALSE(info.isLocked()); |
640 |
2 |
info.disableTheory(THEORY_ARITH); |
641 |
2 |
info.disableTheory(THEORY_UF); |
642 |
2 |
info.disableTheory(THEORY_FP); |
643 |
2 |
info.disableTheory(THEORY_SEP); |
644 |
2 |
info.disableTheory(THEORY_BAGS); |
645 |
2 |
info.lock(); |
646 |
2 |
ASSERT_EQ(info.getLogicString(), "QF_AX"); |
647 |
2 |
ASSERT_TRUE(info.isPure(THEORY_ARRAYS)); |
648 |
2 |
ASSERT_FALSE(info.isQuantified()); |
649 |
|
// check all-excluded logic |
650 |
2 |
info = info.getUnlockedCopy(); |
651 |
2 |
ASSERT_FALSE(info.isLocked()); |
652 |
2 |
info.disableEverything(); |
653 |
2 |
info.lock(); |
654 |
2 |
ASSERT_TRUE(info.isLocked()); |
655 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
656 |
2 |
ASSERT_FALSE(info.isQuantified()); |
657 |
2 |
ASSERT_TRUE(info.isPure(THEORY_BOOL)); |
658 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
659 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
660 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
661 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
662 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
663 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
664 |
4 |
ASSERT_THROW(info.isLinear(), IllegalArgumentException); |
665 |
4 |
ASSERT_THROW(info.areIntegersUsed(), IllegalArgumentException); |
666 |
4 |
ASSERT_THROW(info.isDifferenceLogic(), IllegalArgumentException); |
667 |
4 |
ASSERT_THROW(info.areRealsUsed(), IllegalArgumentException); |
668 |
4 |
ASSERT_THROW(info.areTranscendentalsUsed(), IllegalArgumentException); |
669 |
|
|
670 |
|
// check copy is unchanged |
671 |
2 |
info = info.getUnlockedCopy(); |
672 |
2 |
ASSERT_FALSE(info.isLocked()); |
673 |
2 |
info.lock(); |
674 |
2 |
ASSERT_TRUE(info.isLocked()); |
675 |
2 |
ASSERT_FALSE(info.isSharingEnabled()); |
676 |
2 |
ASSERT_FALSE(info.isQuantified()); |
677 |
2 |
ASSERT_TRUE(info.isPure(THEORY_BOOL)); |
678 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); |
679 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); |
680 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); |
681 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); |
682 |
2 |
ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); |
683 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
684 |
4 |
ASSERT_THROW(info.isLinear(), IllegalArgumentException); |
685 |
4 |
ASSERT_THROW(info.areIntegersUsed(), IllegalArgumentException); |
686 |
4 |
ASSERT_THROW(info.isDifferenceLogic(), IllegalArgumentException); |
687 |
4 |
ASSERT_THROW(info.areRealsUsed(), IllegalArgumentException); |
688 |
4 |
ASSERT_THROW(info.areTranscendentalsUsed(), IllegalArgumentException); |
689 |
|
|
690 |
|
// check all-included logic |
691 |
2 |
info = info.getUnlockedCopy(); |
692 |
2 |
ASSERT_FALSE(info.isLocked()); |
693 |
2 |
info.enableEverything(); |
694 |
2 |
info.lock(); |
695 |
2 |
ASSERT_TRUE(info.isLocked()); |
696 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
697 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
698 |
2 |
ASSERT_TRUE(info.isQuantified()); |
699 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
700 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
701 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
702 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
703 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); |
704 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
705 |
2 |
ASSERT_FALSE(info.isLinear()); |
706 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
707 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
708 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
709 |
2 |
ASSERT_TRUE(info.areTranscendentalsUsed()); |
710 |
|
|
711 |
|
// check copy is unchanged |
712 |
2 |
info = info.getUnlockedCopy(); |
713 |
2 |
ASSERT_FALSE(info.isLocked()); |
714 |
2 |
info.lock(); |
715 |
2 |
ASSERT_TRUE(info.isLocked()); |
716 |
2 |
ASSERT_FALSE(info.isPure(THEORY_BOOL)); |
717 |
2 |
ASSERT_TRUE(info.isSharingEnabled()); |
718 |
2 |
ASSERT_TRUE(info.isQuantified()); |
719 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); |
720 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); |
721 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); |
722 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); |
723 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); |
724 |
2 |
ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); |
725 |
2 |
ASSERT_FALSE(info.isLinear()); |
726 |
2 |
ASSERT_TRUE(info.areIntegersUsed()); |
727 |
2 |
ASSERT_FALSE(info.isDifferenceLogic()); |
728 |
2 |
ASSERT_TRUE(info.areRealsUsed()); |
729 |
2 |
ASSERT_TRUE(info.areTranscendentalsUsed()); |
730 |
|
} |
731 |
|
|
732 |
12 |
TEST_F(TestTheoryWhiteLogicInfo, comparison) |
733 |
|
{ |
734 |
4 |
LogicInfo ufHo = LogicInfo("QF_UF").getUnlockedCopy(); |
735 |
2 |
ufHo.enableHigherOrder(); |
736 |
2 |
ufHo.lock(); |
737 |
|
|
738 |
2 |
eq("QF_UF", "QF_UF"); |
739 |
2 |
nc("QF_UF", "QF_LRA"); |
740 |
2 |
nc("QF_UF", "QF_LIA"); |
741 |
2 |
lt("QF_UF", "QF_UFLRA"); |
742 |
2 |
lt("QF_UF", "QF_UFLIA"); |
743 |
2 |
lt("QF_UF", "QF_AUFLIA"); |
744 |
2 |
lt("QF_UF", "QF_AUFLIRA"); |
745 |
2 |
nc("QF_UF", "QF_BV"); |
746 |
2 |
nc("QF_UF", "QF_ABV"); |
747 |
2 |
lt("QF_UF", "QF_AUFBV"); |
748 |
2 |
nc("QF_UF", "QF_IDL"); |
749 |
2 |
nc("QF_UF", "QF_RDL"); |
750 |
2 |
lt("QF_UF", "QF_UFIDL"); |
751 |
2 |
nc("QF_UF", "QF_NIA"); |
752 |
2 |
nc("QF_UF", "QF_NRA"); |
753 |
2 |
lt("QF_UF", "QF_AUFNIRA"); |
754 |
2 |
nc("QF_UF", "LRA"); |
755 |
2 |
nc("QF_UF", "NRA"); |
756 |
2 |
nc("QF_UF", "NIA"); |
757 |
2 |
lt("QF_UF", "UFLRA"); |
758 |
2 |
lt("QF_UF", "UFNIA"); |
759 |
2 |
lt("QF_UF", "AUFLIA"); |
760 |
2 |
lt("QF_UF", "AUFLIRA"); |
761 |
2 |
lt("QF_UF", "AUFNIRA"); |
762 |
2 |
lt("QF_UF", "QF_UFC"); |
763 |
2 |
lt("QF_UF", ufHo); |
764 |
2 |
nc("QF_UFC", ufHo); |
765 |
|
|
766 |
2 |
nc("QF_LRA", "QF_UF"); |
767 |
2 |
eq("QF_LRA", "QF_LRA"); |
768 |
2 |
nc("QF_LRA", "QF_LIA"); |
769 |
2 |
lt("QF_LRA", "QF_UFLRA"); |
770 |
2 |
nc("QF_LRA", "QF_UFLIA"); |
771 |
2 |
nc("QF_LRA", "QF_AUFLIA"); |
772 |
2 |
lt("QF_LRA", "QF_AUFLIRA"); |
773 |
2 |
nc("QF_LRA", "QF_BV"); |
774 |
2 |
nc("QF_LRA", "QF_ABV"); |
775 |
2 |
nc("QF_LRA", "QF_AUFBV"); |
776 |
2 |
nc("QF_LRA", "QF_IDL"); |
777 |
2 |
gt("QF_LRA", "QF_RDL"); |
778 |
2 |
nc("QF_LRA", "QF_UFIDL"); |
779 |
2 |
nc("QF_LRA", "QF_NIA"); |
780 |
2 |
lt("QF_LRA", "QF_NRA"); |
781 |
2 |
lt("QF_LRA", "QF_AUFNIRA"); |
782 |
2 |
lt("QF_LRA", "LRA"); |
783 |
2 |
lt("QF_LRA", "NRA"); |
784 |
2 |
nc("QF_LRA", "NIA"); |
785 |
2 |
lt("QF_LRA", "UFLRA"); |
786 |
2 |
nc("QF_LRA", "UFNIA"); |
787 |
2 |
nc("QF_LRA", "AUFLIA"); |
788 |
2 |
lt("QF_LRA", "AUFLIRA"); |
789 |
2 |
lt("QF_LRA", "AUFNIRA"); |
790 |
2 |
lt("QF_LRA", "QF_UFCLRA"); |
791 |
|
|
792 |
2 |
nc("QF_LIA", "QF_UF"); |
793 |
2 |
nc("QF_LIA", "QF_LRA"); |
794 |
2 |
eq("QF_LIA", "QF_LIA"); |
795 |
2 |
nc("QF_LIA", "QF_UFLRA"); |
796 |
2 |
lt("QF_LIA", "QF_UFLIA"); |
797 |
2 |
lt("QF_LIA", "QF_AUFLIA"); |
798 |
2 |
lt("QF_LIA", "QF_AUFLIRA"); |
799 |
2 |
nc("QF_LIA", "QF_BV"); |
800 |
2 |
nc("QF_LIA", "QF_ABV"); |
801 |
2 |
nc("QF_LIA", "QF_AUFBV"); |
802 |
2 |
gt("QF_LIA", "QF_IDL"); |
803 |
2 |
nc("QF_LIA", "QF_RDL"); |
804 |
2 |
nc("QF_LIA", "QF_UFIDL"); |
805 |
2 |
lt("QF_LIA", "QF_NIA"); |
806 |
2 |
nc("QF_LIA", "QF_NRA"); |
807 |
2 |
lt("QF_LIA", "QF_AUFNIRA"); |
808 |
2 |
nc("QF_LIA", "LRA"); |
809 |
2 |
nc("QF_LIA", "NRA"); |
810 |
2 |
lt("QF_LIA", "NIA"); |
811 |
2 |
nc("QF_LIA", "UFLRA"); |
812 |
2 |
lt("QF_LIA", "UFNIA"); |
813 |
2 |
lt("QF_LIA", "AUFLIA"); |
814 |
2 |
lt("QF_LIA", "AUFLIRA"); |
815 |
2 |
lt("QF_LIA", "AUFNIRA"); |
816 |
|
|
817 |
2 |
gt("QF_UFLRA", "QF_UF"); |
818 |
2 |
gt("QF_UFLRA", "QF_LRA"); |
819 |
2 |
nc("QF_UFLRA", "QF_LIA"); |
820 |
2 |
eq("QF_UFLRA", "QF_UFLRA"); |
821 |
2 |
nc("QF_UFLRA", "QF_UFLIA"); |
822 |
2 |
nc("QF_UFLRA", "QF_AUFLIA"); |
823 |
2 |
lt("QF_UFLRA", "QF_AUFLIRA"); |
824 |
2 |
nc("QF_UFLRA", "QF_BV"); |
825 |
2 |
nc("QF_UFLRA", "QF_ABV"); |
826 |
2 |
nc("QF_UFLRA", "QF_AUFBV"); |
827 |
2 |
nc("QF_UFLRA", "QF_IDL"); |
828 |
2 |
gt("QF_UFLRA", "QF_RDL"); |
829 |
2 |
nc("QF_UFLRA", "QF_UFIDL"); |
830 |
2 |
nc("QF_UFLRA", "QF_NIA"); |
831 |
2 |
nc("QF_UFLRA", "QF_NRA"); |
832 |
2 |
lt("QF_UFLRA", "QF_AUFNIRA"); |
833 |
2 |
nc("QF_UFLRA", "LRA"); |
834 |
2 |
nc("QF_UFLRA", "NRA"); |
835 |
2 |
nc("QF_UFLRA", "NIA"); |
836 |
2 |
lt("QF_UFLRA", "UFLRA"); |
837 |
2 |
nc("QF_UFLRA", "UFNIA"); |
838 |
2 |
nc("QF_UFLRA", "AUFLIA"); |
839 |
2 |
lt("QF_UFLRA", "AUFLIRA"); |
840 |
2 |
lt("QF_UFLRA", "AUFNIRA"); |
841 |
|
|
842 |
2 |
gt("QF_UFLIA", "QF_UF"); |
843 |
2 |
nc("QF_UFLIA", "QF_LRA"); |
844 |
2 |
gt("QF_UFLIA", "QF_LIA"); |
845 |
2 |
nc("QF_UFLIA", "QF_UFLRA"); |
846 |
2 |
eq("QF_UFLIA", "QF_UFLIA"); |
847 |
2 |
lt("QF_UFLIA", "QF_AUFLIA"); |
848 |
2 |
lt("QF_UFLIA", "QF_AUFLIRA"); |
849 |
2 |
nc("QF_UFLIA", "QF_BV"); |
850 |
2 |
nc("QF_UFLIA", "QF_ABV"); |
851 |
2 |
nc("QF_UFLIA", "QF_AUFBV"); |
852 |
2 |
gt("QF_UFLIA", "QF_IDL"); |
853 |
2 |
nc("QF_UFLIA", "QF_RDL"); |
854 |
2 |
gt("QF_UFLIA", "QF_UFIDL"); |
855 |
2 |
nc("QF_UFLIA", "QF_NIA"); |
856 |
2 |
nc("QF_UFLIA", "QF_NRA"); |
857 |
2 |
lt("QF_UFLIA", "QF_AUFNIRA"); |
858 |
2 |
nc("QF_UFLIA", "LRA"); |
859 |
2 |
nc("QF_UFLIA", "NRA"); |
860 |
2 |
nc("QF_UFLIA", "NIA"); |
861 |
2 |
nc("QF_UFLIA", "UFLRA"); |
862 |
2 |
lt("QF_UFLIA", "UFNIA"); |
863 |
2 |
lt("QF_UFLIA", "AUFLIA"); |
864 |
2 |
lt("QF_UFLIA", "AUFLIRA"); |
865 |
2 |
lt("QF_UFLIA", "AUFNIRA"); |
866 |
|
|
867 |
2 |
gt("QF_AUFLIA", "QF_UF"); |
868 |
2 |
nc("QF_AUFLIA", "QF_LRA"); |
869 |
2 |
gt("QF_AUFLIA", "QF_LIA"); |
870 |
2 |
nc("QF_AUFLIA", "QF_UFLRA"); |
871 |
2 |
gt("QF_AUFLIA", "QF_UFLIA"); |
872 |
2 |
eq("QF_AUFLIA", "QF_AUFLIA"); |
873 |
2 |
lt("QF_AUFLIA", "QF_AUFLIRA"); |
874 |
2 |
nc("QF_AUFLIA", "QF_BV"); |
875 |
2 |
nc("QF_AUFLIA", "QF_ABV"); |
876 |
2 |
nc("QF_AUFLIA", "QF_AUFBV"); |
877 |
2 |
gt("QF_AUFLIA", "QF_IDL"); |
878 |
2 |
nc("QF_AUFLIA", "QF_RDL"); |
879 |
2 |
gt("QF_AUFLIA", "QF_UFIDL"); |
880 |
2 |
nc("QF_AUFLIA", "QF_NIA"); |
881 |
2 |
nc("QF_AUFLIA", "QF_NRA"); |
882 |
2 |
lt("QF_AUFLIA", "QF_AUFNIRA"); |
883 |
2 |
nc("QF_AUFLIA", "LRA"); |
884 |
2 |
nc("QF_AUFLIA", "NRA"); |
885 |
2 |
nc("QF_AUFLIA", "NIA"); |
886 |
2 |
nc("QF_AUFLIA", "UFLRA"); |
887 |
2 |
nc("QF_AUFLIA", "UFNIA"); |
888 |
2 |
lt("QF_AUFLIA", "AUFLIA"); |
889 |
2 |
lt("QF_AUFLIA", "AUFLIRA"); |
890 |
2 |
lt("QF_AUFLIA", "AUFNIRA"); |
891 |
|
|
892 |
2 |
gt("QF_AUFLIRA", "QF_UF"); |
893 |
2 |
gt("QF_AUFLIRA", "QF_LRA"); |
894 |
2 |
gt("QF_AUFLIRA", "QF_LIA"); |
895 |
2 |
gt("QF_AUFLIRA", "QF_UFLRA"); |
896 |
2 |
gt("QF_AUFLIRA", "QF_UFLIA"); |
897 |
2 |
gt("QF_AUFLIRA", "QF_AUFLIA"); |
898 |
2 |
eq("QF_AUFLIRA", "QF_AUFLIRA"); |
899 |
2 |
nc("QF_AUFLIRA", "QF_BV"); |
900 |
2 |
nc("QF_AUFLIRA", "QF_ABV"); |
901 |
2 |
nc("QF_AUFLIRA", "QF_AUFBV"); |
902 |
2 |
gt("QF_AUFLIRA", "QF_IDL"); |
903 |
2 |
gt("QF_AUFLIRA", "QF_RDL"); |
904 |
2 |
gt("QF_AUFLIRA", "QF_UFIDL"); |
905 |
2 |
nc("QF_AUFLIRA", "QF_NIA"); |
906 |
2 |
nc("QF_AUFLIRA", "QF_NRA"); |
907 |
2 |
lt("QF_AUFLIRA", "QF_AUFNIRA"); |
908 |
2 |
nc("QF_AUFLIRA", "LRA"); |
909 |
2 |
nc("QF_AUFLIRA", "NRA"); |
910 |
2 |
nc("QF_AUFLIRA", "NIA"); |
911 |
2 |
nc("QF_AUFLIRA", "UFLRA"); |
912 |
2 |
nc("QF_AUFLIRA", "UFNIA"); |
913 |
2 |
nc("QF_AUFLIRA", "AUFLIA"); |
914 |
2 |
lt("QF_AUFLIRA", "AUFLIRA"); |
915 |
2 |
lt("QF_AUFLIRA", "AUFNIRA"); |
916 |
|
|
917 |
2 |
nc("QF_BV", "QF_UF"); |
918 |
2 |
nc("QF_BV", "QF_LRA"); |
919 |
2 |
nc("QF_BV", "QF_LIA"); |
920 |
2 |
nc("QF_BV", "QF_UFLRA"); |
921 |
2 |
nc("QF_BV", "QF_UFLIA"); |
922 |
2 |
nc("QF_BV", "QF_AUFLIA"); |
923 |
2 |
nc("QF_BV", "QF_AUFLIRA"); |
924 |
2 |
eq("QF_BV", "QF_BV"); |
925 |
2 |
lt("QF_BV", "QF_ABV"); |
926 |
2 |
lt("QF_BV", "QF_AUFBV"); |
927 |
2 |
nc("QF_BV", "QF_IDL"); |
928 |
2 |
nc("QF_BV", "QF_RDL"); |
929 |
2 |
nc("QF_BV", "QF_UFIDL"); |
930 |
2 |
nc("QF_BV", "QF_NIA"); |
931 |
2 |
nc("QF_BV", "QF_NRA"); |
932 |
2 |
nc("QF_BV", "QF_AUFNIRA"); |
933 |
2 |
nc("QF_BV", "LRA"); |
934 |
2 |
nc("QF_BV", "NRA"); |
935 |
2 |
nc("QF_BV", "NIA"); |
936 |
2 |
nc("QF_BV", "UFLRA"); |
937 |
2 |
nc("QF_BV", "UFNIA"); |
938 |
2 |
nc("QF_BV", "AUFLIA"); |
939 |
2 |
nc("QF_BV", "AUFLIRA"); |
940 |
2 |
nc("QF_BV", "AUFNIRA"); |
941 |
|
|
942 |
2 |
nc("QF_ABV", "QF_UF"); |
943 |
2 |
nc("QF_ABV", "QF_LRA"); |
944 |
2 |
nc("QF_ABV", "QF_LIA"); |
945 |
2 |
nc("QF_ABV", "QF_UFLRA"); |
946 |
2 |
nc("QF_ABV", "QF_UFLIA"); |
947 |
2 |
nc("QF_ABV", "QF_AUFLIA"); |
948 |
2 |
nc("QF_ABV", "QF_AUFLIRA"); |
949 |
2 |
gt("QF_ABV", "QF_BV"); |
950 |
2 |
eq("QF_ABV", "QF_ABV"); |
951 |
2 |
lt("QF_ABV", "QF_AUFBV"); |
952 |
2 |
nc("QF_ABV", "QF_IDL"); |
953 |
2 |
nc("QF_ABV", "QF_RDL"); |
954 |
2 |
nc("QF_ABV", "QF_UFIDL"); |
955 |
2 |
nc("QF_ABV", "QF_NIA"); |
956 |
2 |
nc("QF_ABV", "QF_NRA"); |
957 |
2 |
nc("QF_ABV", "QF_AUFNIRA"); |
958 |
2 |
nc("QF_ABV", "LRA"); |
959 |
2 |
nc("QF_ABV", "NRA"); |
960 |
2 |
nc("QF_ABV", "NIA"); |
961 |
2 |
nc("QF_ABV", "UFLRA"); |
962 |
2 |
nc("QF_ABV", "UFNIA"); |
963 |
2 |
nc("QF_ABV", "AUFLIA"); |
964 |
2 |
nc("QF_ABV", "AUFLIRA"); |
965 |
2 |
nc("QF_ABV", "AUFNIRA"); |
966 |
|
|
967 |
2 |
gt("QF_AUFBV", "QF_UF"); |
968 |
2 |
nc("QF_AUFBV", "QF_LRA"); |
969 |
2 |
nc("QF_AUFBV", "QF_LIA"); |
970 |
2 |
nc("QF_AUFBV", "QF_UFLRA"); |
971 |
2 |
nc("QF_AUFBV", "QF_UFLIA"); |
972 |
2 |
nc("QF_AUFBV", "QF_AUFLIA"); |
973 |
2 |
nc("QF_AUFBV", "QF_AUFLIRA"); |
974 |
2 |
gt("QF_AUFBV", "QF_BV"); |
975 |
2 |
gt("QF_AUFBV", "QF_ABV"); |
976 |
2 |
eq("QF_AUFBV", "QF_AUFBV"); |
977 |
2 |
nc("QF_AUFBV", "QF_IDL"); |
978 |
2 |
nc("QF_AUFBV", "QF_RDL"); |
979 |
2 |
nc("QF_AUFBV", "QF_UFIDL"); |
980 |
2 |
nc("QF_AUFBV", "QF_NIA"); |
981 |
2 |
nc("QF_AUFBV", "QF_NRA"); |
982 |
2 |
nc("QF_AUFBV", "QF_AUFNIRA"); |
983 |
2 |
nc("QF_AUFBV", "LRA"); |
984 |
2 |
nc("QF_AUFBV", "NRA"); |
985 |
2 |
nc("QF_AUFBV", "NIA"); |
986 |
2 |
nc("QF_AUFBV", "UFLRA"); |
987 |
2 |
nc("QF_AUFBV", "UFNIA"); |
988 |
2 |
nc("QF_AUFBV", "AUFLIA"); |
989 |
2 |
nc("QF_AUFBV", "AUFLIRA"); |
990 |
2 |
nc("QF_AUFBV", "AUFNIRA"); |
991 |
|
|
992 |
2 |
nc("QF_IDL", "QF_UF"); |
993 |
2 |
nc("QF_IDL", "QF_LRA"); |
994 |
2 |
lt("QF_IDL", "QF_LIA"); |
995 |
2 |
nc("QF_IDL", "QF_UFLRA"); |
996 |
2 |
lt("QF_IDL", "QF_UFLIA"); |
997 |
2 |
lt("QF_IDL", "QF_AUFLIA"); |
998 |
2 |
lt("QF_IDL", "QF_AUFLIRA"); |
999 |
2 |
nc("QF_IDL", "QF_BV"); |
1000 |
2 |
nc("QF_IDL", "QF_ABV"); |
1001 |
2 |
nc("QF_IDL", "QF_AUFBV"); |
1002 |
2 |
eq("QF_IDL", "QF_IDL"); |
1003 |
2 |
nc("QF_IDL", "QF_RDL"); |
1004 |
2 |
lt("QF_IDL", "QF_UFIDL"); |
1005 |
2 |
lt("QF_IDL", "QF_NIA"); |
1006 |
2 |
nc("QF_IDL", "QF_NRA"); |
1007 |
2 |
nc("QF_IDL", "QF_NRAT"); |
1008 |
2 |
lt("QF_IDL", "QF_AUFNIRA"); |
1009 |
2 |
nc("QF_IDL", "LRA"); |
1010 |
2 |
nc("QF_IDL", "NRA"); |
1011 |
2 |
lt("QF_IDL", "NIA"); |
1012 |
2 |
nc("QF_IDL", "UFLRA"); |
1013 |
2 |
lt("QF_IDL", "UFNIA"); |
1014 |
2 |
lt("QF_IDL", "AUFLIA"); |
1015 |
2 |
lt("QF_IDL", "AUFLIRA"); |
1016 |
2 |
lt("QF_IDL", "AUFNIRA"); |
1017 |
|
|
1018 |
2 |
nc("QF_RDL", "QF_UF"); |
1019 |
2 |
lt("QF_RDL", "QF_LRA"); |
1020 |
2 |
nc("QF_RDL", "QF_LIA"); |
1021 |
2 |
lt("QF_RDL", "QF_UFLRA"); |
1022 |
2 |
nc("QF_RDL", "QF_UFLIA"); |
1023 |
2 |
nc("QF_RDL", "QF_AUFLIA"); |
1024 |
2 |
lt("QF_RDL", "QF_AUFLIRA"); |
1025 |
2 |
nc("QF_RDL", "QF_BV"); |
1026 |
2 |
nc("QF_RDL", "QF_ABV"); |
1027 |
2 |
nc("QF_RDL", "QF_AUFBV"); |
1028 |
2 |
nc("QF_RDL", "QF_IDL"); |
1029 |
2 |
eq("QF_RDL", "QF_RDL"); |
1030 |
2 |
nc("QF_RDL", "QF_UFIDL"); |
1031 |
2 |
nc("QF_RDL", "QF_NIA"); |
1032 |
2 |
lt("QF_RDL", "QF_NRA"); |
1033 |
2 |
lt("QF_RDL", "QF_AUFNIRA"); |
1034 |
2 |
lt("QF_RDL", "LRA"); |
1035 |
2 |
lt("QF_RDL", "NRA"); |
1036 |
2 |
nc("QF_RDL", "NIA"); |
1037 |
2 |
lt("QF_RDL", "UFLRA"); |
1038 |
2 |
nc("QF_RDL", "UFNIA"); |
1039 |
2 |
nc("QF_RDL", "AUFLIA"); |
1040 |
2 |
lt("QF_RDL", "AUFLIRA"); |
1041 |
2 |
lt("QF_RDL", "AUFNIRA"); |
1042 |
|
|
1043 |
2 |
gt("QF_UFIDL", "QF_UF"); |
1044 |
2 |
nc("QF_UFIDL", "QF_LRA"); |
1045 |
2 |
nc("QF_UFIDL", "QF_LIA"); |
1046 |
2 |
nc("QF_UFIDL", "QF_UFLRA"); |
1047 |
2 |
lt("QF_UFIDL", "QF_UFLIA"); |
1048 |
2 |
lt("QF_UFIDL", "QF_AUFLIA"); |
1049 |
2 |
lt("QF_UFIDL", "QF_AUFLIRA"); |
1050 |
2 |
nc("QF_UFIDL", "QF_BV"); |
1051 |
2 |
nc("QF_UFIDL", "QF_ABV"); |
1052 |
2 |
nc("QF_UFIDL", "QF_AUFBV"); |
1053 |
2 |
gt("QF_UFIDL", "QF_IDL"); |
1054 |
2 |
nc("QF_UFIDL", "QF_RDL"); |
1055 |
2 |
eq("QF_UFIDL", "QF_UFIDL"); |
1056 |
2 |
nc("QF_UFIDL", "QF_NIA"); |
1057 |
2 |
nc("QF_UFIDL", "QF_NRA"); |
1058 |
2 |
lt("QF_UFIDL", "QF_AUFNIRA"); |
1059 |
2 |
nc("QF_UFIDL", "LRA"); |
1060 |
2 |
nc("QF_UFIDL", "NRA"); |
1061 |
2 |
nc("QF_UFIDL", "NIA"); |
1062 |
2 |
nc("QF_UFIDL", "UFLRA"); |
1063 |
2 |
lt("QF_UFIDL", "UFNIA"); |
1064 |
2 |
lt("QF_UFIDL", "AUFLIA"); |
1065 |
2 |
lt("QF_UFIDL", "AUFLIRA"); |
1066 |
2 |
lt("QF_UFIDL", "AUFNIRA"); |
1067 |
|
|
1068 |
2 |
nc("QF_NIA", "QF_UF"); |
1069 |
2 |
nc("QF_NIA", "QF_LRA"); |
1070 |
2 |
gt("QF_NIA", "QF_LIA"); |
1071 |
2 |
nc("QF_NIA", "QF_UFLRA"); |
1072 |
2 |
nc("QF_NIA", "QF_UFLIA"); |
1073 |
2 |
nc("QF_NIA", "QF_AUFLIA"); |
1074 |
2 |
nc("QF_NIA", "QF_AUFLIRA"); |
1075 |
2 |
nc("QF_NIA", "QF_BV"); |
1076 |
2 |
nc("QF_NIA", "QF_ABV"); |
1077 |
2 |
nc("QF_NIA", "QF_AUFBV"); |
1078 |
2 |
gt("QF_NIA", "QF_IDL"); |
1079 |
2 |
nc("QF_NIA", "QF_RDL"); |
1080 |
2 |
nc("QF_NIA", "QF_UFIDL"); |
1081 |
2 |
eq("QF_NIA", "QF_NIA"); |
1082 |
2 |
nc("QF_NIA", "QF_NRA"); |
1083 |
2 |
lt("QF_NIA", "QF_AUFNIRA"); |
1084 |
2 |
nc("QF_NIA", "LRA"); |
1085 |
2 |
nc("QF_NIA", "NRA"); |
1086 |
2 |
lt("QF_NIA", "NIA"); |
1087 |
2 |
nc("QF_NIA", "UFLRA"); |
1088 |
2 |
lt("QF_NIA", "UFNIA"); |
1089 |
2 |
nc("QF_NIA", "AUFLIA"); |
1090 |
2 |
nc("QF_NIA", "AUFLIRA"); |
1091 |
2 |
lt("QF_NIA", "AUFNIRA"); |
1092 |
|
|
1093 |
2 |
nc("QF_NRA", "QF_UF"); |
1094 |
2 |
gt("QF_NRA", "QF_LRA"); |
1095 |
2 |
nc("QF_NRA", "QF_LIA"); |
1096 |
2 |
nc("QF_NRA", "QF_UFLRA"); |
1097 |
2 |
nc("QF_NRA", "QF_UFLIA"); |
1098 |
2 |
nc("QF_NRA", "QF_AUFLIA"); |
1099 |
2 |
nc("QF_NRA", "QF_AUFLIRA"); |
1100 |
2 |
nc("QF_NRA", "QF_BV"); |
1101 |
2 |
nc("QF_NRA", "QF_ABV"); |
1102 |
2 |
nc("QF_NRA", "QF_AUFBV"); |
1103 |
2 |
nc("QF_NRA", "QF_IDL"); |
1104 |
2 |
gt("QF_NRA", "QF_RDL"); |
1105 |
2 |
nc("QF_NRA", "QF_UFIDL"); |
1106 |
2 |
nc("QF_NRA", "QF_NIA"); |
1107 |
2 |
eq("QF_NRA", "QF_NRA"); |
1108 |
2 |
lt("QF_NRA", "QF_AUFNIRA"); |
1109 |
2 |
nc("QF_NRA", "LRA"); |
1110 |
2 |
lt("QF_NRA", "NRA"); |
1111 |
2 |
nc("QF_NRA", "NIA"); |
1112 |
2 |
nc("QF_NRA", "UFLRA"); |
1113 |
2 |
nc("QF_NRA", "UFNIA"); |
1114 |
2 |
nc("QF_NRA", "AUFLIA"); |
1115 |
2 |
nc("QF_NRA", "AUFLIRA"); |
1116 |
2 |
lt("QF_NRA", "AUFNIRA"); |
1117 |
2 |
lt("QF_NRA", "QF_NRAT"); |
1118 |
|
|
1119 |
2 |
gt("QF_AUFNIRA", "QF_UF"); |
1120 |
2 |
gt("QF_AUFNIRA", "QF_LRA"); |
1121 |
2 |
gt("QF_AUFNIRA", "QF_LIA"); |
1122 |
2 |
gt("QF_AUFNIRA", "QF_UFLRA"); |
1123 |
2 |
gt("QF_AUFNIRA", "QF_UFLIA"); |
1124 |
2 |
gt("QF_AUFNIRA", "QF_AUFLIA"); |
1125 |
2 |
gt("QF_AUFNIRA", "QF_AUFLIRA"); |
1126 |
2 |
nc("QF_AUFNIRA", "QF_BV"); |
1127 |
2 |
nc("QF_AUFNIRA", "QF_ABV"); |
1128 |
2 |
nc("QF_AUFNIRA", "QF_AUFBV"); |
1129 |
2 |
gt("QF_AUFNIRA", "QF_IDL"); |
1130 |
2 |
gt("QF_AUFNIRA", "QF_RDL"); |
1131 |
2 |
gt("QF_AUFNIRA", "QF_UFIDL"); |
1132 |
2 |
gt("QF_AUFNIRA", "QF_NIA"); |
1133 |
2 |
gt("QF_AUFNIRA", "QF_NRA"); |
1134 |
2 |
eq("QF_AUFNIRA", "QF_AUFNIRA"); |
1135 |
2 |
nc("QF_AUFNIRA", "LRA"); |
1136 |
2 |
nc("QF_AUFNIRA", "NRA"); |
1137 |
2 |
nc("QF_AUFNIRA", "NIA"); |
1138 |
2 |
nc("QF_AUFNIRA", "UFLRA"); |
1139 |
2 |
nc("QF_AUFNIRA", "UFNIA"); |
1140 |
2 |
nc("QF_AUFNIRA", "AUFLIA"); |
1141 |
2 |
nc("QF_AUFNIRA", "AUFLIRA"); |
1142 |
2 |
lt("QF_AUFNIRA", "AUFNIRA"); |
1143 |
2 |
lt("QF_AUFNIRA", "QF_AUFNIRAT"); |
1144 |
|
|
1145 |
2 |
nc("LRA", "QF_UF"); |
1146 |
2 |
gt("LRA", "QF_LRA"); |
1147 |
2 |
nc("LRA", "QF_LIA"); |
1148 |
2 |
nc("LRA", "QF_UFLRA"); |
1149 |
2 |
nc("LRA", "QF_UFLIA"); |
1150 |
2 |
nc("LRA", "QF_AUFLIA"); |
1151 |
2 |
nc("LRA", "QF_AUFLIRA"); |
1152 |
2 |
nc("LRA", "QF_BV"); |
1153 |
2 |
nc("LRA", "QF_ABV"); |
1154 |
2 |
nc("LRA", "QF_AUFBV"); |
1155 |
2 |
nc("LRA", "QF_IDL"); |
1156 |
2 |
gt("LRA", "QF_RDL"); |
1157 |
2 |
nc("LRA", "QF_UFIDL"); |
1158 |
2 |
nc("LRA", "QF_NIA"); |
1159 |
2 |
nc("LRA", "QF_NRA"); |
1160 |
2 |
nc("LRA", "QF_AUFNIRA"); |
1161 |
2 |
eq("LRA", "LRA"); |
1162 |
2 |
lt("LRA", "NRA"); |
1163 |
2 |
nc("LRA", "NIA"); |
1164 |
2 |
lt("LRA", "UFLRA"); |
1165 |
2 |
nc("LRA", "UFNIA"); |
1166 |
2 |
nc("LRA", "AUFLIA"); |
1167 |
2 |
lt("LRA", "AUFLIRA"); |
1168 |
2 |
lt("LRA", "AUFNIRA"); |
1169 |
|
|
1170 |
2 |
nc("NRA", "QF_UF"); |
1171 |
2 |
gt("NRA", "QF_LRA"); |
1172 |
2 |
nc("NRA", "QF_LIA"); |
1173 |
2 |
nc("NRA", "QF_UFLRA"); |
1174 |
2 |
nc("NRA", "QF_UFLIA"); |
1175 |
2 |
nc("NRA", "QF_AUFLIA"); |
1176 |
2 |
nc("NRA", "QF_AUFLIRA"); |
1177 |
2 |
nc("NRA", "QF_BV"); |
1178 |
2 |
nc("NRA", "QF_ABV"); |
1179 |
2 |
nc("NRA", "QF_AUFBV"); |
1180 |
2 |
nc("NRA", "QF_IDL"); |
1181 |
2 |
gt("NRA", "QF_RDL"); |
1182 |
2 |
nc("NRA", "QF_UFIDL"); |
1183 |
2 |
nc("NRA", "QF_NIA"); |
1184 |
2 |
gt("NRA", "QF_NRA"); |
1185 |
2 |
nc("NRA", "QF_AUFNIRA"); |
1186 |
2 |
gt("NRA", "LRA"); |
1187 |
2 |
eq("NRA", "NRA"); |
1188 |
2 |
nc("NRA", "NIA"); |
1189 |
2 |
nc("NRA", "UFLRA"); |
1190 |
2 |
nc("NRA", "UFNIA"); |
1191 |
2 |
nc("NRA", "AUFLIA"); |
1192 |
2 |
nc("NRA", "AUFLIRA"); |
1193 |
2 |
lt("NRA", "AUFNIRA"); |
1194 |
|
|
1195 |
2 |
nc("NIA", "QF_UF"); |
1196 |
2 |
nc("NIA", "QF_LRA"); |
1197 |
2 |
gt("NIA", "QF_LIA"); |
1198 |
2 |
nc("NIA", "QF_UFLRA"); |
1199 |
2 |
nc("NIA", "QF_UFLIA"); |
1200 |
2 |
nc("NIA", "QF_AUFLIA"); |
1201 |
2 |
nc("NIA", "QF_AUFLIRA"); |
1202 |
2 |
nc("NIA", "QF_BV"); |
1203 |
2 |
nc("NIA", "QF_ABV"); |
1204 |
2 |
nc("NIA", "QF_AUFBV"); |
1205 |
2 |
gt("NIA", "QF_IDL"); |
1206 |
2 |
nc("NIA", "QF_RDL"); |
1207 |
2 |
nc("NIA", "QF_UFIDL"); |
1208 |
2 |
gt("NIA", "QF_NIA"); |
1209 |
2 |
nc("NIA", "QF_NRA"); |
1210 |
2 |
nc("NIA", "QF_AUFNIRA"); |
1211 |
2 |
nc("NIA", "LRA"); |
1212 |
2 |
nc("NIA", "NRA"); |
1213 |
2 |
eq("NIA", "NIA"); |
1214 |
2 |
nc("NIA", "UFLRA"); |
1215 |
2 |
lt("NIA", "UFNIA"); |
1216 |
2 |
nc("NIA", "AUFLIA"); |
1217 |
2 |
nc("NIA", "AUFLIRA"); |
1218 |
2 |
lt("NIA", "AUFNIRA"); |
1219 |
|
|
1220 |
2 |
gt("UFLRA", "QF_UF"); |
1221 |
2 |
gt("UFLRA", "QF_LRA"); |
1222 |
2 |
nc("UFLRA", "QF_LIA"); |
1223 |
2 |
gt("UFLRA", "QF_UFLRA"); |
1224 |
2 |
nc("UFLRA", "QF_UFLIA"); |
1225 |
2 |
nc("UFLRA", "QF_AUFLIA"); |
1226 |
2 |
nc("UFLRA", "QF_AUFLIRA"); |
1227 |
2 |
nc("UFLRA", "QF_BV"); |
1228 |
2 |
nc("UFLRA", "QF_ABV"); |
1229 |
2 |
nc("UFLRA", "QF_AUFBV"); |
1230 |
2 |
nc("UFLRA", "QF_IDL"); |
1231 |
2 |
gt("UFLRA", "QF_RDL"); |
1232 |
2 |
nc("UFLRA", "QF_UFIDL"); |
1233 |
2 |
nc("UFLRA", "QF_NIA"); |
1234 |
2 |
nc("UFLRA", "QF_NRA"); |
1235 |
2 |
nc("UFLRA", "QF_AUFNIRA"); |
1236 |
2 |
gt("UFLRA", "LRA"); |
1237 |
2 |
nc("UFLRA", "NRA"); |
1238 |
2 |
nc("UFLRA", "NIA"); |
1239 |
2 |
eq("UFLRA", "UFLRA"); |
1240 |
2 |
nc("UFLRA", "UFNIA"); |
1241 |
2 |
nc("UFLRA", "AUFLIA"); |
1242 |
2 |
lt("UFLRA", "AUFLIRA"); |
1243 |
2 |
lt("UFLRA", "AUFNIRA"); |
1244 |
|
|
1245 |
2 |
gt("UFNIA", "QF_UF"); |
1246 |
2 |
nc("UFNIA", "QF_LRA"); |
1247 |
2 |
gt("UFNIA", "QF_LIA"); |
1248 |
2 |
nc("UFNIA", "QF_UFLRA"); |
1249 |
2 |
gt("UFNIA", "QF_UFLIA"); |
1250 |
2 |
nc("UFNIA", "QF_AUFLIA"); |
1251 |
2 |
nc("UFNIA", "QF_AUFLIRA"); |
1252 |
2 |
nc("UFNIA", "QF_BV"); |
1253 |
2 |
nc("UFNIA", "QF_ABV"); |
1254 |
2 |
nc("UFNIA", "QF_AUFBV"); |
1255 |
2 |
gt("UFNIA", "QF_IDL"); |
1256 |
2 |
nc("UFNIA", "QF_RDL"); |
1257 |
2 |
gt("UFNIA", "QF_UFIDL"); |
1258 |
2 |
gt("UFNIA", "QF_NIA"); |
1259 |
2 |
nc("UFNIA", "QF_NRA"); |
1260 |
2 |
nc("UFNIA", "QF_AUFNIRA"); |
1261 |
2 |
nc("UFNIA", "LRA"); |
1262 |
2 |
nc("UFNIA", "NRA"); |
1263 |
2 |
gt("UFNIA", "NIA"); |
1264 |
2 |
nc("UFNIA", "UFLRA"); |
1265 |
2 |
eq("UFNIA", "UFNIA"); |
1266 |
2 |
nc("UFNIA", "AUFLIA"); |
1267 |
2 |
nc("UFNIA", "AUFLIRA"); |
1268 |
2 |
lt("UFNIA", "AUFNIRA"); |
1269 |
|
|
1270 |
2 |
gt("AUFLIA", "QF_UF"); |
1271 |
2 |
nc("AUFLIA", "QF_LRA"); |
1272 |
2 |
gt("AUFLIA", "QF_LIA"); |
1273 |
2 |
nc("AUFLIA", "QF_UFLRA"); |
1274 |
2 |
gt("AUFLIA", "QF_UFLIA"); |
1275 |
2 |
gt("AUFLIA", "QF_AUFLIA"); |
1276 |
2 |
nc("AUFLIA", "QF_AUFLIRA"); |
1277 |
2 |
nc("AUFLIA", "QF_BV"); |
1278 |
2 |
nc("AUFLIA", "QF_ABV"); |
1279 |
2 |
nc("AUFLIA", "QF_AUFBV"); |
1280 |
2 |
gt("AUFLIA", "QF_IDL"); |
1281 |
2 |
nc("AUFLIA", "QF_RDL"); |
1282 |
2 |
gt("AUFLIA", "QF_UFIDL"); |
1283 |
2 |
nc("AUFLIA", "QF_NIA"); |
1284 |
2 |
nc("AUFLIA", "QF_NRA"); |
1285 |
2 |
nc("AUFLIA", "QF_AUFNIRA"); |
1286 |
2 |
nc("AUFLIA", "LRA"); |
1287 |
2 |
nc("AUFLIA", "NRA"); |
1288 |
2 |
nc("AUFLIA", "NIA"); |
1289 |
2 |
nc("AUFLIA", "UFLRA"); |
1290 |
2 |
nc("AUFLIA", "UFNIA"); |
1291 |
2 |
eq("AUFLIA", "AUFLIA"); |
1292 |
2 |
lt("AUFLIA", "AUFLIRA"); |
1293 |
2 |
lt("AUFLIA", "AUFNIRA"); |
1294 |
|
|
1295 |
2 |
gt("AUFLIRA", "QF_UF"); |
1296 |
2 |
gt("AUFLIRA", "QF_LRA"); |
1297 |
2 |
gt("AUFLIRA", "QF_LIA"); |
1298 |
2 |
gt("AUFLIRA", "QF_UFLRA"); |
1299 |
2 |
gt("AUFLIRA", "QF_UFLIA"); |
1300 |
2 |
gt("AUFLIRA", "QF_AUFLIA"); |
1301 |
2 |
gt("AUFLIRA", "QF_AUFLIRA"); |
1302 |
2 |
nc("AUFLIRA", "QF_BV"); |
1303 |
2 |
nc("AUFLIRA", "QF_ABV"); |
1304 |
2 |
nc("AUFLIRA", "QF_AUFBV"); |
1305 |
2 |
gt("AUFLIRA", "QF_IDL"); |
1306 |
2 |
gt("AUFLIRA", "QF_RDL"); |
1307 |
2 |
gt("AUFLIRA", "QF_UFIDL"); |
1308 |
2 |
nc("AUFLIRA", "QF_NIA"); |
1309 |
2 |
nc("AUFLIRA", "QF_NRA"); |
1310 |
2 |
nc("AUFLIRA", "QF_AUFNIRA"); |
1311 |
2 |
gt("AUFLIRA", "LRA"); |
1312 |
2 |
nc("AUFLIRA", "NRA"); |
1313 |
2 |
nc("AUFLIRA", "NIA"); |
1314 |
2 |
gt("AUFLIRA", "UFLRA"); |
1315 |
2 |
nc("AUFLIRA", "UFNIA"); |
1316 |
2 |
gt("AUFLIRA", "AUFLIA"); |
1317 |
2 |
eq("AUFLIRA", "AUFLIRA"); |
1318 |
2 |
lt("AUFLIRA", "AUFNIRA"); |
1319 |
|
|
1320 |
2 |
gt("AUFNIRA", "QF_UF"); |
1321 |
2 |
gt("AUFNIRA", "QF_LRA"); |
1322 |
2 |
gt("AUFNIRA", "QF_LIA"); |
1323 |
2 |
gt("AUFNIRA", "QF_UFLRA"); |
1324 |
2 |
gt("AUFNIRA", "QF_UFLIA"); |
1325 |
2 |
gt("AUFNIRA", "QF_AUFLIA"); |
1326 |
2 |
gt("AUFNIRA", "QF_AUFLIRA"); |
1327 |
2 |
nc("AUFNIRA", "QF_BV"); |
1328 |
2 |
nc("AUFNIRA", "QF_ABV"); |
1329 |
2 |
nc("AUFNIRA", "QF_AUFBV"); |
1330 |
2 |
gt("AUFNIRA", "QF_IDL"); |
1331 |
2 |
gt("AUFNIRA", "QF_RDL"); |
1332 |
2 |
gt("AUFNIRA", "QF_UFIDL"); |
1333 |
2 |
gt("AUFNIRA", "QF_NIA"); |
1334 |
2 |
gt("AUFNIRA", "QF_NRA"); |
1335 |
2 |
gt("AUFNIRA", "QF_AUFNIRA"); |
1336 |
2 |
gt("AUFNIRA", "LRA"); |
1337 |
2 |
gt("AUFNIRA", "NRA"); |
1338 |
2 |
gt("AUFNIRA", "NIA"); |
1339 |
2 |
gt("AUFNIRA", "UFLRA"); |
1340 |
2 |
gt("AUFNIRA", "UFNIA"); |
1341 |
2 |
gt("AUFNIRA", "AUFLIA"); |
1342 |
2 |
gt("AUFNIRA", "AUFLIRA"); |
1343 |
2 |
eq("AUFNIRA", "AUFNIRA"); |
1344 |
2 |
lt("AUFNIRA", "AUFNIRAT"); |
1345 |
|
|
1346 |
2 |
gt("QF_UFC", "QF_UF"); |
1347 |
2 |
gt("QF_UFCLRA", "QF_UFLRA"); |
1348 |
|
|
1349 |
2 |
gt(ufHo, "QF_UF"); |
1350 |
2 |
} |
1351 |
|
} // namespace test |
1352 |
12 |
} // namespace cvc5 |