cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
boolbv_bitreverse.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Michael Tautschnig
6
7
\*******************************************************************/
8
9
#include <
util/bitvector_expr.h
>
10
11
#include "
boolbv.h
"
12
13
#include <algorithm>
14
15
bvt
boolbvt::convert_bitreverse
(
const
bitreverse_exprt
&expr)
16
{
17
const
std::size_t width =
boolbv_width
(expr.
type
());
18
19
bvt
bv =
convert_bv
(expr.
op
(), width);
20
21
std::reverse(bv.begin(), bv.end());
22
23
return
bv;
24
}
bitvector_expr.h
API to expression classes for bitvectors.
boolbv.h
bitreverse_exprt
Reverse the order of bits in a bit-vector.
Definition
bitvector_expr.h:1507
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition
boolbv.cpp:40
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition
boolbv.h:106
boolbvt::convert_bitreverse
virtual bvt convert_bitreverse(const bitreverse_exprt &expr)
Definition
boolbv_bitreverse.cpp:15
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
unary_exprt::op
const exprt & op() const
Definition
std_expr.h:384
bvt
std::vector< literalt > bvt
Definition
literal.h:201
solvers
flattening
boolbv_bitreverse.cpp
Generated by
1.17.0