19 if(expr.
id()==ID_bitnot)
22 throw "bitnot takes one operand";
28 if(op_bv.size()!=width)
29 throw "convert_bitwise: unexpected operand width";
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)
46 throw "convert_bitwise: unexpected operand width";
52 for(std::size_t i=0; i<width; i++)
54 if(expr.
id()==ID_bitand)
56 else if(expr.
id()==ID_bitor)
58 else if(expr.
id()==ID_bitxor)
60 else if(expr.
id()==ID_bitnand)
62 else if(expr.
id()==ID_bitnor)
64 else if(expr.
id()==ID_bitxnor)
67 throw "unexpected operand";
75 throw "unexpected bitwise operand";
bvt inverted(const bvt &op)
boolbv_widtht boolbv_width
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr)
virtual literalt lxor(literalt a, literalt b)=0
void conversion_failed(const exprt &expr, bvt &bv)
#define forall_operands(it, expr)
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
Base class for all expressions.
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt
virtual bvt convert_bitwise(const exprt &expr)