blob: 75357b76c9cb15f593298e2169cdeebaf98b4244 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
/********************* */
/*! \file slicer.cpp
** \verbatim
** Top contributors (to current version):
** Liana Hadarean, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Bitvector theory.
**
** Bitvector theory.
**/
#include "theory/bv/slicer.h"
#include <sstream>
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
using namespace std;
namespace cvc5 {
namespace theory {
namespace bv {
/**
* Base
*
*/
Base::Base(uint32_t size)
: d_size(size),
d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
{
Assert(d_size > 0);
}
void Base::sliceAt(Index index)
{
Index vector_index = index / 32;
if (vector_index == d_repr.size())
return;
Index int_index = index % 32;
uint32_t bit_mask = 1u << int_index;
d_repr[vector_index] = d_repr[vector_index] | bit_mask;
}
bool Base::isCutPoint (Index index) const
{
// there is an implicit cut point at the end and begining of the bv
if (index == d_size || index == 0)
return true;
Index vector_index = index / 32;
Assert(vector_index < d_size);
Index int_index = index % 32;
uint32_t bit_mask = 1u << int_index;
return (bit_mask & d_repr[vector_index]) != 0;
}
std::string Base::debugPrint() const {
std::ostringstream os;
os << "[";
bool first = true;
for (int i = d_size - 1; i >= 0; --i) {
if (isCutPoint(i)) {
if (first)
first = false;
else
os <<"| ";
os << i ;
}
}
os << "]";
return os.str();
}
} // namespace bv
} // namespace theory
} // namespace cvc5
|
