cprover
boolbv_replication.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#include "
boolbv.h
"
10
11
#include <
util/arith_tools.h
>
12
#include <
util/bitvector_expr.h
>
13
14
bvt
boolbvt::convert_replication
(
const
replication_exprt
&expr)
15
{
16
std::size_t width=
boolbv_width
(expr.
type
());
17
18
if
(width==0)
19
return
conversion_failed
(expr);
20
21
mp_integer
times = numeric_cast_v<mp_integer>(expr.
times
());
22
23
bvt
bv;
24
bv.resize(width);
25
26
const
std::size_t u_times = numeric_cast_v<std::size_t>(times);
27
const
bvt
&op =
convert_bv
(expr.
op
());
28
29
INVARIANT
(
30
op.size() * u_times == bv.size(),
31
"result bitvector width shall be equal to the operand bitvector width times"
32
"the number of replications"
);
33
34
std::size_t bit_idx = 0;
35
36
for
(std::size_t i = 0; i < u_times; i++)
37
{
38
for
(
const
auto
&bit : op)
39
{
40
bv[bit_idx] = bit;
41
bit_idx++;
42
}
43
}
44
45
return
bv;
46
}
arith_tools.h
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
mp_integer
BigInt mp_integer
Definition:
mp_arith.h:19
replication_exprt::times
constant_exprt & times()
Definition:
bitvector_expr.h:529
replication_exprt
Bit-vector replication.
Definition:
bitvector_expr.h:518
replication_exprt::op
exprt & op()
Definition:
bitvector_expr.h:539
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:82
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:126
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition:
boolbv.h:96
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition:
boolbv.cpp:47
boolbvt::convert_replication
virtual bvt convert_replication(const replication_exprt &expr)
Definition:
boolbv_replication.cpp:14
boolbv.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition:
invariant.h:424
bitvector_expr.h
API to expression classes for bitvectors.
solvers
flattening
boolbv_replication.cpp
Generated by
1.8.20