GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_utils.cpp Lines: 217 237 91.6 %
Date: 2021-03-22 Branches: 341 812 42.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Liana Hadarean
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 Util functions for theory BV.
13
 **
14
 ** Util functions for theory BV.
15
 **/
16
17
#include "theory/bv/theory_bv_utils.h"
18
19
#include <vector>
20
21
#include "options/theory_options.h"
22
#include "theory/theory.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace bv {
27
namespace utils {
28
29
/* ------------------------------------------------------------------------- */
30
31
4214601
unsigned getSize(TNode node)
32
{
33
4214601
  return node.getType().getBitVectorSize();
34
}
35
36
43
const bool getBit(TNode node, unsigned i)
37
{
38
43
  Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
39
43
  return node.getConst<BitVector>().extract(i, i).getValue() == 1u;
40
}
41
42
/* ------------------------------------------------------------------------- */
43
44
533508
unsigned getExtractHigh(TNode node)
45
{
46
533508
  return node.getOperator().getConst<BitVectorExtract>().d_high;
47
}
48
49
506406
unsigned getExtractLow(TNode node)
50
{
51
506406
  return node.getOperator().getConst<BitVectorExtract>().d_low;
52
}
53
54
68
unsigned getSignExtendAmount(TNode node)
55
{
56
68
  return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
57
}
58
59
/* ------------------------------------------------------------------------- */
60
61
3244
bool isOnes(TNode node)
62
{
63
3244
  if (!node.isConst()) return false;
64
77
  return node == mkOnes(getSize(node));
65
}
66
67
14071
bool isZero(TNode node)
68
{
69
14071
  if (!node.isConst()) return false;
70
10874
  return node == mkZero(getSize(node));
71
}
72
73
3813
bool isOne(TNode node)
74
{
75
3813
  if (!node.isConst()) return false;
76
646
  return node == mkOne(getSize(node));
77
}
78
79
822736
unsigned isPow2Const(TNode node, bool& isNeg)
80
{
81
822736
  if (node.getKind() != kind::CONST_BITVECTOR)
82
  {
83
545106
    return false;
84
  }
85
86
555260
  BitVector bv = node.getConst<BitVector>();
87
277630
  unsigned p = bv.isPow2();
88
277630
  if (p != 0)
89
  {
90
38571
    isNeg = false;
91
38571
    return p;
92
  }
93
478118
  BitVector nbv = -bv;
94
239059
  p = nbv.isPow2();
95
239059
  if (p != 0)
96
  {
97
7361
    isNeg = true;
98
7361
    return p;
99
  }
100
231698
  return false;
101
}
102
103
969633
bool isBvConstTerm(TNode node)
104
{
105
969633
  if (node.getNumChildren() == 0)
106
  {
107
    return node.isConst();
108
  }
109
110
1755388
  for (const TNode& n : node)
111
  {
112
1356508
    if (!n.isConst()) { return false; }
113
  }
114
398880
  return true;
115
}
116
117
14
bool isBVPredicate(TNode node)
118
{
119
14
  Kind k = node.getKind();
120
14
  if (k == kind::NOT)
121
  {
122
    node = node[0];
123
    k = node.getKind();
124
  }
125
  return k == kind::EQUAL
126
2
         || k == kind::BITVECTOR_ULT
127
2
         || k == kind::BITVECTOR_SLT
128
2
         || k == kind::BITVECTOR_UGT
129
2
         || k == kind::BITVECTOR_UGE
130
2
         || k == kind::BITVECTOR_SGT
131
2
         || k == kind::BITVECTOR_SGE
132
2
         || k == kind::BITVECTOR_ULE
133
2
         || k == kind::BITVECTOR_SLE
134
2
         || k == kind::BITVECTOR_REDOR
135
16
         || k == kind::BITVECTOR_REDAND;
136
}
137
138
45882
static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
139
{
140
91764
  TNode t = term.getKind() == kind::NOT ? term[0] : term;
141
142
91764
  std::vector<TNode> stack;
143
91764
  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
144
45882
  stack.push_back(t);
145
146
539708
  while (!stack.empty())
147
  {
148
380003
    TNode n = stack.back();
149
246913
    stack.pop_back();
150
151
246913
    if (cache.find(n) != cache.end()) continue;
152
153
240465
    if (n.getNumChildren() == 0)
154
    {
155
52296
      cache[n] = true;
156
52296
      visited[n] = true;
157
52296
      continue;
158
    }
159
160
271746
    if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
161
135873
        == theory::THEORY_BV)
162
    {
163
49843
      Kind k = n.getKind();
164
49843
      Assert(k != kind::CONST_BITVECTOR);
165
52626
      if (k != kind::EQUAL
166
2783
          && (iseq || k != kind::BITVECTOR_CONCAT)
167
2783
          && (iseq || k != kind::BITVECTOR_EXTRACT)
168
52626
          && n.getMetaKind() != kind::metakind::VARIABLE)
169
      {
170
2783
        cache[n] = false;
171
2783
        continue;
172
      }
173
    }
174
175
133090
    if (!visited[n])
176
    {
177
66545
      visited[n] = true;
178
66545
      stack.push_back(n);
179
66545
      stack.insert(stack.end(), n.begin(), n.end());
180
    }
181
    else
182
    {
183
66545
      bool iseqt = true;
184
198320
      for (const Node& c : n)
185
      {
186
133134
        Assert(cache.find(c) != cache.end());
187
133134
        if (!cache[c])
188
        {
189
1359
          iseqt = false;
190
1359
          break;
191
        }
192
      }
193
66545
      cache[n] = iseqt;
194
    }
195
  }
196
45882
  Assert(cache.find(t) != cache.end());
197
91764
  return cache[t];
198
}
199
200
bool isCoreTerm(TNode term, TNodeBoolMap& cache)
201
{
202
  return isCoreEqTerm(false, term, cache);
203
}
204
205
45882
bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
206
{
207
45882
  return isCoreEqTerm(true, term, cache);
208
}
209
210
1729336
bool isBitblastAtom(Node lit)
211
{
212
3458672
  TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit;
213
3458672
  return atom.getKind() != kind::EQUAL || atom[0].getType().isBitVector();
214
}
215
216
/* ------------------------------------------------------------------------- */
217
218
38549
Node mkTrue()
219
{
220
38549
  return NodeManager::currentNM()->mkConst<bool>(true);
221
}
222
223
106315
Node mkFalse()
224
{
225
106315
  return NodeManager::currentNM()->mkConst<bool>(false);
226
}
227
228
224291
Node mkZero(unsigned size)
229
{
230
224291
  Assert(size > 0);
231
224291
  return mkConst(size, 0u);
232
}
233
234
13770
Node mkOne(unsigned size)
235
{
236
13770
  Assert(size > 0);
237
13770
  return mkConst(size, 1u);
238
}
239
240
23972
Node mkOnes(unsigned size)
241
{
242
23972
  Assert(size > 0);
243
23972
  return mkConst(BitVector::mkOnes(size));
244
}
245
246
54
Node mkMinSigned(unsigned size)
247
{
248
54
  Assert(size > 0);
249
54
  return mkConst(BitVector::mkMinSigned(size));
250
}
251
252
64
Node mkMaxSigned(unsigned size)
253
{
254
64
  Assert(size > 0);
255
64
  return mkConst(BitVector::mkMaxSigned(size));
256
}
257
258
/* ------------------------------------------------------------------------- */
259
260
636751
Node mkConst(unsigned size, unsigned int value)
261
{
262
1273502
  BitVector val(size, value);
263
1273502
  return NodeManager::currentNM()->mkConst<BitVector>(val);
264
}
265
266
59867
Node mkConst(unsigned size, Integer& value)
267
{
268
59867
  return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
269
}
270
271
1096135
Node mkConst(const BitVector& value)
272
{
273
1096135
  return NodeManager::currentNM()->mkConst<BitVector>(value);
274
}
275
276
/* ------------------------------------------------------------------------- */
277
278
94
Node mkVar(unsigned size)
279
{
280
94
  NodeManager* nm = NodeManager::currentNM();
281
282
  return nm->mkSkolem("BVSKOLEM$$",
283
188
                      nm->mkBitVectorType(size),
284
282
                      "is a variable created by the theory of bitvectors");
285
}
286
287
/* ------------------------------------------------------------------------- */
288
289
Node mkSortedNode(Kind kind, TNode child1, TNode child2)
290
{
291
  Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
292
         || kind == kind::BITVECTOR_XOR);
293
294
  if (child1 < child2)
295
  {
296
    return NodeManager::currentNM()->mkNode(kind, child1, child2);
297
  }
298
  else
299
  {
300
    return NodeManager::currentNM()->mkNode(kind, child2, child1);
301
  }
302
}
303
304
323866
Node mkSortedNode(Kind kind, std::vector<Node>& children)
305
{
306
323866
  Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
307
         || kind == kind::BITVECTOR_XOR);
308
323866
  Assert(children.size() > 0);
309
323866
  if (children.size() == 1)
310
  {
311
75105
    return children[0];
312
  }
313
248761
  std::sort(children.begin(), children.end());
314
248761
  return NodeManager::currentNM()->mkNode(kind, children);
315
}
316
317
/* ------------------------------------------------------------------------- */
318
319
Node mkNot(Node child)
320
{
321
  return NodeManager::currentNM()->mkNode(kind::NOT, child);
322
}
323
324
Node mkAnd(TNode node1, TNode node2)
325
{
326
  return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
327
}
328
329
Node mkOr(TNode node1, TNode node2)
330
{
331
  return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
332
}
333
334
Node mkXor(TNode node1, TNode node2)
335
{
336
  return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
337
}
338
339
/* ------------------------------------------------------------------------- */
340
341
351
Node mkSignExtend(TNode node, unsigned amount)
342
{
343
351
  NodeManager* nm = NodeManager::currentNM();
344
  Node signExtendOp =
345
702
      nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount));
