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
forall_expr
(it, operands)
29
{
30
const
bvt
&tmp =
convert_bv
(*it, op_width);
31
32
forall_literals
(it2, tmp)
33
bv.push_back(*it2);
34
}
35
}
36
37
return
bv;
38
}
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:1531
forall_literals
#define forall_literals(it, bv)
Definition:
literal.h:203
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
exprt::operandst
std::vector< exprt > operandst
Definition:
expr.h:55
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
boolbv.h
exprt::operands
operandst & operands()
Definition:
expr.h:95
forall_expr
#define forall_expr(it, expr)
Definition:
expr.h:29
solvers
flattening
boolbv_vector.cpp
Generated by
1.8.20