cprover
boolbv_array.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_array)
20  {
21  assert(expr.has_operands());
22  const exprt::operandst &operands=expr.operands();
23  assert(!operands.empty());
24  std::size_t op_width=width/operands.size();
25 
26  bvt bv;
27  bv.reserve(width);
28 
29  forall_expr(it, operands)
30  {
31  const bvt &tmp=convert_bv(*it);
32 
33  if(tmp.size()!=op_width)
34  throw "convert_array: unexpected operand width";
35 
36  forall_literals(it2, tmp)
37  bv.push_back(*it2);
38  }
39 
40  return bv;
41  }
42 
43  return conversion_failed(expr);
44 }
boolbv_widtht boolbv_width
Definition: boolbv.h:90
#define forall_expr(it, expr)
Definition: expr.h:28
typet & type()
Definition: expr.h:60
#define forall_literals(it, bv)
Definition: literal.h:199
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
bool has_operands() const
Definition: expr.h:67
std::vector< exprt > operandst
Definition: expr.h:49
virtual bvt convert_array(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197