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