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