GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/slicer.cpp Lines: 1 32 3.1 %
Date: 2021-03-23 Branches: 2 64 3.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file slicer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz
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.
13
 **
14
 ** Bitvector theory.
15
 **/
16
#include "theory/bv/slicer.h"
17
18
#include <sstream>
19
20
#include "theory/bv/theory_bv_utils.h"
21
#include "theory/rewriter.h"
22
23
using namespace std;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bv {
28
29
/**
30
 * Base
31
 *
32
 */
33
Base::Base(uint32_t size)
34
  : d_size(size),
35
    d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
36
{
37
  Assert(d_size > 0);
38
}
39
40
void Base::sliceAt(Index index)
41
{
42
  Index vector_index = index / 32;
43
  if (vector_index == d_repr.size())
44
    return;
45
46
  Index int_index = index % 32;
47
  uint32_t bit_mask = 1u << int_index;
48
  d_repr[vector_index] = d_repr[vector_index] | bit_mask;
49
}
50
51
bool Base::isCutPoint (Index index) const
52
{
53
  // there is an implicit cut point at the end and begining of the bv
54
  if (index == d_size || index == 0)
55
    return true;
56
57
  Index vector_index = index / 32;
58
  Assert(vector_index < d_size);
59
  Index int_index = index % 32;
60
  uint32_t bit_mask = 1u << int_index;
61
62
  return (bit_mask & d_repr[vector_index]) != 0;
63
}
64
65
std::string Base::debugPrint() const {
66
  std::ostringstream os;
67
  os << "[";
68
  bool first = true;
69
  for (int i = d_size - 1; i >= 0; --i) {
70
    if (isCutPoint(i)) {
71
      if (first)
72
        first = false;
73
      else
74
        os <<"| ";
75
76
      os << i ;
77
    }
78
  }
79
  os << "]";
80
  return os.str();
81
}
82
83
84
}  // namespace bv
85
}  // namespace theory
86
26685
}  // namespace CVC4