GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_type_rules.h Lines: 101 142 71.1 %
Date: 2021-03-22 Branches: 145 476 30.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Dejan Jovanovic
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 Bitvector theory typing rules
13
 **
14
 ** Bitvector theory typing rules.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#include <algorithm>
20
21
#ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
22
#define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
23
24
namespace CVC4 {
25
namespace theory {
26
namespace bv {
27
28
/* -------------------------------------------------------------------------- */
29
30
class CardinalityComputer
31
{
32
 public:
33
2463
  inline static Cardinality computeCardinality(TypeNode type)
34
  {
35
2463
    Assert(type.getKind() == kind::BITVECTOR_TYPE);
36
37
2463
    unsigned size = type.getConst<BitVectorSize>();
38
2463
    if (size == 0)
39
    {
40
2
      return 0;
41
    }
42
4922
    Integer i = Integer(2).pow(size);
43
2461
    return i;
44
  }
45
}; /* class CardinalityComputer */
46
47
/* -------------------------------------------------------------------------- */
48
49
class BitVectorConstantTypeRule
50
{
51
 public:
52
81523
  inline static TypeNode computeType(NodeManager* nodeManager,
53
                                     TNode n,
54
                                     bool check)
55
  {
56
81523
    if (check)
57
    {
58
66451
      if (n.getConst<BitVector>().getSize() == 0)
59
      {
60
        throw TypeCheckingExceptionPrivate(n, "constant of size 0");
61
      }
62
    }
63
81523
    return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
64
  }
65
}; /* class BitVectorConstantTypeRule */
66
67
/* -------------------------------------------------------------------------- */
68
69
class BitVectorFixedWidthTypeRule
70
{
71
 public:
72
935174
  inline static TypeNode computeType(NodeManager* nodeManager,
73
                                     TNode n,
74
                                     bool check)
75
  {
76
935174
    TNode::iterator it = n.begin();
77
935174
    TypeNode t = (*it).getType(check);
78
935174
    if (check)
79
    {
80
935174
      if (!t.isBitVector())
81
      {
82
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
83
      }
84
935174
      TNode::iterator it_end = n.end();
85
2354289
      for (++it; it != it_end; ++it)
86
      {
87
1419115
        if ((*it).getType(check) != t)
88
        {
89
          throw TypeCheckingExceptionPrivate(
90
              n, "expecting bit-vector terms of the same width");
91
        }
92
      }
93
    }
94
935174
    return t;
95
  }
96
}; /* class BitVectorFixedWidthTypeRule */
97
98
/* -------------------------------------------------------------------------- */
99
100
class BitVectorPredicateTypeRule
101
{
102
 public:
103
96521
  inline static TypeNode computeType(NodeManager* nodeManager,
104
                                     TNode n,
105
                                     bool check)
106
  {
107
96521
    if (check)
108
    {
109
193042
      TypeNode lhsType = n[0].getType(check);
110
96521
      if (!lhsType.isBitVector())
111
      {
112
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
113
      }
114
193042
      TypeNode rhsType = n[1].getType(check);
115
96521
      if (lhsType != rhsType)
116
      {
117
        throw TypeCheckingExceptionPrivate(
118
            n, "expecting bit-vector terms of the same width");
119
      }
120
    }
121
96521
    return nodeManager->booleanType();
122
  }
123
}; /* class BitVectorPredicateTypeRule */
124
125
class BitVectorUnaryPredicateTypeRule
126
{
127
 public:
128
  inline static TypeNode computeType(NodeManager* nodeManager,
129
                                     TNode n,
130
                                     bool check)
131
  {
132
    if (check)
133
    {
134
      TypeNode type = n[0].getType(check);
135
      if (!type.isBitVector())
136
      {
137
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
138
      }
139
    }
140
    return nodeManager->booleanType();
141
  }
142
}; /* class BitVectorUnaryPredicateTypeRule */
143
144
class BitVectorBVPredTypeRule
145
{
146
 public:
147
157679
  inline static TypeNode computeType(NodeManager* nodeManager,
148
                                     TNode n,
149
                                     bool check)
150
  {
151
157679
    if (check)
152
    {
153
315358
      TypeNode lhs = n[0].getType(check);
154
315358
      TypeNode rhs = n[1].getType(check);
155
157679
      if (!lhs.isBitVector() || lhs != rhs)
156
      {
157
        throw TypeCheckingExceptionPrivate(
158
            n, "expecting bit-vector terms of the same width");
159
      }
160
    }
161
157679
    return nodeManager->mkBitVectorType(1);
162
  }
163
}; /* class BitVectorBVPredTypeRule */
164
165
/* -------------------------------------------------------------------------- */
166
/* non-parameterized operator kinds                                           */
167
/* -------------------------------------------------------------------------- */
168
169
class BitVectorConcatTypeRule
170
{
171
 public:
172
112033
  inline static TypeNode computeType(NodeManager* nodeManager,
173
                                     TNode n,
174
                                     bool check)
175
  {
176
112033
    unsigned size = 0;
177
112033
    TNode::iterator it = n.begin();
178
112033
    TNode::iterator it_end = n.end();
179
705061
    for (; it != it_end; ++it)
180
    {
181
593028
      TypeNode t = (*it).getType(check);
182
      // NOTE: We're throwing a type-checking exception here even
183
      // when check is false, bc if we don't check that the arguments
184
      // are bit-vectors the result type will be inaccurate
185
296514
      if (!t.isBitVector())
186
      {
187
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
188
      }
189
296514
      size += t.getBitVectorSize();
190
    }
191
112033
    return nodeManager->mkBitVectorType(size);
192
  }
193
}; /* class BitVectorConcatTypeRule */
194
195
class BitVectorITETypeRule
196
{
197
 public:
198
10125
  inline static TypeNode computeType(NodeManager* nodeManager,
199
                                     TNode n,
200
                                     bool check)
201
  {
202
10125
    Assert(n.getNumChildren() == 3);
203
10125
    TypeNode thenpart = n[1].getType(check);
204
10125
    if (check)
205
    {
206
20250
      TypeNode cond = n[0].getType(check);
207
10125
      if (cond != nodeManager->mkBitVectorType(1))
208
      {
209
        throw TypeCheckingExceptionPrivate(
210
            n, "expecting condition to be bit-vector term size 1");
211
      }
212
20250
      TypeNode elsepart = n[2].getType(check);
213
10125
      if (thenpart != elsepart)
214
      {
215
        throw TypeCheckingExceptionPrivate(
216
            n, "expecting then and else parts to have same type");
217
      }
218
    }
219
10125
    return thenpart;
220
  }
221
}; /* class BitVectorITETypeRule */
222
223
/* -------------------------------------------------------------------------- */
224
/* parameterized operator kinds                                               */
225
/* -------------------------------------------------------------------------- */
226
227
class BitVectorBitOfTypeRule
228
{
229
 public:
230
167018
  inline static TypeNode computeType(NodeManager* nodeManager,
231
                                     TNode n,
232
                                     bool check)
233
  {
234
167018
    if (check)
235
    {
236
167018
      BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
237
334036
      TypeNode t = n[0].getType(check);
238
239
167018
      if (!t.isBitVector())
240
      {
241
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
242
      }
243
167018
      if (info.d_bitIndex >= t.getBitVectorSize())
244
      {
245
        throw TypeCheckingExceptionPrivate(
246
            n, "extract index is larger than the bitvector size");
247
      }
248
    }
249
167018
    return nodeManager->booleanType();
250
  }
251
}; /* class BitVectorBitOfTypeRule */
252
253
class BitVectorExtractTypeRule
254
{
255
 public:
256
124012
  inline static TypeNode computeType(NodeManager* nodeManager,
257
                                     TNode n,
258
                                     bool check)
259
  {
260
124012
    BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
261
262
    // NOTE: We're throwing a type-checking exception here even
263
    // if check is false, bc if we allow high < low the resulting
264
    // type will be illegal
265
124012
    if (extractInfo.d_high < extractInfo.d_low)
266
    {
267
      throw TypeCheckingExceptionPrivate(
268
          n, "high extract index is smaller than the low extract index");
269
    }
270
271
124012
    if (check)
272
    {
273
248024
      TypeNode t = n[0].getType(check);
274
124012
      if (!t.isBitVector())
275
      {
276
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
277
      }
278
124012
      if (extractInfo.d_high >= t.getBitVectorSize())
279
      {
280
        throw TypeCheckingExceptionPrivate(
281
            n, "high extract index is bigger than the size of the bit-vector");
282
      }
283
    }
284
124012
    return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
285
124012
                                        + 1);
286
  }
287
}; /* class BitVectorExtractTypeRule */
288
289
class BitVectorRepeatTypeRule
290
{
291
 public:
292
419
  inline static TypeNode computeType(NodeManager* nodeManager,
293
                                     TNode n,
294
                                     bool check)
295
  {
296
838
    TypeNode t = n[0].getType(check);
297
    // NOTE: We're throwing a type-checking exception here even
298
    // when check is false, bc if the argument isn't a bit-vector
299
    // the result type will be inaccurate
300
419
    if (!t.isBitVector())
301
    {
302
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
303
    }
304
419
    unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
305
419
    if (repeatAmount == 0)
306
    {
307
1
      throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
308
    }
309
836
    return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
310
  }
311
}; /* class BitVectorRepeatTypeRule */
312
313
class BitVectorExtendTypeRule
314
{
315
 public:
316
31442
  inline static TypeNode computeType(NodeManager* nodeManager,
317
                                     TNode n,
318
                                     bool check)
319
  {
320
62884
    TypeNode t = n[0].getType(check);
321
    // NOTE: We're throwing a type-checking exception here even
322
    // when check is false, bc if the argument isn't a bit-vector
323
    // the result type will be inaccurate
324
31442
    if (!t.isBitVector())
325
    {
326
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
327
    }
328
    unsigned extendAmount =
329
31442
        n.getKind() == kind::BITVECTOR_SIGN_EXTEND
330
82094
            ? (unsigned)n.getOperator().getConst<BitVectorSignExtend>()
331
50652
            : (unsigned)n.getOperator().getConst<BitVectorZeroExtend>();
332
62884
    return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
333
  }
334
}; /* class BitVectorExtendTypeRule */
335
336
class IntToBitVectorOpTypeRule
337
{
338
 public:
339
17
  inline static TypeNode computeType(NodeManager* nodeManager,
340
                                     TNode n,
341
                                     bool check)
342
  {
343
17
    if (n.getKind() == kind::INT_TO_BITVECTOR_OP)
344
    {
345
17
      size_t bvSize = n.getConst<IntToBitVector>();
346
17
      if (bvSize == 0)
347
      {
348
1
        throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
349
      }
350
32
      return nodeManager->mkFunctionType(nodeManager->integerType(),
351
64
                                         nodeManager->mkBitVectorType(bvSize));
352
    }
353
354
    InternalError()
355
        << "bv-conversion typerule invoked for non-bv-conversion kind";
356
  }
357
}; /* class IntToBitVectorOpTypeRule */
358
359
class BitVectorConversionTypeRule
360
{
361
 public:
362
995
  inline static TypeNode computeType(NodeManager* nodeManager,
363
                                     TNode n,
364
                                     bool check)
365
  {
366
995
    if (n.getKind() == kind::BITVECTOR_TO_NAT)
367
    {
368
465
      if (check && !n[0].getType(check).isBitVector())
369
      {
370
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
371
      }
372
465
      return nodeManager->integerType();
373
    }
374
375
530
    if (n.getKind() == kind::INT_TO_BITVECTOR)
376
    {
377
530
      size_t bvSize = n.getOperator().getConst<IntToBitVector>();
378
530
      if (check && !n[0].getType(check).isInteger())
379
      {
380
        throw TypeCheckingExceptionPrivate(n, "expecting integer term");
381
      }
382
530
      return nodeManager->mkBitVectorType(bvSize);
383
    }
384
385
    InternalError()
386
        << "bv-conversion typerule invoked for non-bv-conversion kind";
387
  }
388
}; /* class BitVectorConversionTypeRule */
389
390
/* -------------------------------------------------------------------------- */
391
/* internal                                                                   */
392
/* -------------------------------------------------------------------------- */
393
394
class BitVectorEagerAtomTypeRule
395
{
396
 public:
397
237
  inline static TypeNode computeType(NodeManager* nodeManager,
398
                                     TNode n,
399
                                     bool check)
400
  {
401
237
    if (check)
402
    {
403
474
      TypeNode lhsType = n[0].getType(check);
404
237
      if (!lhsType.isBoolean())
405
      {
406
        throw TypeCheckingExceptionPrivate(n, "expecting boolean term");
407
      }
408
    }
409
237
    return nodeManager->booleanType();
410
  }
411
}; /* class BitVectorEagerAtomTypeRule */
412
413
class BitVectorAckermanizationUdivTypeRule
414
{
415
 public:
416
  inline static TypeNode computeType(NodeManager* nodeManager,
417
                                     TNode n,
418
                                     bool check)
419
  {
420
    TypeNode lhsType = n[0].getType(check);
421
    if (check)
422
    {
423
      if (!lhsType.isBitVector())
424
      {
425
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
426
      }
427
    }
428
    return lhsType;
429
  }
430
}; /* class BitVectorAckermanizationUdivTypeRule */
431
432
class BitVectorAckermanizationUremTypeRule
433
{
434
 public:
435
  inline static TypeNode computeType(NodeManager* nodeManager,
436
                                     TNode n,
437
                                     bool check)
438
  {
439
    TypeNode lhsType = n[0].getType(check);
440
    if (check)
441
    {
442
      if (!lhsType.isBitVector())
443
      {
444
        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
445
      }
446
    }
447
    return lhsType;
448
  }
449
}; /* class BitVectorAckermanizationUremTypeRule */
450
451
}  // namespace bv
452
}  // namespace theory
453
}  // namespace CVC4
454
455
#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */