cprover
boolbv_replication.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/arith_tools.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  mp_integer times;
21  if(to_integer(expr.op0(), times))
22  throw "replication takes constant as first parameter";
23 
24  bvt bv;
25  bv.resize(width);
26 
27  const std::size_t u_times=integer2unsigned(times);
28  const bvt &op=convert_bv(expr.op1());
29  std::size_t offset=0;
30 
31  for(std::size_t i=0; i<u_times; i++)
32  {
33  if(op.size()+offset>width)
34  throw "replication operand width too big";
35 
36  for(std::size_t i=0; i<op.size(); i++)
37  bv[i+offset]=op[i];
38 
39  offset+=op.size();
40  }
41 
42  if(offset!=bv.size())
43  throw "replication operand width too small";
44 
45  return bv;
46 }
BigInt mp_integer
Definition: mp_arith.h:19
exprt & op0()
Definition: expr.h:84
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual bvt convert_replication(const replication_exprt &expr)
typet & type()
Definition: expr.h:60
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
Bit-vector replication.
Definition: std_expr.h:2361
std::vector< literalt > bvt
Definition: literal.h:197