GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/logic_info_white.cpp Lines: 1233 1236 99.8 %
Date: 2021-03-23 Branches: 4144 12768 32.5 %

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