cprover
boolbv_bitwise.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.id()==ID_bitnot)
20  {
21  if(expr.operands().size()!=1)
22  throw "bitnot takes one operand";
23 
24  const exprt &op0=expr.op0();
25 
26  const bvt &op_bv=convert_bv(op0);
27 
28  if(op_bv.size()!=width)
29  throw "convert_bitwise: unexpected operand width";
30 
31  return bv_utils.inverted(op_bv);
32  }
33  else if(expr.id()==ID_bitand || expr.id()==ID_bitor ||
34  expr.id()==ID_bitxor ||
35  expr.id()==ID_bitnand || expr.id()==ID_bitnor ||
36  expr.id()==ID_bitxnor)
37  {
38  bvt bv;
39  bv.resize(width);
40 
41  forall_operands(it, expr)
42  {
43  const bvt &op=convert_bv(*it);
44 
45  if(op.size()!=width)
46  throw "convert_bitwise: unexpected operand width";
47 
48  if(it==expr.operands().begin())
49  bv=op;
50  else
51  {
52  for(std::size_t i=0; i<width; i++)
53  {
54  if(expr.id()==ID_bitand)
55  bv[i]=prop.land(bv[i], op[i]);
56  else if(expr.id()==ID_bitor)
57  bv[i]=prop.lor(bv[i], op[i]);
58  else if(expr.id()==ID_bitxor)
59  bv[i]=prop.lxor(bv[i], op[i]);
60  else if(expr.id()==ID_bitnand)
61  bv[i]=prop.lnand(bv[i], op[i]);
62  else if(expr.id()==ID_bitnor)
63  bv[i]=prop.lnor(bv[i], op[i]);
64  else if(expr.id()==ID_bitxnor)
65  bv[i]=prop.lequal(bv[i], op[i]);
66  else
67  throw "unexpected operand";
68  }
69  }
70  }
71 
72  return bv;
73  }
74 
75  throw "unexpected bitwise operand";
76 }
bvt inverted(const bvt &op)
Definition: bv_utils.cpp:561
bv_utilst bv_utils
Definition: boolbv.h:93
exprt & op0()
Definition: expr.h:84
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:60
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
virtual literalt lxor(literalt a, literalt b)=0
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
#define forall_operands(it, expr)
Definition: expr.h:17
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
Base class for all expressions.
Definition: expr.h:46
operandst & operands()
Definition: expr.h:70
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt
Definition: literal.h:197
virtual bvt convert_bitwise(const exprt &expr)