346
702
  return nm->mkNode(signExtendOp, node);
347
}
348
349
/* ------------------------------------------------------------------------- */
350
351
57086
Node mkExtract(TNode node, unsigned high, unsigned low)
352
{
353
57086
  NodeManager *nm = NodeManager::currentNM();
354
114172
  Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
355
114172
  return nm->mkNode(extractOp, node);
356
}
357
358
184013
Node mkBitOf(TNode node, unsigned index)
359
{
360
184013
  NodeManager *nm = NodeManager::currentNM();
361
368026
  Node bitOfOp = nm->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
362
368026
  return nm->mkNode(bitOfOp, node);
363
}
364
365
/* ------------------------------------------------------------------------- */
366
367
29249
Node mkConcat(TNode t1, TNode t2)
368
{
369
29249
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
370
}
371
372
613763
Node mkConcat(std::vector<Node>& children)
373
{
374
613763
  if (children.size() > 1)
375
533378
    return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
376
  else
377
80385
    return children[0];
378
}
379
380
583
Node mkConcat(TNode node, unsigned repeat)
381
{
382
583
  Assert(repeat);
383
583
  if (repeat == 1)
384
  {
385
90
    return node;
386
  }
387
986
  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
388
5535
  for (unsigned i = 0; i < repeat; ++i)
389
  {
390
5042
    result << node;
391
  }
392
986
  Node resultNode = result;
393
493
  return resultNode;
394
}
395
396
/* ------------------------------------------------------------------------- */
397
398
Node mkInc(TNode t)
399
{
400
  return NodeManager::currentNM()->mkNode(
401
      kind::BITVECTOR_PLUS, t, mkOne(getSize(t)));
402
}
403
404
2
Node mkDec(TNode t)
405
{
406
  return NodeManager::currentNM()->mkNode(
407
2
      kind::BITVECTOR_SUB, t, mkOne(getSize(t)));
408
}
409
410
/* ------------------------------------------------------------------------- */
411
412
30
Node mkUmulo(TNode t1, TNode t2)
413
{
414
30
  unsigned w = getSize(t1);
415
30
  if (w == 1) return mkFalse();
416
417
28
  NodeManager* nm = NodeManager::currentNM();
418
56
  Node uppc;
419
56
  std::vector<Node> tmp;
420
421
28
  uppc = mkExtract(t1, w - 1, w - 1);
422
238
  for (size_t i = 1; i < w; ++i)
423
  {
424
210
    tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
425
630
    uppc = nm->mkNode(
426
420
        kind::BITVECTOR_OR, mkExtract(t1, w - 1 - i, w - 1 - i), uppc);
427
  }
428
56
  Node zext_t1 = mkConcat(mkZero(1), t1);
429
56
  Node zext_t2 = mkConcat(mkZero(1), t2);
430
56
  Node mul = nm->mkNode(kind::BITVECTOR_MULT, zext_t1, zext_t2);
431
28
  tmp.push_back(mkExtract(mul, w, w));
432
28
  return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1));
