GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_quantifiers_bv_inverter_white.cpp Lines: 927 943 98.3 %
Date: 2021-03-22 Branches: 631 1422 44.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_quantifiers_bv_inverter_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mathias Preiner, Abdalrhman Mohamed
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 tests for BV inverter.
13
 **
14
 ** Unit tests for BV inverter.
15
 **/
16
17
#include "expr/node.h"
18
#include "test_smt.h"
19
#include "theory/bv/theory_bv_utils.h"
20
#include "theory/quantifiers/bv_inverter_utils.h"
21
#include "util/result.h"
22
23
namespace CVC4 {
24
25
using namespace kind;
26
using namespace theory;
27
using namespace theory::quantifiers;
28
using namespace theory::quantifiers::utils;
29
30
namespace test {
31
32
1024
class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
33
{
34
 protected:
35
512
  void SetUp() override
36
  {
37
512
    TestSmtNoFinishInit::SetUp();
38
512
    d_smtEngine->setOption("cegqi-full", "true");
39
512
    d_smtEngine->setOption("produce-models", "true");
40
512
    d_smtEngine->finishInit();
41
42
512
    d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4));
43
512
    d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4));
44
512
    d_sk = d_nodeManager->mkSkolem("sk", d_t.getType());
45
512
    d_x = d_nodeManager->mkBoundVar(d_t.getType());
46
512
    d_bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {d_x});
47
512
  }
48
49
112
  void runTestPred(bool pol,
50
                   Kind k,
51
                   Node x,
52
                   Node (*getic)(bool, Kind, Node, Node))
53
  {
54
112
    ASSERT_TRUE(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL
55
112
                || k == BITVECTOR_UGT || k == BITVECTOR_SGT);
56
112
    ASSERT_TRUE(k != EQUAL || pol == false);
57
58
224
    Node sc = getic(pol, k, d_sk, d_t);
59
112
    Kind ksc = sc.getKind();
60
112
    ASSERT_TRUE((k == BITVECTOR_ULT && pol == false)
61
                || (k == BITVECTOR_SLT && pol == false)
62
                || (k == BITVECTOR_UGT && pol == false)
63
112
                || (k == BITVECTOR_SGT && pol == false) || ksc == IMPLIES);
64
224
    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
65
112
    if (!pol)
66
    {
67
56
      if (k == BITVECTOR_ULT)
68
      {
69
14
        k = BITVECTOR_UGE;
70
      }
71
42
      else if (k == BITVECTOR_UGT)
72
      {
73
14
        k = BITVECTOR_ULE;
74
      }
75
28
      else if (k == BITVECTOR_SLT)
76
      {
77
14
        k = BITVECTOR_SGE;
78
      }
79
14
      else if (k == BITVECTOR_SGT)
80
      {
81
14
        k = BITVECTOR_ULE;
82
      }
83
      else
84
      {
85
        ASSERT_TRUE(k == EQUAL);
86
        k = DISTINCT;
87
      }
88
    }
89
224
    Node body = d_nodeManager->mkNode(k, x, d_t);
90
224
    Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body);
91
224
    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
92
224
    Result res = d_smtEngine->checkSat(a);
93
112
    ASSERT_EQ(res.d_sat, Result::UNSAT);
94
  }
95
96
320
  void runTest(bool pol,
97
               Kind litk,
98
               Kind k,
99
               unsigned idx,
100
               Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node))
101
  {
102
320
    ASSERT_TRUE(k == BITVECTOR_MULT || k == BITVECTOR_UREM
103
                || k == BITVECTOR_UDIV || k == BITVECTOR_AND
104
                || k == BITVECTOR_OR || k == BITVECTOR_LSHR
105
320
                || k == BITVECTOR_ASHR || k == BITVECTOR_SHL);
106
107
640
    Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t);
108
320
    ASSERT_FALSE(sc.isNull());
109
320
    Kind ksc = sc.getKind();
110
320
    ASSERT_TRUE((k == BITVECTOR_UDIV && idx == 1 && pol == false)
111
                || (k == BITVECTOR_ASHR && idx == 0 && pol == false)
112
320
                || ksc == IMPLIES);
113
640
    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
114
    Node body = idx == 0 ? d_nodeManager->mkNode(
115
480
                    litk, d_nodeManager->mkNode(k, d_x, d_s), d_t)
116
                         : d_nodeManager->mkNode(
117
1120
                             litk, d_nodeManager->mkNode(k, d_s, d_x), d_t);
118
    Node scr =
119
640
        d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode());
120
640
    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
121
640
    Result res = d_smtEngine->checkSat(a);
122
320
    if (res.d_sat == Result::SAT)
123
    {
124
      std::cout << std::endl;
125
      std::cout << "s " << d_smtEngine->getValue(d_s) << std::endl;
126
      std::cout << "t " << d_smtEngine->getValue(d_t) << std::endl;
127
      std::cout << "x " << d_smtEngine->getValue(d_x) << std::endl;
128
    }
