cprover
boolbv_vector.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#include "
boolbv.h
"
11
12
bvt
boolbvt::convert_vector
(
const
vector_exprt
&expr)
13
{
14
std::size_t width=
boolbv_width
(expr.
type
());
15
16
if
(width==0)
17
return
conversion_failed
(expr);
18
19
const
exprt::operandst
&operands = expr.
operands
();
20
21
bvt
bv;
22
bv.reserve(width);
23
24
if
(!operands.empty())
25
{
26
std::size_t op_width = width / operands.size();
27
28
for
(
const
auto
&op : operands)
29
{
30
const
bvt
&tmp =
convert_bv
(op, op_width);
31
32
bv.insert(bv.end(), tmp.begin(), tmp.end());
33
}
34
}
35
36
return
bv;
37
}
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
boolbvt::convert_vector
virtual bvt convert_vector(const vector_exprt &expr)
Definition:
boolbv_vector.cpp:12
vector_exprt
Vector constructor from list of elements.
Definition:
std_expr.h:1480
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
exprt::operandst
std::vector< exprt > operandst
Definition:
expr.h:56
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
boolbv.h
exprt::operands
operandst & operands()
Definition:
expr.h:96
solvers
flattening
boolbv_vector.cpp
Generated by
1.8.20