cprover
boolbv_complex.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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  if(expr.type().id()==ID_complex)
20  {
21  const exprt::operandst &operands=expr.operands();
22 
23  bvt bv;
24  bv.reserve(width);
25 
26  if(operands.size()==2)
27  {
28  std::size_t op_width=width/operands.size();
29 
30  forall_expr(it, operands)
31  {
32  const bvt &tmp=convert_bv(*it);
33 
34  if(tmp.size()!=op_width)
35  throw "convert_complex: unexpected operand width";
36 
37  forall_literals(it2, tmp)
38  bv.push_back(*it2);
39  }
40  }
41 
42  return bv;
43  }
44 
45  return conversion_failed(expr);
46 }
47 
49 {
50  std::size_t width=boolbv_width(expr.type());
51 
52  if(width==0)
53  return conversion_failed(expr);
54 
55  if(expr.operands().size()!=1)
56  return conversion_failed(expr);
57 
58  bvt bv=convert_bv(expr.op0());
59 
60  assert(bv.size()==width*2);
61  bv.resize(width); // chop
62 
63  return bv;
64 }
65 
67 {
68  std::size_t width=boolbv_width(expr.type());
69 
70  if(width==0)
71  return conversion_failed(expr);
72 
73  if(expr.operands().size()!=1)
74  return conversion_failed(expr);
75 
76  bvt bv=convert_bv(expr.op0());
77 
78  assert(bv.size()==width*2);
79  bv.erase(bv.begin(), bv.begin()+width);
80 
81  return bv;
82 }
virtual bvt convert_complex_real(const exprt &expr)
exprt & op0()
Definition: expr.h:72
boolbv_widtht boolbv_width
Definition: boolbv.h:90
#define forall_expr(it, expr)
Definition: expr.h:28
typet & type()
Definition: expr.h:56
#define forall_literals(it, bv)
Definition: literal.h:202
virtual bvt convert_complex(const exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
virtual bvt convert_complex_imag(const exprt &expr)
std::vector< exprt > operandst
Definition: expr.h:45
Base class for all expressions.
Definition: expr.h:42
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200