cprover
boolbv_vector.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_vector)
20  {
21  const exprt::operandst &operands=expr.operands();
22 
23  bvt bv;
24  bv.reserve(width);
25 
26  if(!operands.empty())
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_vector: 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 }
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
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
std::vector< exprt > operandst
Definition: expr.h:45
virtual bvt convert_vector(const exprt &expr)
Base class for all expressions.
Definition: expr.h:42
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200