129
320
    ASSERT_EQ(res.d_sat, Result::UNSAT);
130
  }
131
132
60
  void runTestConcat(bool pol, Kind litk, unsigned idx)
133
  {
134
120
    Node s1, s2, sv_t;
135
120
    Node x, t, sk;
136
120
    Node sc;
137
138
60
    if (idx == 0)
139
    {
140
20
      s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
141
20
      x = d_nodeManager->mkBoundVar(s2.getType());
142
20
      sk = d_nodeManager->mkSkolem("sk", s2.getType());
143
20
      t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
144
20
      sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, x, s2);
145
20
      sc = getICBvConcat(pol, litk, 0, sk, sv_t, t);
146
    }
147
40
    else if (idx == 1)
148
    {
149
20
      s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
150
20
      x = d_nodeManager->mkBoundVar(s1.getType());
151
20
      sk = d_nodeManager->mkSkolem("sk", s1.getType());
152
20
      t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
153
20
      sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x);
154
20
      sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
155
    }
156
    else
157
    {
158
20
      ASSERT_TRUE(idx == 2);
159
20
      s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
160
20
      s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
161
20
      x = d_nodeManager->mkBoundVar(s2.getType());
162
20
      sk = d_nodeManager->mkSkolem("sk", s1.getType());
163
20
      t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(12));
164
20
      sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x, s2);
165
20
      sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
166
    }
167
168
60
    ASSERT_FALSE(sc.isNull());
169
60
    Kind ksc = sc.getKind();
170
60
    ASSERT_TRUE((litk == kind::EQUAL && pol == false) || ksc == IMPLIES);
171
120
    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
172
120
    Node body = d_nodeManager->mkNode(litk, sv_t, t);
173
120
    Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x});
174
    Node scr =
175
120
        d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
176
120
    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
177
120
    Result res = d_smtEngine->checkSat(a);
178
60
    if (res.d_sat == Result::SAT)
179
    {
180
      std::cout << std::endl;
181
      if (!s1.isNull())
182
        std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl;
183
      if (!s2.isNull())
184
        std::cout << "s2 " << d_smtEngine->getValue(s2) << std::endl;
185
      std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
186
      std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
187
    }
188
60
    ASSERT_TRUE(res.d_sat == Result::UNSAT);
189
  }
190
191
20
  void runTestSext(bool pol, Kind litk)
192
  {
193
20
    unsigned ws = 3;
194
20
    unsigned wx = 5;
195
20
    unsigned w = 8;
196
197
40
    Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(wx));
198
40
    Node sk = d_nodeManager->mkSkolem("sk", x.getType());
199
20
    x = d_nodeManager->mkBoundVar(x.getType());
200
201
40
    Node t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(w));
202
40
    Node sv_t = bv::utils::mkSignExtend(x, ws);
203
40
    Node sc = getICBvSext(pol, litk, 0, sk, sv_t, t);
204
205
20
    ASSERT_FALSE(sc.isNull());
206
20
    Kind ksc = sc.getKind();
207
20
    ASSERT_TRUE((litk == kind::EQUAL && pol == false)
208
                || (litk == kind::BITVECTOR_ULT && pol == false)
209
                || (litk == kind::BITVECTOR_UGT && pol == false)
210
20
                || ksc == IMPLIES);
211
40
    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
212
40
    Node body = d_nodeManager->mkNode(litk, sv_t, t);
213
40
    Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x});
214
    Node scr =
215
40
        d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
216
40
    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
217
40
    Result res = d_smtEngine->checkSat(a);
218
20
    if (res.d_sat == Result::SAT)
219
    {
220
      std::cout << std::endl;
221
      std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
222
      std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
223
    }
224
20
    ASSERT_TRUE(res.d_sat == Result::UNSAT);
225
  }
226
227
  Node d_s;
228
  Node d_t;
229
  Node d_sk;
230
  Node d_x;
231
  Node d_bvarlist;
