CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
boolbv_complex.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/invariant.h>
12
14{
15 std::size_t width=boolbv_width(expr.type());
16
18 expr.type().id() == ID_complex,
19 "complex expression shall have complex type");
20
21 bvt bv;
22 bv.reserve(width);
23
24 const exprt::operandst &operands = expr.operands();
25 std::size_t op_width = width / operands.size();
26
27 for(const auto &op : operands)
28 {
29 const bvt &tmp = convert_bv(op, op_width);
30
31 bv.insert(bv.end(), tmp.begin(), tmp.end());
32 }
33
34 return bv;
35}
36
38{
39 std::size_t width=boolbv_width(expr.type());
40
41 bvt bv = convert_bv(expr.op(), width * 2);
42
43 bv.resize(width); // chop
44
45 return bv;
46}
47
49{
50 std::size_t width=boolbv_width(expr.type());
51
52 bvt bv = convert_bv(expr.op(), width * 2);
53
54 bv.erase(bv.begin(), bv.begin()+width);
55
56 return bv;
57}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual bvt convert_complex(const complex_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:388
const exprt & op() const
Definition std_expr.h:391
std::vector< literalt > bvt
Definition literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534