cprover
Loading...
Searching...
No Matches
boolbv_vector.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#include "boolbv.h"
11
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}
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:40
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:84
virtual bvt convert_vector(const vector_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Vector constructor from list of elements.
Definition std_expr.h:1575
std::vector< literalt > bvt
Definition literal.h:201