232
};
233
234
/* Generic invertibility conditions for LT ---------------------------------  */
235
236
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ult_true)
237
{
238
2
  runTestPred(true, BITVECTOR_ULT, d_x, getICBvUltUgt);
239
2
}
240
241
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ult_false)
242
{
243
2
  runTestPred(false, BITVECTOR_ULT, d_x, getICBvUltUgt);
244
2
}
245
246
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ugt_true)
247
{
248
2
  runTestPred(true, BITVECTOR_UGT, d_x, getICBvUltUgt);
249
2
}
250
251
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ugt_false)
252
{
253
2
  runTestPred(false, BITVECTOR_UGT, d_x, getICBvUltUgt);
254
2
}
255
256
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_slt_true)
257
{
258
2
  runTestPred(true, BITVECTOR_SLT, d_x, getICBvSltSgt);
259
2
}
260
261
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_slt_false)
262
{
263
2
  runTestPred(false, BITVECTOR_SLT, d_x, getICBvSltSgt);
264
2
}
265
266
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sgt_true)
267
{
268
2
  runTestPred(true, BITVECTOR_SGT, d_x, getICBvSltSgt);
269
2
}
270
271
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, test_getIC_bv_sgt_false)
272
{
273
2
  runTestPred(false, BITVECTOR_SGT, d_x, getICBvSltSgt);
274
2
}
275
276
/* Equality and Disequality   ----------------------------------------------  */
277
278
/* Mult */
279
280
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_true0)
281
{
282
2
  runTest(true, EQUAL, BITVECTOR_MULT, 0, getICBvMult);
283
2
}
284
285
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_trueu)
286
{
287
2
  runTest(true, EQUAL, BITVECTOR_MULT, 1, getICBvMult);
288
2
}
289
290
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_false0)
291
{
292
2
  runTest(false, EQUAL, BITVECTOR_MULT, 0, getICBvMult);
293
2
}
294
295
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_false1)
296
{
297
2
  runTest(false, EQUAL, BITVECTOR_MULT, 1, getICBvMult);
298
2
}
299
300
/* Urem */
301
302
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true0)
303
{
304
2
  runTest(true, EQUAL, BITVECTOR_UREM, 0, getICBvUrem);
305
2
}
306
307
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true1)
308
{
309
2
  runTest(true, EQUAL, BITVECTOR_UREM, 1, getICBvUrem);
310
2
}
311
312
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false0)
313
{
314
2
  runTest(false, EQUAL, BITVECTOR_UREM, 0, getICBvUrem);
315
2
}
316
317
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false1)
318
{
319
2
  runTest(false, EQUAL, BITVECTOR_UREM, 1, getICBvUrem);
320
2
}
321
322
/* Udiv */
323
324
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true0)
325
{
326
2
  runTest(true, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv);
327
2
}
328
329
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true1)
330
{
331
2
  runTest(true, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv);
332
2
}
333
334
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false0)
335
{
336
2
  runTest(false, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv);
337
2
}
338
339
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false1)
340
{
341
2
  runTest(false, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv);
342
2
}
343
344
/* And */
345
346
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_eq_true0)
347
{
348
2
  runTest(true, EQUAL, BITVECTOR_AND, 0, getICBvAndOr);
349
2
}
350
351
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_eq_true1)
352
{
353
2
  runTest(true, EQUAL, BITVECTOR_AND, 1, getICBvAndOr);
354
2
}
355
356
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_eq_false0)
357
{
358
2
  runTest(false, EQUAL, BITVECTOR_AND, 0, getICBvAndOr);
359
2
}
360
361
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_eq_false1)
362
{
363
2
  runTest(false, EQUAL, BITVECTOR_AND, 1, getICBvAndOr);
364
2
}
365
366
/* Or */
367
368
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_eq_true0)
369
{
370
2
  runTest(true, EQUAL, BITVECTOR_OR, 0, getICBvAndOr);
371
2
}
372
373
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_eq_true1)
374
{
375
2
  runTest(true, EQUAL, BITVECTOR_OR, 1, getICBvAndOr);
376
2
}
377
378
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_eq_false0)
379
{
380
2
  runTest(false, EQUAL, BITVECTOR_OR, 0, getICBvAndOr);
381
2
}
382
383
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_eq_false1)
384
{
385
2
  runTest(false, EQUAL, BITVECTOR_OR, 1, getICBvAndOr);
386
2
}
387
388
/* Lshr */
389
390
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_eq_true0)
391
{
392
2
  runTest(true, EQUAL, BITVECTOR_LSHR, 0, getICBvLshr);
393
2
}
394
395
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_eq_true1)
396
{
397
2
  runTest(true, EQUAL, BITVECTOR_LSHR, 1, getICBvLshr);
398
2
}
399
400
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_eq_false0)
401
{
402
2
  runTest(false, EQUAL, BITVECTOR_LSHR, 0, getICBvLshr);
403
2
}
404
405
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_eq_false1)
406
{
407
2
  runTest(false, EQUAL, BITVECTOR_LSHR, 1, getICBvLshr);
408
2
}
409
410
/* Ashr */
411
412
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_eq_true0)
413
{
414
2
  runTest(true, EQUAL, BITVECTOR_ASHR, 0, getICBvAshr);
415
2
}
416
417
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_eq_true1)
418
{
419
2
  runTest(true, EQUAL, BITVECTOR_ASHR, 1, getICBvAshr);
420
2
}
421
422
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_eq_false0)
423
{
424
2
  runTest(false, EQUAL, BITVECTOR_ASHR, 0, getICBvAshr);
425
2
}
426
427
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_eq_false1)
428
{
429
2
  runTest(false, EQUAL, BITVECTOR_ASHR, 1, getICBvAshr);
430
2
}
431
432
/* Shl */
433
434
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_eq_true0)
435
{
436
2
  runTest(true, EQUAL, BITVECTOR_SHL, 0, getICBvShl);
437
2
}
438
439
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_eq_true1)
440
{
441
2
  runTest(true, EQUAL, BITVECTOR_SHL, 1, getICBvShl);
442
2
}
443
444
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_eq_false0)
445
{
446
2
  runTest(false, EQUAL, BITVECTOR_SHL, 0, getICBvShl);
447
2
}
448
449
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_eq_false1)
450
{
451
2
  runTest(false, EQUAL, BITVECTOR_SHL, 1, getICBvShl);
452
2
}
453
454
/* Concat */
455
456
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_true0)
457
{
458
2
  runTestConcat(true, EQUAL, 0);
459
2
}
460
461
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_true1)
462
{
463
2
  runTestConcat(true, EQUAL, 1);
464
2
}
465
466
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_true2)
467
{
468
2
  runTestConcat(true, EQUAL, 2);
469
2
}
470
471
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_false0)
472
{
473
2
  runTestConcat(false, EQUAL, 0);
474
2
}
475
476
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_false1)
477
{
478
2
  runTestConcat(false, EQUAL, 1);
479
2
}
480
481
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_eq_false2)
482
{
483
2
  runTestConcat(false, EQUAL, 2);
484
2
}
485
486
/* Sext */
487
488
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_eq_true)
489
{
490
2
  runTestSext(true, EQUAL);
491
2
}
492
493
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_eq_false)
494
{
495
2
  runTestSext(false, EQUAL);
496
2
}
497
498
/* Inequality --------------------------------------------------------------  */
499
500
/* Not */
501
502
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ult_true0)
503
{
504
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
505
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
506
2
}
507
508
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ult_true1)
509
{
510
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
511
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
512
2
}
513
514
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ult_false0)
515
{
516
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
517
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
518
2
}
519
520
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ult_false1)
521
{
522
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
523
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
524
2
}
525
526
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ugt_true0)
527
{
528
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
529
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
530
2
}
531
532
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ugt_true1)
533
{
534
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
535
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
536
2
}
537
538
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ugt_false0)
539
{
540
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
541
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
542
2
}
543
544
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_ugt_false1)
545
{
546
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
547
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
548
2
}
549
550
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_slt_true0)
551
{
552
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
553
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
554
2
}
555
556
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_slt_true1)
557
{
558
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
559
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
560
2
}
561
562
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_slt_false0)
563
{
564
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
565
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
566
2
}
567
568
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_slt_false1)
569
{
570
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
571
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
572
2
}
573
574
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_sgt_true0)
575
{
576
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
577
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
578
2
}
579
580
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_sgt_true1)
581
{
582
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
583
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
584
2
}
585
586
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_sgt_false0)
587
{
588
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
589
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
590
2
}
591
592
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_not_sgt_false1)
593
{
594
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NOT, d_x);
595
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
596
2
}
597
598
/* Neg */
599
600
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ult_true0)
601
{
602
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
603
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
604
2
}
605
606
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ult_true1)
607
{
608
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
609
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
610
2
}
611
612
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ult_false0)
613
{
614
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
615
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
616
2
}
617
618
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ult_false1)
619
{
620
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
621
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
622
2
}
623
624
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ugt_true0)
625
{
626
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
627
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
628
2
}
629
630
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ugt_true1)
631
{
632
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
633
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
634
2
}
635
636
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ugt_false0)
637
{
638
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
639
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
640
2
}
641
642
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_ugt_false1)
643
{
644
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
645
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
646
2
}
647
648
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_slt_true0)
649
{
650
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
651
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
652
2
}
653
654
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_slt_true1)
655
{
656
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
657
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
658
2
}
659
660
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_slt_false0)
661
{
662
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
663
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
664
2
}
665
666
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_slt_false1)
667
{
668
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
669
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
670
2
}
671
672
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_true0)
673
{
674
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
675
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
676
2
}
677
678
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_true1)
679
{
680
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
681
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
682
2
}
683
684
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_false0)
685
{
686
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
687
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
688
2
}
689
690
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_false1)
691
{
692
4
  Node x = d_nodeManager->mkNode(BITVECTOR_NEG, d_x);
693
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
694
2
}
695
696
/* Add */
697
698
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true0)
699
{
700
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
701
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
702
2
}
703
704
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true1)
705
{
706
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
707
2
  runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
708
2
}
709
710
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false0)
711
{
712
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
713
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
714
2
}
715
716
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false1)
717
{
718
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
719
2
  runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
720
2
}
721
722
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true0)
723
{
724
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
725
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
726
2
}
727
728
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true1)
729
{
730
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
731
2
  runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
732
2
}
733
734
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false0)
735
{
736
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
737
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
738
2
}
739
740
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false1)
741
{
742
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
743
2
  runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
744
2
}
745
746
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true0)
747
{
748
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
749
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
750
2
}
751
752
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true1)
753
{
754
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
755
2
  runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
756
2
}
757
758
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false0)
759
{
760
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
761
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
762
2
}
763
764
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false1)
765
{
766
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
767
2
  runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
768
2
}
769
770
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true0)
771
{
772
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
773
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
774
2
}
775
776
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true1)
777
{
778
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
779
2
  runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
780
2
}
781
782
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false0)
783
{
784
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
785
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
786
2
}
787
788
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false1)
789
{
790
4
  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
791
2
  runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
792
2
}
793
794
/* Mult */
795
796
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ult_true0)
797
{
798
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_MULT, 0, getICBvMult);
799
2
}
800
801
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ult_true1)
802
{
803
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_MULT, 1, getICBvMult);
804
2
}
805
806
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ult_false0)
807
{
808
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_MULT, 0, getICBvMult);
809
2
}
810
811
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ult_false1)
812
{
813
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_MULT, 1, getICBvMult);
814
2
}
815
816
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ugt_true0)
817
{
818
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_MULT, 0, getICBvMult);
819
2
}
820
821
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ugt_true1)
822
{
823
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_MULT, 1, getICBvMult);
824
2
}
825
826
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ugt_false0)
827
{
828
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_MULT, 0, getICBvMult);
829
2
}
830
831
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_ugt_false1)
832
{
833
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_MULT, 1, getICBvMult);
834
2
}
835
836
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_slt_true0)
837
{
838
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_MULT, 0, getICBvMult);
839
2
}
840
841
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_slt_true1)
842
{
843
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_MULT, 1, getICBvMult);
844
2
}
845
846
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_slt_false0)
847
{
848
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_MULT, 0, getICBvMult);
849
2
}
850
851
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_slt_false1)
852
{
853
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_MULT, 1, getICBvMult);
854
2
}
855
856
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_true0)
857
{
858
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_MULT, 0, getICBvMult);
859
2
}
860
861
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_true1)
862
{
863
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_MULT, 1, getICBvMult);
864
2
}
865
866
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_false0)
867
{
868
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_MULT, 0, getICBvMult);
869
2
}
870
871
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_false1)
872
{
873
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_MULT, 1, getICBvMult);
874
2
}
875
876
/* Urem */
877
878
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true0)
879
{
880
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem);
881
2
}
882
883
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true1)
884
{
885
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem);
886
2
}
887
888
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false0)
889
{
890
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem);
891
2
}
892
893
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false1)
894
{
895
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem);
896
2
}
897
898
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true0)
899
{
900
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem);
901
2
}
902
903
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true1)
904
{
905
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem);
906
2
}
907
908
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false0)
909
{
910
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem);
911
2
}
912
913
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false1)
914
{
915
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem);
916
2
}
917
918
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true0)
919
{
920
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem);
921
2
}
922
923
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true1)
924
{
925
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem);
926
2
}
927
928
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false0)
929
{
930
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem);
931
2
}
932
933
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false1)
934
{
935
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem);
936
2
}
937
938
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true0)
939
{
940
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem);
941
2
}
942
943
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true1)
944
{
945
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem);
946
2
}
947
948
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false0)
949
{
950
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem);
951
2
}
952
953
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false1)
954
{
955
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem);
956
2
}
957
958
/* Udiv */
959
960
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true0)
961
{
962
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv);
963
2
}
964
965
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true1)
966
{
967
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv);
968
2
}
969
970
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false0)
971
{
972
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv);
973
2
}
974
975
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false1)
976
{
977
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv);
978
2
}
979
980
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true0)
981
{
982
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv);
983
2
}
984
985
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true1)
986
{
987
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv);
988
2
}
989
990
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false0)
991
{
992
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv);
993
2
}
994
995
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false1)
996
{
997
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv);
998
2
}
999
1000
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true0)
1001
{
1002
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv);
1003
2
}
1004
1005
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true1)
1006
{
1007
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv);
1008
2
}
1009
1010
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false0)
1011
{
1012
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv);
1013
2
}
1014
1015
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false1)
1016
{
1017
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv);
1018
2
}
1019
1020
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true0)
1021
{
1022
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv);
1023
2
}
1024
1025
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true1)
1026
{
1027
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv);
1028
2
}
1029
1030
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false0)
1031
{
1032
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv);
1033
2
}
1034
1035
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false1)
1036
{
1037
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv);
1038
2
}
1039
1040
/* And */
1041
1042
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ult_true0)
1043
{
1044
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_AND, 0, getICBvAndOr);
1045
2
}
1046
1047
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ult_true1)
1048
{
1049
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_AND, 1, getICBvAndOr);
1050
2
}
1051
1052
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ult_false0)
1053
{
1054
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_AND, 0, getICBvAndOr);
1055
2
}
1056
1057
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ult_false1)
1058
{
1059
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_AND, 1, getICBvAndOr);
1060
2
}
1061
1062
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ugt_true0)
1063
{
1064
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_AND, 0, getICBvAndOr);
1065
2
}
1066
1067
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ugt_true1)
1068
{
1069
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_AND, 1, getICBvAndOr);
1070
2
}
1071
1072
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ugt_false0)
1073
{
1074
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_AND, 0, getICBvAndOr);
1075
2
}
1076
1077
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_ugt_false1)
1078
{
1079
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_AND, 1, getICBvAndOr);
1080
2
}
1081
1082
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_slt_true0)
1083
{
1084
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_AND, 0, getICBvAndOr);
1085
2
}
1086
1087
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_slt_true1)
1088
{
1089
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_AND, 1, getICBvAndOr);
1090
2
}
1091
1092
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_slt_false0)
1093
{
1094
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_AND, 0, getICBvAndOr);
1095
2
}
1096
1097
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_slt_false1)
1098
{
1099
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_AND, 1, getICBvAndOr);
1100
2
}
1101
1102
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_sgt_true0)
1103
{
1104
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_AND, 0, getICBvAndOr);
1105
2
}
1106
1107
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_sgt_true1)
1108
{
1109
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_AND, 1, getICBvAndOr);
1110
2
}
1111
1112
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_sgt_false0)
1113
{
1114
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_AND, 0, getICBvAndOr);
1115
2
}
1116
1117
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_and_sgt_false1)
1118
{
1119
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_AND, 1, getICBvAndOr);
1120
2
}
1121
1122
/* Or */
1123
1124
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ult_true0)
1125
{
1126
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_OR, 0, getICBvAndOr);
1127
2
}
1128
1129
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ult_true1)
1130
{
1131
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_OR, 1, getICBvAndOr);
1132
2
}
1133
1134
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ult_false0)
1135
{
1136
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_OR, 0, getICBvAndOr);
1137
2
}
1138
1139
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ult_false1)
1140
{
1141
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_OR, 1, getICBvAndOr);
1142
2
}
1143
1144
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ugt_true0)
1145
{
1146
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_OR, 0, getICBvAndOr);
1147
2
}
1148
1149
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ugt_true1)
1150
{
1151
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_OR, 1, getICBvAndOr);
1152
2
}
1153
1154
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ugt_false0)
1155
{
1156
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_OR, 0, getICBvAndOr);
1157
2
}
1158
1159
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_ugt_false1)
1160
{
1161
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_OR, 1, getICBvAndOr);
1162
2
}
1163
1164
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_slt_true0)
1165
{
1166
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_OR, 0, getICBvAndOr);
1167
2
}
1168
1169
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_slt_true1)
1170
{
1171
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_OR, 1, getICBvAndOr);
1172
2
}
1173
1174
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_slt_false0)
1175
{
1176
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_OR, 0, getICBvAndOr);
1177
2
}
1178
1179
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_slt_false1)
1180
{
1181
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_OR, 1, getICBvAndOr);
1182
2
}
1183
1184
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_sgt_true0)
1185
{
1186
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_OR, 0, getICBvAndOr);
1187
2
}
1188
1189
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_sgt_true1)
1190
{
1191
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_OR, 1, getICBvAndOr);
1192
2
}
1193
1194
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_sgt_false0)
1195
{
1196
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_OR, 0, getICBvAndOr);
1197
2
}
1198
1199
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_or_sgt_false1)
1200
{
1201
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_OR, 1, getICBvAndOr);
1202
2
}
1203
1204
/* Lshr */
1205
1206
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ult_true0)
1207
{
1208
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_LSHR, 0, getICBvLshr);
1209
2
}
1210
1211
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ult_true1)
1212
{
1213
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_LSHR, 1, getICBvLshr);
1214
2
}
1215
1216
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ult_false0)
1217
{
1218
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_LSHR, 0, getICBvLshr);
1219
2
}
1220
1221
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ult_false1)
1222
{
1223
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_LSHR, 1, getICBvLshr);
1224
2
}
1225
1226
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ugt_true0)
1227
{
1228
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_LSHR, 0, getICBvLshr);
1229
2
}
1230
1231
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ugt_true1)
1232
{
1233
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_LSHR, 1, getICBvLshr);
1234
2
}
1235
1236
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ugt_false0)
1237
{
1238
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_LSHR, 0, getICBvLshr);
1239
2
}
1240
1241
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_ugt_false1)
1242
{
1243
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_LSHR, 1, getICBvLshr);
1244
2
}
1245
1246
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_slt_true0)
1247
{
1248
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_LSHR, 0, getICBvLshr);
1249
2
}
1250
1251
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_slt_true1)
1252
{
1253
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_LSHR, 1, getICBvLshr);
1254
2
}
1255
1256
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_slt_false0)
1257
{
1258
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_LSHR, 0, getICBvLshr);
1259
2
}
1260
1261
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_slt_false1)
1262
{
1263
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_LSHR, 1, getICBvLshr);
1264
2
}
1265
1266
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_sgt_true0)
1267
{
1268
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_LSHR, 0, getICBvLshr);
1269
2
}
1270
1271
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_sgt_true1)
1272
{
1273
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_LSHR, 1, getICBvLshr);
1274
2
}
1275
1276
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_sgt_false0)
1277
{
1278
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_LSHR, 0, getICBvLshr);
1279
2
}
1280
1281
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_lshr_sgt_false1)
1282
{
1283
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_LSHR, 1, getICBvLshr);
1284
2
}
1285
1286
/* Ashr */
1287
1288
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ult_true0)
1289
{
1290
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_ASHR, 0, getICBvAshr);
1291
2
}
1292
1293
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ult_true1)
1294
{
1295
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_ASHR, 1, getICBvAshr);
1296
2
}
1297
1298
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ult_false0)
1299
{
1300
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_ASHR, 0, getICBvAshr);
1301
2
}
1302
1303
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ult_false1)
1304
{
1305
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_ASHR, 1, getICBvAshr);
1306
2
}
1307
1308
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ugt_true0)
1309
{
1310
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_ASHR, 0, getICBvAshr);
1311
2
}
1312
1313
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ugt_true1)
1314
{
1315
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_ASHR, 1, getICBvAshr);
1316
2
}
1317
1318
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ugt_false0)
1319
{
1320
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_ASHR, 0, getICBvAshr);
1321
2
}
1322
1323
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_ugt_false1)
1324
{
1325
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_ASHR, 1, getICBvAshr);
1326
2
}
1327
1328
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_slt_true0)
1329
{
1330
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_ASHR, 0, getICBvAshr);
1331
2
}
1332
1333
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_slt_true1)
1334
{
1335
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_ASHR, 1, getICBvAshr);
1336
2
}
1337
1338
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_slt_false0)
1339
{
1340
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_ASHR, 0, getICBvAshr);
1341
2
}
1342
1343
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_slt_false1)
1344
{
1345
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_ASHR, 1, getICBvAshr);
1346
2
}
1347
1348
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_sgt_true0)
1349
{
1350
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_ASHR, 0, getICBvAshr);
1351
2
}
1352
1353
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_sgt_true1)
1354
{
1355
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_ASHR, 1, getICBvAshr);
1356
2
}
1357
1358
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_sgt_false0)
1359
{
1360
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_ASHR, 0, getICBvAshr);
1361
2
}
1362
1363
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_ashr_sgt_false1)
1364
{
1365
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_ASHR, 1, getICBvAshr);
1366
2
}
1367
1368
/* Shl */
1369
1370
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ult_true0)
1371
{
1372
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_SHL, 0, getICBvShl);
1373
2
}
1374
1375
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ult_true1)
1376
{
1377
2
  runTest(true, BITVECTOR_ULT, BITVECTOR_SHL, 1, getICBvShl);
1378
2
}
1379
1380
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ult_false0)
1381
{
1382
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_SHL, 0, getICBvShl);
1383
2
}
1384
1385
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ult_false1)
1386
{
1387
2
  runTest(false, BITVECTOR_ULT, BITVECTOR_SHL, 1, getICBvShl);
1388
2
}
1389
1390
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ugt_true0)
1391
{
1392
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_SHL, 0, getICBvShl);
1393
2
}
1394
1395
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ugt_true1)
1396
{
1397
2
  runTest(true, BITVECTOR_UGT, BITVECTOR_SHL, 1, getICBvShl);
1398
2
}
1399
1400
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ugt_false0)
1401
{
1402
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_SHL, 0, getICBvShl);
1403
2
}
1404
1405
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_ugt_false1)
1406
{
1407
2
  runTest(false, BITVECTOR_UGT, BITVECTOR_SHL, 1, getICBvShl);
1408
2
}
1409
1410
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_slt_true0)
1411
{
1412
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_SHL, 0, getICBvShl);
1413
2
}
1414
1415
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_slt_true1)
1416
{
1417
2
  runTest(true, BITVECTOR_SLT, BITVECTOR_SHL, 1, getICBvShl);
1418
2
}
1419
1420
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_slt_false0)
1421
{
1422
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_SHL, 0, getICBvShl);
1423
2
}
1424
1425
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_slt_false1)
1426
{
1427
2
  runTest(false, BITVECTOR_SLT, BITVECTOR_SHL, 1, getICBvShl);
1428
2
}
1429
1430
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_sgt_true0)
1431
{
1432
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_SHL, 0, getICBvShl);
1433
2
}
1434
1435
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_sgt_true1)
1436
{
1437
2
  runTest(true, BITVECTOR_SGT, BITVECTOR_SHL, 1, getICBvShl);
1438
2
}
1439
1440
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_sgt_false0)
1441
{
1442
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_SHL, 0, getICBvShl);
1443
2
}
1444
1445
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_shl_sgt_false1)
1446
{
1447
2
  runTest(false, BITVECTOR_SGT, BITVECTOR_SHL, 1, getICBvShl);
1448
2
}
1449
1450
/* Concat */
1451
1452
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_true0)
1453
{
1454
2
  runTestConcat(true, BITVECTOR_ULT, 0);
1455
2
}
1456
1457
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_true1)
1458
{
1459
2
  runTestConcat(true, BITVECTOR_ULT, 1);
1460
2
}
1461
1462
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_true2)
1463
{
1464
2
  runTestConcat(true, BITVECTOR_ULT, 2);
1465
2
}
1466
1467
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_false0)
1468
{
1469
2
  runTestConcat(false, BITVECTOR_ULT, 0);
1470
2
}
1471
1472
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_false1)
1473
{
1474
2
  runTestConcat(false, BITVECTOR_ULT, 1);
1475
2
}
1476
1477
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ult_false2)
1478
{
1479
2
  runTestConcat(false, BITVECTOR_ULT, 2);
1480
2
}
1481
1482
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_true0)
1483
{
1484
2
  runTestConcat(true, BITVECTOR_UGT, 0);
1485
2
}
1486
1487
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_true1)
1488
{
1489
2
  runTestConcat(true, BITVECTOR_UGT, 1);
1490
2
}
1491
1492
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_true2)
1493
{
1494
2
  runTestConcat(true, BITVECTOR_UGT, 2);
1495
2
}
1496
1497
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_false0)
1498
{
1499
2
  runTestConcat(false, BITVECTOR_UGT, 0);
1500
2
}
1501
1502
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_false1)
1503
{
1504
2
  runTestConcat(false, BITVECTOR_UGT, 1);
1505
2
}
1506
1507
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_ugt_false2)
1508
{
1509
2
  runTestConcat(false, BITVECTOR_UGT, 2);
1510
2
}
1511
1512
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_true0)
1513
{
1514
2
  runTestConcat(true, BITVECTOR_SLT, 0);
1515
2
}
1516
1517
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_true1)
1518
{
1519
2
  runTestConcat(true, BITVECTOR_SLT, 1);
1520
2
}
1521
1522
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_true2)
1523
{
1524
2
  runTestConcat(true, BITVECTOR_SLT, 2);
1525
2
}
1526
1527
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_false0)
1528
{
1529
2
  runTestConcat(false, BITVECTOR_SLT, 0);
1530
2
}
1531
1532
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_false1)
1533
{
1534
2
  runTestConcat(false, BITVECTOR_SLT, 1);
1535
2
}
1536
1537
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_slt_false2)
1538
{
1539
2
  runTestConcat(false, BITVECTOR_SLT, 2);
1540
2
}
1541
1542
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_true0)
1543
{
1544
2
  runTestConcat(true, BITVECTOR_SGT, 0);
1545
2
}
1546
1547
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_true1)
1548
{
1549
2
  runTestConcat(true, BITVECTOR_SGT, 1);
1550
2
}
1551
1552
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_true2)
1553
{
1554
2
  runTestConcat(true, BITVECTOR_SGT, 2);
1555
2
}
1556
1557
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_false0)
1558
{
1559
2
  runTestConcat(false, BITVECTOR_SGT, 0);
1560
2
}
1561
1562
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_false1)
1563
{
1564
2
  runTestConcat(false, BITVECTOR_SGT, 1);
1565
2
}
1566
1567
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_concat_sgt_false2)
1568
{
1569
2
  runTestConcat(false, BITVECTOR_SGT, 2);
1570
2
}
1571
1572
/* Sext */
1573
1574
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_ult_true)
1575
{
1576
2
  runTestSext(true, BITVECTOR_ULT);
1577
2
}
1578
1579
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_ult_false)
1580
{
1581
2
  runTestSext(false, BITVECTOR_ULT);
1582
2
}
1583
1584
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_ugt_true)
1585
{
1586
2
  runTestSext(true, BITVECTOR_UGT);
1587
2
}
1588
1589
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_ugt_false)
1590
{
1591
2
  runTestSext(false, BITVECTOR_UGT);
1592
2
}
1593
1594
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_slt_true)
1595
{
1596
2
  runTestSext(true, BITVECTOR_SLT);
1597
2
}
1598
1599
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_slt_false)
1600
{
1601
2
  runTestSext(false, BITVECTOR_SLT);
1602
2
}
1603
1604
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_sgt_true)
1605
{
1606
2
  runTestSext(true, BITVECTOR_SGT);
1607
2
}
1608
1609
265
TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_sgt_false)
1610
{
1611
2
  runTestSext(false, BITVECTOR_SGT);
1612
2
}
1613
}  // namespace test
1614
92351835
}  // namespace CVC4