GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/type_enumerator.h Lines: 13 13 100.0 %
Date: 2021-03-22 Branches: 11 20 55.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Mathias Preiner, Tim King
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 An enumerator for bitvectors
13
 **
14
 ** An enumerator for bitvectors.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__BV__TYPE_ENUMERATOR_H
21
22
#include "expr/kind.h"
23
#include "expr/type_node.h"
24
#include "theory/type_enumerator.h"
25
#include "theory/bv/theory_bv_utils.h"
26
#include "util/bitvector.h"
27
#include "util/integer.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace bv {
32
33
19270
class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
34
  size_t d_size;
35
  Integer d_bits;
36
37
public:
38
39
8036
  BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
40
    TypeEnumeratorBase<BitVectorEnumerator>(type),
41
8036
    d_size(type.getBitVectorSize()),
42
16072
    d_bits(0) {
43
8036
  }
44
45
39070
  Node operator*() override
46
  {
47
39070
    if(d_bits != d_bits.modByPow2(d_size)) {
48
1003
      throw NoMoreValuesException(getType());
49
    }
50
38067
    return utils::mkConst(d_size, d_bits);
51
  }
52
53
10143
  BitVectorEnumerator& operator++() override
54
  {
55
10143
    d_bits += 1;
56
10143
    return *this;
57
  }
58
59
49440
  bool isFinished() override { return d_bits != d_bits.modByPow2(d_size); }
60
};/* BitVectorEnumerator */
61
62
}/* CVC4::theory::bv namespace */
63
}/* CVC4::theory namespace */
64
}/* CVC4 namespace */
65
66
#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */