Go to the documentation of this file.
19 if(expr.
id()==ID_bitnot)
25 else if(expr.
id()==ID_bitand || expr.
id()==ID_bitor ||
26 expr.
id()==ID_bitxor ||
27 expr.
id()==ID_bitnand || expr.
id()==ID_bitnor ||
28 expr.
id()==ID_bitxnor)
41 for(std::size_t i=0; i<width; i++)
43 if(expr.
id()==ID_bitand)
45 else if(expr.
id()==ID_bitor)
47 else if(expr.
id()==ID_bitxor)
49 else if(expr.
id()==ID_bitnand)
51 else if(expr.
id()==ID_bitnor)
53 else if(expr.
id()==ID_bitxnor)
std::vector< literalt > bvt
Base class for all expressions.
virtual literalt lor(literalt a, literalt b)=0
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
static bvt inverted(const bvt &op)
virtual literalt land(literalt a, literalt b)=0
typet & type()
Return the type of the expression.
virtual literalt lxor(literalt a, literalt b)=0
void conversion_failed(const exprt &expr, bvt &bv)
virtual std::size_t boolbv_width(const typet &type) const
#define forall_operands(it, expr)
virtual literalt lnand(literalt a, literalt b)=0
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_bitwise(const exprt &expr)
virtual literalt lequal(literalt a, literalt b)=0
API to expression classes for bitvectors.
virtual literalt lnor(literalt a, literalt b)=0