cprover
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
17 if(width==0)
18 return conversion_failed(expr);
19
21 expr.type().id() == ID_complex,
22 "complex expression shall have complex type");
23
24 bvt bv;
25 bv.reserve(width);
26
27 const exprt::operandst &operands = expr.operands();
28 std::size_t op_width = width / operands.size();
29
30 for(const auto &op : operands)
31 {
32 const bvt &tmp = convert_bv(op, op_width);
33
34 bv.insert(bv.end(), tmp.begin(), tmp.end());
35 }
36
37 return bv;
38}
39
41{
42 std::size_t width=boolbv_width(expr.type());
43
44 if(width==0)
45 return conversion_failed(expr);
46
47 bvt bv = convert_bv(expr.op(), width * 2);
48
49 bv.resize(width); // chop
50
51 return bv;
52}
53
55{
56 std::size_t width=boolbv_width(expr.type());
57
58 if(width==0)
59 return conversion_failed(expr);
60
61 bvt bv = convert_bv(expr.op(), width * 2);
62
63 bv.erase(bv.begin(), bv.begin()+width);
64
65 return bv;
66}
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 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 std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
Complex constructor from a pair of numbers.
Definition: std_expr.h:1761
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
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
const irep_idt & id() const
Definition: irep.h:396
const exprt & op() const
Definition: std_expr.h:293
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:510