433
}
434
435
/* ------------------------------------------------------------------------- */
436
437
715
Node flattenAnd(std::vector<TNode>& queue)
438
{
439
1430
  TNodeSet nodes;
440
4687
  while (!queue.empty())
441
  {
442
3972
    TNode current = queue.back();
443
1986
    queue.pop_back();
444
1986
    if (current.getKind() == kind::AND)
445
    {
446
16
      for (const TNode& n : current)
447
      {
448
11
        if (nodes.count(n) == 0) { queue.push_back(n); }
449
      }
450
    }
451
    else
452
    {
453
1981
      nodes.insert(current);
454
    }
455
  }
456
1430
  std::vector<TNode> children(nodes.begin(), nodes.end());
457
1430
  return mkAnd(children);
458
}
459
460
/* ------------------------------------------------------------------------- */
461
462
249
Node eliminateBv2Nat(TNode node)
463
{
464
249
  const unsigned size = utils::getSize(node[0]);
465
249
  NodeManager* const nm = NodeManager::currentNM();
466
498
  const Node z = nm->mkConst(Rational(0));
467
498
  const Node bvone = utils::mkOne(1);
468
469
498
  Integer i = 1;
470
498
  std::vector<Node> children;
471
1395
  for (unsigned bit = 0; bit < size; ++bit, i *= 2)
472
  {
473
    Node cond =
474
        nm->mkNode(kind::EQUAL,
475
2292
                   nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
476
4584
                   bvone);
477
1146
    children.push_back(
478
2292
        nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
479
  }
480
  // avoid plus with one child
481
498
  return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
482
}
483
484
307
Node eliminateInt2Bv(TNode node)
485
{
486
307
  const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
487
307
  NodeManager* const nm = NodeManager::currentNM();
488
614
  const Node bvzero = utils::mkZero(1);
489
614
  const Node bvone = utils::mkOne(1);
490
491
614
  std::vector<Node> v;
492
614
  Integer i = 2;
493
3203
  while (v.size() < size)
494
  {
495
    Node cond = nm->mkNode(
496
        kind::GEQ,
497
2896
        nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
498
5792
        nm->mkConst(Rational(i, 2)));
499
1448
    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
500
1448
    i *= 2;
501
  }
502
307
  if (v.size() == 1)
503
  {
504
5
    return v[0];
505
  }
506
604
  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
507
302
  result.append(v.rbegin(), v.rend());
508
302
  return Node(result);
509
}
510
511
}/* CVC4::theory::bv::utils namespace */
512
}/* CVC4::theory::bv namespace */
513
}/* CVC4::theory namespace */
514
26676
}/* CVC4 namespace */