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
13
bvt
boolbvt::convert_replication
(
const
replication_exprt
&expr)
14
{
15
std::size_t width=
boolbv_width
(expr.
type
());
16
17
if
(width==0)
18
return
conversion_failed
(expr);
19
20
mp_integer
times = numeric_cast_v<mp_integer>(expr.
times
());
21
22
bvt
bv;
23
bv.resize(width);
24
25
const
std::size_t u_times = numeric_cast_v<std::size_t>(times);
26
const
bvt
&op =
convert_bv
(expr.
op
());
27
28
INVARIANT
(
29
op.size() * u_times == bv.size(),
30
"result bitvector width shall be equal to the operand bitvector width times"
31
"the number of replications"
);
32
33
std::size_t bit_idx = 0;
34
35
for
(std::size_t i = 0; i < u_times; i++)
36
{
37
for
(
const
auto
&bit : op)
38
{
39
bv[bit_idx] = bit;
40
bit_idx++;
41
}
42
}
43
44
return
bv;
45
}
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:
std_expr.h:4006
replication_exprt
Bit-vector replication.
Definition:
std_expr.h:3999
replication_exprt::op
exprt & op()
Definition:
std_expr.h:4016
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition:
boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:113
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:119
boolbvt::convert_replication
virtual bvt convert_replication(const replication_exprt &expr)
Definition:
boolbv_replication.cpp:13
boolbv.h
validation_modet::INVARIANT
@ INVARIANT
solvers
flattening
boolbv_replication.cpp
Generated by
1.8.20