CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
boolbv_bitreverse.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#include <util/bitvector_expr.h>
10
11#include "boolbv.h"
12
13#include <algorithm>
14
15bvt 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.
bitreverse_exprt
Reverse the order of bits in a bit-vector.
Definition bitvector_expr.h:1465
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:39
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
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:84
unary_exprt::op
const exprt & op() const
Definition std_expr.h:391
bvt
std::vector< literalt > bvt
Definition literal.h:201